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

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-quadratic-function/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-quadratic-function-01 · production-20261019-adopted-96



## 目標與範圍

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。





## 逐步主鏈

S01 · definition操作前

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

操作後

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

條件：a\neq0

規則：mko_quadratic · 依賴：G1, mko_quadratic

葉節點依據：mko_quadratic + def_unfold

對照頂點式 a(x−h)²+k 讀出 a=−2、h=3、k=5。a≠0，所以 q 是本條目所說的二次函數；定義域是全部實數。MKO 預告的結論是：頂點 (3,5)、對稱軸 x=3，因 a<0 全域最大值為 5，在 x=3 取得；本稿逐一證明。



S02 · equivalent操作前

q(1)

操作後

-3

條件：無

規則：numeric_evaluation · 依賴：S01

葉節點依據：numeric_evaluation + eq_replace

依 MKO 的代入次序：先算 x−h，再平方，再乘 a，最後加 k；三個子步 S02.1 至 S02.3 給出 q(1)=−3。



S03 · equivalent操作前

x=1,\ 2h-x

操作後

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

條件：無

規則：numeric_evaluation · 依賴：S01, S02

葉節點依據：numeric_evaluation

x=1 關於對稱軸 x=3 的對稱點是 2·3−1=5；兩點與軸的距離都是 2。代入得 q(5)=−2·4+5=−3，與 q(1) 相同，所以 (1,−3) 與 (5,−3) 互為對稱點。



S04 · equivalent操作前

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

操作後

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

條件：無

規則：L_mirror · 依賴：S01

葉節點依據：add_assoc + add_inverse + neg_mul + eq_replace

依引理 L_mirror，((2h−x)−h)²=(x−h)²，代入後 q(2h−x)=q(x) 對所有實數 x 成立（本例為 q(6−x)=q(x)）。x=h 時 2h−h=h，頂點的對稱點就是它自己。引理在 S04.1、S04.2 證明。



S05 · implies操作前

x\in\mathbb{R}

操作後

(x-3)^2\ge0

條件：無

規則：square_nonneg · 依賴：square_nonneg

葉節點依據：square_nonneg

對任意實數 x，(x−3)² 是平方，因此非負；等號恰在 x−3=0 時成立。



S06 · implies操作前

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

操作後

-2(x-3)^2\le0

條件：-2<0

規則：order_basics · 依賴：S05, order_basics

葉節點依據：order_basics + case_analysis + mul_zero

分兩種情形：若 (x−3)²=0，乘積為 0；若 (x−3)²>0，把 0<(x−3)² 兩邊乘以負數 −2，不等號反向，得 0>−2(x−3)²。兩種情形都有 −2(x−3)²≤0。正因 a<0，開口向下。



S07 · implies操作前

-2(x-3)^2\le0

操作後

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

條件：無

規則：order_basics · 依賴：S06, order_basics

葉節點依據：order_basics + forall_intro

兩邊同加 5，順序保持：q(x)≤5。x 是任意實數，所以 5 是 q 在全部實數上的一個上界。



S08 · implies操作前

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

操作後

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

條件：無

規則：mko_quadratic · 依賴：S07, S01

葉節點依據：mko_quadratic + numeric_evaluation + and_intro_elim

q(3)=−2·0+5=5，上界 5 被取得，所以 5 是全域最大值，在 x=3 取得。頂點是坐標對 (3,5)，最大值是數 5，取得處是 x=3，三者不同。



S09 · equivalent操作前

q(x)=5

操作後

x=3

條件：-2\neq0

規則：zero_product · 依賴：S01, zero_product, square_nonneg

葉節點依據：eq_congruence + zero_product + square_nonneg

q(x)=5 ⇔ −2(x−3)²=0（兩邊減 5）⇔ (x−3)²=0（零積性質，−2≠0）⇔ x=3（平方為零當且僅當底數為零）。所以最大值只在 x=3 取得。



S10 · implies操作前

x_0\in\mathbb{R}

操作後

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

條件：無

規則：L_unbounded · 依賴：S01

葉節點依據：order_basics + forall_intro

q 沒有全域最小值：任取候選點 x₀，依引理 L_unbounded 取 M=q(x₀)，存在 x 使 q(x)<q(x₀)，所以 q(x₀) 不是最小值。引理在 S10.1、S10.2 證明；這對應 MKO 所說「另一方向沒有全域極值」。



S11 · implies操作前

4\le x\le6

操作後

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

條件：x\in[4,6]

