Quadratic functions in vertex form: evaluation, symmetry, global maximum and a restricted domain

Goal and scope

q:ℝ→ℝ, q(x)=−2(x−3)²+5 (a=−2, h=3, k=5). Evaluate q(1) step by step and find its mirror point; prove q(6−x)=q(x) for every real x; prove that the global maximum of q is 5, attained only at x=3, that the vertex is (3,5), and that q has no global minimum; then show that on the restricted domain [4,6] the maximum is 3 (at x=4), and that the conclusions do not carry over when a=0.

Inside the MKO: the input ranges over all reals, a≠0, integer parameters, exact substitution (a1, a2). Symmetry is proved for general h; the extremum results are proved for this function with a=−2<0, and the case a>0 is analogous but not written out. On the restricted domain only the maximum on [4,6] is treated. Completing the square from ax²+bx+c, solving quadratic equations and differentiation are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• square_nonneg
• order_basics
• distributive
• neg_mul
• numeric_evaluation

• G1 — q:ℝ→ℝ, q(x)=−2(x−3)²+5; a=−2, h=3, k=5 are integers, a≠0, and the domain is all reals (MKO a1, a2).
• G2 — Restricted-domain question: D=[4,6], that is 4≤x≤6.
• G3 — Comparison: r(x)=0·(x−3)²+5 (a=0, not a quadratic in this entry).

• q(x)=a(x-h)^2+k — a quadratic in vertex form
• a=-2,\ h=3,\ k=5 — this guide's parameters
• (h,k)=(3,5) — the vertex (a coordinate pair)
• x=h — the axis of symmetry
• 2h-x — the x-coordinate after reflection across the symmetry axis

Rules and sources

• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_zero · prerequisite — Additive identity: u+0=u.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• mko_quadratic · cited — Let q:R→R be q(x)=a(x−h)²+k with real a,h,k and a≠0. Its vertex is (h,k) and its axis is x=h. When a>0, the global minimum is k; when a<0, the global maximum is k, both attained at x=h. The point (2h−x,q(x)) mirrors (x,q(x)) across the axis. · mko-quadratic-function
• L_mirror · lemma — For all reals x, h: ((2h−x)−h)²=(x−h)².
• L_unbounded · lemma — For every real M there is a real x with q(x)<M (q(x)=−2(x−3)²+5).
• L_sq_ge_one · lemma — For a real u≥1: u²≥u≥1.

Main derivation

q(x)=-2(x-3)^2+5

a=-2\neq0,\ h=3,\ k=5,\ \mathrm{dom}\,q=\mathbb{R}

q(1)

-3

x=1,\ 2h-x

2h-x=5,\ q(5)=-2(5-3)^2+5=-3=q(1)

q(2h-x)=a((2h-x)-h)^2+k

a(x-h)^2+k=q(x)

x\in\mathbb{R}

(x-3)^2\ge0

(x-3)^2\ge0,\ a=-2<0

-2(x-3)^2\le0

-2(x-3)^2\le0

q(x)=-2(x-3)^2+5\le5\ \ \forall x\in\mathbb{R}

q(3)=-2\cdot0^2+5

q(3)=5=\max_{\mathbb{R}}q,\ \text{vertex}\ (3,5)

q(x)=5

x=3

x_0\in\mathbb{R}

\exists x:\ q(x)<q(x_0)

4\le x\le6

x-3\ge1\ \Rightarrow\ (x-3)^2\ge1

(x-3)^2\ge1\ \ (x\in[4,6])

q(x)\le-2+5=3,\ q(4)=3=\max_{[4,6]}q

r(x)=0\cdot(x-3)^2+5

r(x)=5\ \ \forall x

\text{S02 to S13}

q(1)=q(5)=-3;\ q(6-x)=q(x);\ \max_{\mathbb{R}}q=5\ \text{only at}\ 3;\ \text{no min};\ \max_{[4,6]}q=3

Substeps and lemmas

x-h\ \text{at}\ x=1

1-3=-2

(-2)^2

4

a\cdot4+k

-2\cdot4+5=-3

(2h-x)-h

h-x

(h-x)^2

(-(x-h))^2=(x-h)^2

q(3+t)

-2t^2+5

M\in\mathbb{R},\ t=|5-M|+1

q(3+t)=5-2t^2<M

u\ge1

u^2\ge u\ge1

Reverse audits

