頂點式二次函數：求值、對稱、全域最大值與限制區間

目標與範圍

q:ℝ→ℝ，q(x)=−2(x−3)²+5（a=−2、h=3、k=5）。依序求 q(1) 及其對稱點；證明對所有實數 x 有 q(6−x)=q(x)；證明 q 的全域最大值為 5、只在 x=3 取得，頂點為 (3,5)，且 q 沒有全域最小值；再說明限制在 [4,6] 時最大值是 3（在 x=4），以及 a=0 時結論不能沿用。

在 MKO 範圍內：自變數遍及全部實數、a≠0、整數參數、精確代入（a1、a2）。對稱性對一般 h 證明；極值結論只對 a=−2<0 的這個函數證明，a>0 的情形同理但未寫出。限制區間只處理 [4,6] 上的最大值。不處理一般式 ax²+bx+c 的配方、二次方程式的解或微分；不改動 canonical MKO 或英文 edition。

已知條件與符號

• square_nonneg
• order_basics
• distributive
• neg_mul
• numeric_evaluation

• G1 — q:ℝ→ℝ，q(x)=−2(x−3)²+5；a=−2、h=3、k=5 為整數，a≠0，定義域為全部實數（MKO a1、a2）。
• G2 — 限制區間題：D=[4,6]，即 4≤x≤6。
• G3 — 對照：r(x)=0·(x−3)²+5（a=0，不屬於本條目的二次函數）。

• q(x)=a(x-h)^2+k — 頂點式二次函數
• a=-2,\ h=3,\ k=5 — 本稿的參數
• (h,k)=(3,5) — 頂點（坐標對）
• x=h — 對稱軸
• 2h-x — 橫坐標 x 關於對稱軸反射後的值

規則與來源

• square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
• order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• add_zero · prerequisite — 加法單位元：u+0=u。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• zero_product · prerequisite — 零乘積性質：在 ℤ、ℚ、ℝ、ℂ（或任何整域）中，uv=0 ⇔ u=0 或 v=0。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• mko_quadratic · cited — 令 q:R→R，q(x)=a(x−h)²+k，其中 a、h、k 為實數且 a≠0。其頂點為 (h,k)，對稱軸為 x=h；a>0 時全域最小值為 k，a<0 時全域最大值為 k，均在 x=h 取得。圖上 (x,q(x)) 關於該軸的對稱點為 (2h−x,q(x))。 · mko-quadratic-function
• L_mirror · lemma — 對所有實數 x、h：((2h−x)−h)²=(x−h)²。
• L_unbounded · lemma — 對每個實數 M，存在實數 x 使 q(x)<M（q(x)=−2(x−3)²+5）。
• L_sq_ge_one · lemma — 對實數 u≥1：u²≥u≥1。

逐步主鏈

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

局部子步與引理

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

逐步反向審查