規則：L_sq_ge_one · 依賴：G2

葉節點依據：order_basics

轉到限制區間 D=[4,6]（MKO a1 要求另行檢查）。x≥4 兩邊減 3 得 x−3≥1；依引理 L_sq_ge_one，(x−3)²≥1。證明在 S11.1。



S12 · implies操作前

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

操作後

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

條件：-2<0

規則：order_basics · 依賴：S11, S09, G2

葉節點依據：order_basics + numeric_evaluation

把 (x−3)²≥1 乘以 −2<0，不等號反向：−2(x−3)²≤−2；加 5 得 q(x)≤3。q(4)=−2·1+5=3，所以 D 上最大值是 3，在 x=4 取得。全域最大值 5 只在 x=3 取得（S09），而 3∉D，所以 5 在 D 上不會出現。



S13 · implies操作前

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

操作後

r(x)=5\ \ \forall x

條件：無

規則：mul_zero · 依賴：G3

葉節點依據：mul_zero + forall_intro

a=0 時 0·(x−3)²=0，r 是常數函數 5：每一點都是最大值點，也都是最小值點，沒有唯一頂點或對稱軸。這不是本條目的二次函數，S08、S09 的「只在 x=3 取得」不能沿用（MKO a2）。



S14 · implies操作前

\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

條件：無

規則：and_intro_elim · 依賴：S02, S03, S04, S08, S09, S10, S12, S13

葉節點依據：and_intro_elim

整理：q(1)=−3，對稱點 5 也有 q(5)=−3；q(6−x)=q(x) 對所有 x 成立；全域最大值 5 只在 x=3 取得，頂點 (3,5)，沒有全域最小值；限制在 [4,6] 時最大值是 3（x=4）；a=0 時結論失效。







## 局部子步與引理

S02.1 · equivalent操作前

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

操作後

1-3=-2

條件：無

規則：numeric_evaluation · 依賴：S01

葉節點依據：numeric_evaluation

先算括號內：1−3=−2。



S02.2 · equivalent操作前

(-2)^2

操作後

4

條件：無

規則：numeric_evaluation · 依賴：S02.1

葉節點依據：numeric_evaluation + neg_mul

平方：(−2)²=(−2)(−2)=4，負數的平方為正。



S02.3 · equivalent操作前

a\cdot4+k

操作後

-2\cdot4+5=-3

條件：無

規則：numeric_evaluation · 依賴：S02.2

葉節點依據：numeric_evaluation

乘以 a=−2 得 −8，再加 k=5 得 −3。負的 a 保持原樣，不取絕對值。



S04.1 · equivalent操作前

(2h-x)-h

操作後

h-x

條件：無

規則：add_assoc · 依賴：add_assoc, add_inverse

葉節點依據：add_assoc + add_comm + add_inverse + add_zero

(2h−x)−h=(h+h−x)−h=h−x（加法結合、交換與反元素）。



S04.2 · equivalent操作前

(h-x)^2

操作後

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

條件：無

規則：neg_mul · 依賴：S04.1, neg_mul

葉節點依據：neg_mul + distributive

h−x=−(x−h)，而 (−u)(−u)=u·u，所以 (h−x)²=(x−h)²。S04.1 與 S04.2 合起來證得引理 L_mirror。



S10.1 · equivalent操作前

q(3+t)

操作後

-2t^2+5

條件：無

規則：eq_replace · 依賴：S01, eq_replace

葉節點依據：eq_replace + add_inverse

令 x=3+t：x−3=t，所以 q(3+t)=−2t²+5。



S10.2 · implies操作前

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

操作後

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

條件：t\ge1

規則：order_basics · 依賴：S10.1, order_basics, abs_rules

葉節點依據：order_basics + abs_rules + square_nonneg

給定 M，取 t=|5−M|+1≥1。把 t≥1 乘以 t>0 得 t²≥t；又 t>|5−M|≥5−M，所以 t²>5−M；而 t²≥0 使 2t²≥t²>5−M。移項得 5−2t²<M。S10.1 與 S10.2 合起來證得引理 L_unbounded。



S11.1 · implies操作前

u\ge1

操作後

u^2\ge u\ge1

條件：u\ge1

規則：order_basics · 依賴：order_basics

葉節點依據：order_basics + mul_one

u≥1>0。把 u≥1 兩邊乘以正數 u 得 u²≥u，再由傳遞性 u²≥u≥1。此步證得引理 L_sq_ge_one。







## 逐步反向審查


- 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-quadratic-function-01.json)