• S14 · sufficient_goal_reduction · S02, S03, S04, S08, S09, S10, S12, S13, and_intro_elim — Goal G is everything asked in the goal; the sufficient condition H is the conjunction of the step results, all proved forwards, and H⇒G uses only conjunction introduction.
• S13 · premise_audit · mul_zero, G3 — Only multiplication by 0 is used; the conclusion is a contrast showing that the hypothesis a≠0 cannot be dropped.
• S12 · premise_audit · S11, S09, order_basics, numeric_evaluation — It needs both the upper bound (this step) and the point of attainment x=4∈D; the minimum on D is not claimed.
• S11.1 · premise_audit · order_basics, mul_one — It needs u>0 to multiply while keeping the order; for u≤−1 the conclusion u²≥1 still holds but needs a separate argument, which this guide does not need.
• S11 · premise_audit · L_sq_ge_one, order_basics — Only the lower end x≥4 of D is used; this is a one-way inference.
• S10.2 · premise_audit · order_basics, abs_rules, square_nonneg — It uses |u|≥u, order-preservation under multiplication by positives, and transitivity; t is chosen explicitly, with no reliance on a finite check.
• S10.1 · inverse_equivalence · eq_replace, add_inverse — The substitutions x=3+t and t=x−3 are inverse to each other, and the two expressions agree for every t.
• S10 · premise_audit · L_unbounded, forall_intro — x₀ is arbitrary, so no point is a minimizer; this relies on the domain being all reals.
• S09 · inverse_equivalence · eq_congruence, zero_product, square_nonneg — All three links are equivalences: subtracting 5 is reversible, the zero-product property and the zero-square property are two-way.
• S08 · premise_audit · S07, numeric_evaluation, mko_quadratic — A maximum needs both an upper bound and attainment; S07 gives the bound and this step the point of attainment.
• S07 · premise_audit · order_basics, forall_intro — Addition preserves order; the generalization to all x relies only on x being arbitrary. An upper bound is not yet a maximum; S08 shows it is attained.
• S06 · premise_audit · order_basics, case_analysis, mul_zero — Reversal under multiplication by a negative is the key; with a>0 the conclusion would become ≥0, giving a minimum instead of a maximum.
• S05 · premise_audit · square_nonneg — A direct use of nonnegativity of squares; it needs x to be real (MKO a1).
• S04.2 · inverse_equivalence · neg_mul — The sign rule is an identity and holds both ways.
• S04.1 · inverse_equivalence · add_assoc, add_comm, add_inverse — An identity for all reals; it holds both ways.
• S04 · inverse_equivalence · L_mirror, eq_replace — Replacing the squared bracket by an equal expression leaves the same number on both sides, so it holds both ways.
• S03 · inverse_equivalence · numeric_evaluation — Exact arithmetic; this is only one instance, and the general symmetry is proved in S04.
• S02.3 · inverse_equivalence · numeric_evaluation — Exact integer arithmetic, checkable backwards.
• S02.2 · inverse_equivalence · numeric_evaluation, neg_mul — Exact arithmetic with the sign rule (−u)(−v)=uv.
• S02.1 · inverse_equivalence · numeric_evaluation — Integer subtraction, checkable backwards: −2+3=1.
• S02 · inverse_equivalence · numeric_evaluation, eq_replace — Each sub-step is an exact evaluation of equals, so the chain gives the same value on both sides.
• S01 · premise_audit · G1, mko_quadratic — This only reads off the parameters and confirms a≠0; no extremum property is derived yet.

Error controls and negative controls

The vertex is not the extreme value

One misconception identified in the MKO is conflating the vertex with the extreme value. The vertex is the coordinate pair (3,5); the maximum value is the number 5; the place where it is attained is x=3 (S08). Saying 'the maximum is (3,5)' or 'the maximum is 3' is wrong.

A restricted domain needs its own check

The other misconception is to carry the all-reals conclusion over to a restricted domain. On [4,6], x=3 is not in the interval and the maximum is 3 (at x=4), not 5 (S12). Nor does it carry over to a=0: r(x)=5 is constant (S13).

A negative coefficient may not be replaced by its absolute value

Replacing a=−2 by 2 gives 2(x−3)²+5, which opens upwards with minimum 5 and no maximum, the opposite conclusion. S02.3 and S06 both keep the negative sign of a.

• The maximum of q is (3,5) → reject — (3,5) is the vertex (a coordinate pair); the maximum is the number 5, attained at x=3.
• On [4,6] the maximum of q is 5 → reject — q(x)=5 only at x=3, and 3∉[4,6]; the maximum on [4,6] is q(4)=3.
• q also has a global minimum, since a parabola takes an extremum at its vertex → reject — With a<0 the vertex gives the maximum; for every M some x has q(x)<M (S10), so there is no minimum.
• The maximum of r(x)=0·(x−3)²+5 is attained only at x=3 → reject — r is the constant 5, so every x attains the maximum; a=0 is outside this entry.

Result and limitations

q(1)=−3, its mirror point 5 across x=3 also has q(5)=−3, and q(6−x)=q(x) for every real x. Since (x−3)²≥0 and a=−2<0, q(x)≤5 for all x and q(3)=5, so the global maximum is 5, attained only at x=3, and the vertex is (3,5); q has no global minimum. On [4,6] the maximum is 3 (at x=4), and the global maximum 5 does not occur. With a=0 the function is the constant 5 and the conclusions do not apply.

• N13 is only a finite check at the 41 integers from −20 to 20 and does not prove S07; S07 is proved by the argument of S05 and S06.
• The minimum case a>0 is symmetric to this guide and not written out; converting a general quadratic to vertex form is outside this guide.

Verification and source binding

14 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 66a236eb7dc1563609f389b65f6d95f1730346ffad6bd1bf7d19007ea7af878b
• original source SHA-256: 66a236eb7dc1563609f389b65f6d95f1730346ffad6bd1bf7d19007ea7af878b
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)