• S14 · sufficient_goal_reduction · S02, S03, S04, S08, S09, S10, S12, S13, and_intro_elim — 目標 G 為 goal 的全部要求；足夠條件 H 為各步結論的合取，皆已正向證成，H⇒G 只用合取引入。
• S13 · premise_audit · mul_zero, G3 — 只用到乘以 0 得 0；結論是對照，說明 a≠0 這個前提不可省略。
• S12 · premise_audit · S11, S09, order_basics, numeric_evaluation — 需要上界（本步）與取得點 x=4∈D 兩者；不宣稱 D 上的最小值。
• S11.1 · premise_audit · order_basics, mul_one — 需要 u>0 才能保序相乘；對 u≤−1 結論 u²≥1 仍成立但需另證，本稿不需要。
• S11 · premise_audit · L_sq_ge_one, order_basics — 只用到 D 的下端 x≥4；這是單向推論。
• S10.2 · premise_audit · order_basics, abs_rules, square_nonneg — 用到 |u|≥u、正數乘法保序與傳遞性；t 的選法明確，不依賴任何有限核對。
• S10.1 · inverse_equivalence · eq_replace, add_inverse — 代換 x=3+t 與 t=x−3 互逆，兩式對每個 t 同值。
• S10 · premise_audit · L_unbounded, forall_intro — x₀ 任意，所以沒有任何點是最小值點；這依賴定義域是全部實數。
• S09 · inverse_equivalence · eq_congruence, zero_product, square_nonneg — 三個環節都是等價：同減 5 可逆、零積性質雙向、平方為零雙向。
• S08 · premise_audit · S07, numeric_evaluation, mko_quadratic — 最大值需要「上界」與「被取得」兩者；S07 給上界，本步給取得點。
• S07 · premise_audit · order_basics, forall_intro — 加法保序；推廣到所有 x 只因 x 任意。上界還不是最大值，需 S08 證明被取得。
• S06 · premise_audit · order_basics, case_analysis, mul_zero — 乘負數反向是關鍵；若 a>0，結論會變成 ≥0，給出最小值而非最大值。
• S05 · premise_audit · square_nonneg — 直接套用平方非負；這需要 x 是實數（MKO a1）。
• S04.2 · inverse_equivalence · neg_mul — 符號規則是恆等式，雙向成立。
• S04.1 · inverse_equivalence · add_assoc, add_comm, add_inverse — 對所有實數成立的恆等式，雙向成立。
• S04 · inverse_equivalence · L_mirror, eq_replace — 等值替換括號內的平方，兩邊是同一個數，雙向成立。
• S03 · inverse_equivalence · numeric_evaluation — 精確計算；這只是一個實例，一般對稱性在 S04 證明。
• S02.3 · inverse_equivalence · numeric_evaluation — 精確整數計算，可逆向核對。
• S02.2 · inverse_equivalence · numeric_evaluation, neg_mul — 精確計算，符號規則 (−u)(−v)=uv。
• S02.1 · inverse_equivalence · numeric_evaluation — 整數減法，可逆向核對 −2+3=1。
• S02 · inverse_equivalence · numeric_evaluation, eq_replace — 每個子步都是精確的等值計算，串起來兩邊同值。
• S01 · premise_audit · G1, mko_quadratic — 只讀出參數並確認 a≠0；尚未推出任何極值性質。

錯誤控制與反例

頂點不是極值

MKO 的誤解之一是混用頂點與極值。頂點是坐標對 (3,5)；最大值是數 5；取得最大值的位置是 x=3（S08）。說「最大值是 (3,5)」或「最大值是 3」都錯。

限制區間要另行檢查

另一個誤解是在限制區間上直接沿用全實數結論。在 [4,6] 上 x=3 不在區間內，最大值是 3（x=4），不是 5（S12）。零係數 a=0 也不能沿用：r(x)=5 是常數（S13）。

負係數不能取絕對值

若把 a=−2 換成 2，函數變成 2(x−3)²+5，開口向上，最小值 5、沒有最大值，結論恰好相反。S02.3 與 S06 都保留 a 的負號。

• q 的最大值是 (3,5) → reject — (3,5) 是頂點（坐標對）；最大值是數 5，在 x=3 取得。
• 在 [4,6] 上 q 的最大值是 5 → reject — q(x)=5 只在 x=3，而 3∉[4,6]；[4,6] 上最大值為 q(4)=3。
• q 也有全域最小值，因為拋物線在頂點取極值 → reject — a<0 時頂點給最大值；對任意 M 都有 x 使 q(x)<M（S10），所以沒有最小值。
• r(x)=0·(x−3)²+5 的最大值只在 x=3 取得 → reject — r 是常數 5，每個 x 都取得最大值；a=0 不屬於本條目。

結論與限制

q(1)=−3，其關於 x=3 的對稱點 5 也有 q(5)=−3，且對所有實數 q(6−x)=q(x)。因 (x−3)²≥0 且 a=−2<0，q(x)≤5 對所有 x 成立，q(3)=5，所以全域最大值為 5，只在 x=3 取得，頂點為 (3,5)；q 沒有全域最小值。限制在 [4,6] 時最大值為 3（在 x=4），全域最大值 5 不出現。a=0 時函數為常數 5，結論不適用。

• N13 只是在 −20 到 20 的 41 個整數點上的有限核對，不證明 S07；S07 由 S05、S06 的論證證明。
• a>0 的最小值情形與本稿對稱，未逐步寫出；由一般式配方成頂點式不在本稿範圍。

驗證及來源綁定

14 個本稿宣告算術檢查；只支持所列算式。

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

同源完整 JSON（含公式、AST、反控制與修訂記錄）