# 凸函數：二次函數 Jensen gap 的完整證書與單一 Jensen 反例

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

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

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



## 目標與範圍

（一）證明 f(x)=2x²−3x+1 在區間 I=[−1,4] 上是凸函數：先確認 I 是凸集合，再對所有 x,y∈I 與所有 λ∈[0,1] 證明 f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y)，方法是證明二次函數的 Jensen gap 等於 aλ(1−λ)(x−y)²。（二）由同一恆等式得仿射函數 ℓ(x)=3x−5 在 I 上取等號。（三）用一個精確的 Jensen 違反否證 g(x)=−x²+x 在 J=[0,2] 上的凸性，並說明幾個通過的樣本為何不能證明凸性。

停在 MKO 的切片內：明示的非空實區間作定義域，一元仿射與二次函數，精確係數。正面結論用覆蓋全部 x、y、λ 的代數證書；反面結論用單一精確違反。不處理嚴格凸、次梯度、二階導數判別或高維凸函數；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- order_basics
- square_nonneg
- distributive
- power_laws
- forall_intro
- quantifier_negation


- G1 — I=[−1,4]；f:I→ℝ，f(x)=2x²−3x+1（a=2、b=−3、c=1）。
- G2 — ℓ:I→ℝ，ℓ(x)=3x−5（a=0、b=3、c=−5，仿射）。
- G3 — J=[0,2]；g:J→ℝ，g(x)=−x²+x（a=−1、b=1、c=0）。


- I=[-1,4],\ J=[0,2] — 明示的定義域區間
- \lambda\in[0,1] — Jensen 組合的權重
- z=\lambda x+(1-\lambda)y — x 與 y 的凸組合
- G_q(x,y,\lambda) — 函數 q 的 Jensen gap：λq(x)+(1−λ)q(y)−q(z)
- a,\ b,\ c — 二次函數 ax²+bx+c 的係數





## 規則與來源


- 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。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
- mul_one · prerequisite — 乘法單位元：1·u=u。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- add_comm · prerequisite — 加法交換律：u+v=v+u。
- forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
- eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
- mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
- mko_cvxf · cited — 在凸定義域 C 上，f 為凸若對所有 x,y∈C 及 λ∈[0,1]，f(λx+(1−λ)y)≤λf(x)+(1−λ)f(y)。單一 Jensen 違反足以否證；單一通過實例不能證凸，正證書需覆蓋全部 x、y、λ。 · mko-convex-function
- mko_cvxset · cited — 實向量空間的子集 C 為凸，若對所有 x,y∈C 及所有 λ∈[0,1]，λx+(1−λ)y 仍屬於 C。 · mko-convex-set
- mono_nonneg · prerequisite — 乘以非負數保持不等號：若 u≤v 且 w≥0，則 wu≤wv（w>0 時由實數的序，w=0 時兩邊都是 0）。
- ineq_add · prerequisite — 不等式相加：若 u₁≤v₁ 且 u₂≤v₂，則 u₁+u₂≤v₁+v₂。
- L_interval · lemma — 若 α≤s≤β、α≤t≤β 且 λ∈[0,1]，則 α≤λs+(1−λ)t≤β；因此每個閉區間 [α,β] 都是凸集合。
- L_gap · lemma — 對 q(x)=ax²+bx+c 與任意實數 x、y、λ：λq(x)+(1−λ)q(y)−q(λx+(1−λ)y)=aλ(1−λ)(x−y)²。





## 逐步主鏈

S01 · equivalent操作前

f\ \text{convex on}\ I

操作後

I\ \text{convex}\ \land\ \forall x,y\in I\ \forall\lambda\in[0,1]:\ f(\lambda x+(1-\lambda)y)\le\lambda f(x)+(1-\lambda)f(y)

條件：無

規則：mko_cvxf · 依賴：G1, mko_cvxf

葉節點依據：mko_cvxf + def_unfold

依 MKO 的定義展開。定義有兩部分：定義域必須是凸集合（否則 λx+(1−λ)y 可能不在定義域，f 在那裡沒有值），以及對所有 x、y、λ 的 Jensen 不等式。兩部分都要證。



S02 · implies操作前

x,y\in[-1,4],\ \lambda\in[0,1]

操作後

z=\lambda x+(1-\lambda)y\in[-1,4];\ I\ \text{convex}

條件：\lambda\in[0,1]

規則：L_interval · 依賴：G1, L_interval, mko_cvxset

葉節點依據：L_interval + forall_intro

用引理 L_interval（α=−1、β=4、s=x、t=y）：z 仍在 [−1,4] 中。x、y、λ 任意，所以 I 符合凸集合的定義；f(z) 因此有定義，Jensen 不等式才有意義。引理在 S02.1、S02.2 中證明。



S03 · equivalent操作前

f(z)\le\lambda f(x)+(1-\lambda)f(y)

操作後

G_f(x,y,\lambda)=\lambda f(x)+(1-\lambda)f(y)-f(z)\ge 0

條件：無

規則：order_basics · 依賴：S01, S02

葉節點依據：order_basics + def_intro

定義 Jensen gap G_f=λf(x)+(1−λ)f(y)−f(z)。不等式兩邊同減 f(z)，方向不變，所以 Jensen 不等式等價於 G_f≥0。之後只需研究 G_f 的符號。



S04 · equivalent操作前

G_q(x,y,\lambda)\ \text{for } q(x)=ax^2+bx+c

操作後

G_q(x,y,\lambda)=a\lambda(1-\lambda)(x-y)^2

條件：無

規則：L_gap · 依賴：L_gap

葉節點依據：distributive + power_laws + add_inverse

引理 L_gap：任何一元二次（含 a=0 的仿射）函數的 Jensen gap 等於 aλ(1−λ)(x−y)²，對所有實數 x、y、λ 成立。證明分三個子步：常數與一次部分抵消（S04.1），展開平方（S04.2），二次部分化成完全平方（S04.3）。N1 是整個恆等式的多項式核對。



S05 · equivalent操作前

G_f(x,y,\lambda)

操作後

G_f(x,y,\lambda)=2\lambda(1-\lambda)(x-y)^2

條件：無

規則：forall_elim · 依賴：S04, G1

葉節點依據：forall_elim + eq_replace

把 L_gap 用在 a=2、b=−3、c=1 的 f 上（全稱命題代入特例）。b、c 不出現在結果中，只有 a=2 決定 gap。



S06 · implies操作前

0\le\lambda\le 1

操作後

\lambda(1-\lambda)\ge 0

條件：\lambda\ge 0; 1-\lambda\ge 0

規則：mono_nonneg · 依賴：S02.1, mono_nonneg, mul_zero

葉節點依據：mono_nonneg + mul_zero

0≤1−λ 兩邊乘以 λ≥0：λ·0≤λ(1−λ)，而 λ·0=0。所以 λ(1−λ)≥0。



S07 · implies操作前

2>0,\ \lambda(1-\lambda)\ge 0,\ (x-y)^2\ge 0

操作後

G_f(x,y,\lambda)=2\lambda(1-\lambda)(x-y)^2\ge 0

條件：無

規則：mono_nonneg · 依賴：S05, S06, square_nonneg, mono_nonneg

葉節點依據：square_nonneg + mono_nonneg + mul_zero

實數平方非負：(x−y)²≥0。0≤(x−y)² 乘以 λ(1−λ)≥0 得 0≤λ(1−λ)(x−y)²；再乘以 2>0 得 0≤2λ(1−λ)(x−y)²。依 S05，G_f≥0。



S08 · implies操作前

G_f(x,y,\lambda)\ge 0\ \text{for arbitrary } x,y\in I,\ \lambda\in[0,1]

操作後

f\ \text{convex on}\ I

條件：無

規則：forall_intro · 依賴：S01, S02, S03, S07, forall_intro

葉節點依據：forall_intro + and_intro_elim

x、y、λ 是任取的，S03 至 S07 沒有對它們加額外假設，依 ∀ 引入，Jensen 不等式對全部 x,y∈I、λ∈[0,1] 成立；加上 S02 的 I 凸，依 S01，f 在 I 上是凸函數。這是覆蓋全部情況的正證書（MKO a2）。



S09 · implies操作前

x=-1,\ y=4,\ \lambda=\tfrac15

操作後

z=3,\ f(3)=10\le 18=\tfrac15 f(-1)+\tfrac45 f(4),\ G_f=8=2\cdot\tfrac15\cdot\tfrac45\cdot 25

條件：無

規則：numeric_evaluation · 依賴：S05, G1

葉節點依據：numeric_evaluation

一個具體實例作示範：z=(1/5)(−1)+(4/5)·4=3；f(3)=18−9+1=10；f(−1)=6、f(4)=21，(1/5)·6+(4/5)·21=18。gap 18−10=8，與 S05 的公式 2·(1/5)·(4/5)·(−5)²=8 一致。這只是例示，不是證明；證明是 S02 至 S08。



S10 · implies操作前

G_\ell(x,y,\lambda)\ \text{for}\ \ell(x)=3x-5

操作後

G_\ell=0\cdot\lambda(1-\lambda)(x-y)^2=0;\ \ell\ \text{convex on}\ I\ \text{with equality}

條件：無

規則：forall_elim · 依賴：S04, S02, G2, forall_intro

葉節點依據：forall_elim + mul_zero + forall_intro

ℓ 是 a=0 的情形，依 L_gap，G_ℓ=0 對所有 x、y、λ 成立，即 ℓ(z)=λℓ(x)+(1−λ)ℓ(y)，Jensen 取等號（MKO para0）。定義域 I 已在 S02 證明是凸的，所以 ℓ 在 I 上是凸函數（而且反向不等式也成立）。



S11 · equivalent操作前

\neg(g\ \text{convex on}\ J)

操作後

\exists x,y\in J\ \exists\lambda\in[0,1]:\ g(\lambda x+(1-\lambda)y)>\lambda g(x)+(1-\lambda)g(y)

條件：無

規則：quantifier_negation · 依賴：G3, mko_cvxf, L_interval, quantifier_negation

葉節點依據：quantifier_negation + order_basics + L_interval

J=[0,2] 依 L_interval 是凸的，所以定義的第一部分成立；g 不凸等價於 Jensen 部分的否定。¬∀ 等價於 ∃¬，而 ¬(u≤v) 等價於 u>v。所以只要一組 x、y、λ 使 g(z) 嚴格大於右邊。



S12 · implies操作前

x=0,\ y=2,\ \lambda=\tfrac12

操作後

z=1\in J,\ g(1)=0,\ \tfrac12 g(0)+\tfrac12 g(2)=\tfrac12\cdot 0+\tfrac12\cdot(-2)=-1

條件：無

規則：numeric_evaluation · 依賴：G3

葉節點依據：numeric_evaluation

取 J 的兩端點 x=0、y=2 與 λ=1/2∈[0,1]：z=1∈J。精確求值：g(1)=−1+1=0，g(0)=0，g(2)=−4+2=−2，右邊 (1/2)·0+(1/2)·(−2)=−1。



S13 · implies操作前

g(1)=0,\ \tfrac12 g(0)+\tfrac12 g(2)=-1

操作後

0>-1;\ g\ \text{is not convex on}\ J

條件：無

規則：exists_intro · 依賴：S11, S12, exists_intro

葉節點依據：exists_intro + order_basics

0>−1，所以這組 x、y、λ 違反 Jensen 不等式。依 ∃ 引入，S11 的存在命題成立，g 在 J 上不是凸函數。一個精確違反就足夠（MKO a2）。



S14 · implies操作前

G_g(x,y,\lambda)

操作後

G_g=-\lambda(1-\lambda)(x-y)^2;\ G_g(0,2,\tfrac12)=-1

條件：無

規則：forall_elim · 依賴：S04, S06, S12, square_nonneg

葉節點依據：forall_elim + square_nonneg + order_basics

交叉核對：g 的 a=−1，依 L_gap，G_g=−λ(1−λ)(x−y)²。在 (0,2,1/2)：−(1/2)(1/2)·4=−1，正好等於 S12 的右邊減 g(z)：−1−0=−1。更一般地，只要 x≠y 且 0<λ<1，G_g<0：每一個非平凡的 Jensen 實例都失敗。



S15 · implies操作前

\lambda\in\{0,1\}\ \text{or}\ x=y

操作後

G_g=0\ \text{(samples pass)},\ \text{yet } g\ \text{not convex}

條件：無

規則：mul_zero · 依賴：S13, S14

葉節點依據：mul_zero + square_nonneg

當 λ=0、λ=1 或 x=y 時，λ(1−λ)(x−y)²=0，所以 g 在這些樣本上 Jensen 都以等號通過。但 S13 已證 g 不凸。因此「若干 Jensen 樣本通過」不能推出凸性；正面結論必須像 S02 至 S08 那樣覆蓋全部 x、y、λ。







## 局部子步與引理

S02.1 · implies操作前

\alpha\le s,\ \alpha\le t,\ \lambda\ge 0,\ 1-\lambda\ge 0

操作後

\alpha=\lambda\alpha+(1-\lambda)\alpha\le\lambda s+(1-\lambda)t

條件：0\le\lambda\le 1

規則：mono_nonneg · 依賴：mono_nonneg, ineq_add, distributive

葉節點依據：mono_nonneg + ineq_add + distributive + order_basics

由 0≤λ≤1 得 λ≥0 與 1−λ≥0。α≤s 乘以 λ 得 λα≤λs，α≤t 乘以 1−λ 得 (1−λ)α≤(1−λ)t；相加得 λα+(1−λ)α≤λs+(1−λ)t，而依分配律左邊等於 (λ+1−λ)α=α。



S02.2 · implies操作前

s\le\beta,\ t\le\beta

操作後

\lambda s+(1-\lambda)t\le\lambda\beta+(1-\lambda)\beta=\beta

條件：0\le\lambda\le 1

規則：mono_nonneg · 依賴：S02.1, mono_nonneg, ineq_add, distributive

葉節點依據：mono_nonneg + ineq_add + distributive

上界同理：s≤β 乘以 λ，t≤β 乘以 1−λ，相加，再用分配律化簡右邊為 β。S02.1 與 S02.2 合起來證得引理 L_interval。



S04.1 · equivalent操作前

\lambda(bx+c)+(1-\lambda)(by+c)-\big(b(\lambda x+(1-\lambda)y)+c\big)

操作後

0

條件：無

規則：distributive · 依賴：distributive

葉節點依據：distributive + add_inverse + mul_one

一次部分：λbx+(1−λ)by−b(λx+(1−λ)y)=0（分配律）。常數部分：λc+(1−λ)c−c=(λ+1−λ)c−c=0。所以 gap 只剩二次部分。



S04.2 · equivalent操作前

(\lambda x+(1-\lambda)y)^2

操作後

\lambda^2x^2+2\lambda(1-\lambda)xy+(1-\lambda)^2y^2

條件：無

規則：distributive · 依賴：distributive, power_laws

葉節點依據：distributive + power_laws + mul_comm

用 (p+q)²=p²+2pq+q²（分配律展開），p=λx、q=(1−λ)y。



S04.3 · equivalent操作前

a\big(\lambda x^2+(1-\lambda)y^2-(\lambda x+(1-\lambda)y)^2\big)

操作後

a\lambda(1-\lambda)(x-y)^2

條件：無

規則：distributive · 依賴：S04.1, S04.2, distributive

葉節點依據：distributive + power_laws + mul_comm + add_comm

代入 S04.2：x² 的係數是 λ−λ²=λ(1−λ)；y² 的係數是 (1−λ)−(1−λ)²=(1−λ)(1−(1−λ))=λ(1−λ)；xy 的係數是 −2λ(1−λ)。提出 λ(1−λ)：λ(1−λ)(x²−2xy+y²)=λ(1−λ)(x−y)²。乘上 a，再加上 S04.1 的 0，得 G_q=aλ(1−λ)(x−y)²。S04.1 至 S04.3 證得引理 L_gap。







## 逐步反向審查


- S15 · premise_audit · S13, S14, mul_zero — 只用乘以零與 S13 的反例；結論是「通過的樣本不足以證凸」，由 g 這個具體反例支持。
- S14 · premise_audit · S04, S12, forall_elim — 這是與 S13 獨立的核對；S13 的結論不依賴本步。「x≠y 且 0<λ<1 時 G_g<0」用到 λ(1−λ)>0 與 (x−y)²>0，兩者在這些條件下成立。
- S13 · premise_audit · S11, S12, exists_intro — 需要見證在範圍內且不等式嚴格反向，兩者都已核對。
- S12 · premise_audit · G3, numeric_evaluation — 精確計算；x、y 確實在 J 中，λ 確實在 [0,1] 中。
- S11 · inverse_equivalence · quantifier_negation, order_basics, L_interval — 量詞否定與序的三分律都是雙向的；J 凸是此等價的前提。
- S10 · premise_audit · S04, S02, forall_elim, forall_intro — 需要 L_gap 與定義域凸。等號成立並不表示仿射以外的函數也取等號。
- S09 · premise_audit · S05, numeric_evaluation — 精確的有理數計算；只說明這一組 x、y、λ，不推出任何全稱結論。
- S08 · premise_audit · S01, S02, S03, S07, forall_intro — 需要兩部分（定義域凸與 Jensen）都已證，以及 x、y、λ 的任意性。
- S07 · premise_audit · S05, S06, square_nonneg, mono_nonneg — 關鍵是 a=2≥0；若 a<0，同一論證給出 gap≤0（見 S14）。不宣稱反向。
- S06 · premise_audit · mono_nonneg, mul_zero — 需要 λ∈[0,1]；λ>1 或 λ<0 時 λ(1−λ)<0，這正是定義限制 λ 範圍的原因。
- S05 · inverse_equivalence · S04, forall_elim — 代入後仍是恆等式，兩邊相等，雙向成立。
- S04.3 · inverse_equivalence · distributive, power_laws, S04.2 — 展開 aλ(1−λ)(x−y)² 即回到左邊；不使用 L_gap 本身。
- S04.2 · inverse_equivalence · distributive, power_laws — 展開與因式分解互逆，雙向成立。
- S04.1 · inverse_equivalence · distributive, add_inverse — 多項式恆等式，雙向成立。
- S04 · inverse_equivalence · L_gap — 這是多項式恆等式，兩邊是同一個多項式，雙向成立，沒有附加條件。
- S03 · inverse_equivalence · order_basics, def_intro — 同減 f(z) 與同加 f(z) 互逆，兩者都保持不等號方向，雙向成立。
- S02.2 · premise_audit · mono_nonneg, ineq_add, distributive — 與 S02.1 對稱；不使用 L_interval 本身。
- S02.1 · premise_audit · mono_nonneg, ineq_add, distributive — 需要兩個權重非負；證明 L_interval 的下界，沒有使用 L_interval 本身。
- S02 · premise_audit · L_interval, mko_cvxset — 需要 x、y 在區間內與 λ∈[0,1]；不宣稱反向。
- S01 · inverse_equivalence · mko_cvxf, def_unfold — 展開與收回定義互逆，雙向成立。





## 錯誤控制與反例

幾個 Jensen 樣本通過不證凸MKO 指出的誤解是由幾個 Jensen 樣本通過就宣稱全域凸。g 在 λ=0、λ=1 與 x=y 的所有樣本上都通過（S15），卻不是凸函數。S09 對 f 的實例同樣只是例示；f 的凸性來自 S04 至 S08 對全部 x、y、λ 的恆等式與符號論證。

定義域必須凸MKO 的另一個誤解是在非凸定義域上談一般凸函數。若定義域是 D=[0,1]∪[2,3]，x=1、y=2、λ=1/2 給出 3/2∉D，函數在 3/2 沒有值，Jensen 不等式根本無法陳述。所以 S02 先證 I 是凸的，S11 也先確認 J 是凸的。

a 的正負決定 gap 的正負依 L_gap，二次函數的 Jensen gap 是 aλ(1−λ)(x−y)²。a=2 時 gap≥0（凸），a=0 時 gap=0（仿射，取等號），a=−1 時 gap≤0，而且 x≠y、0<λ<1 時嚴格小於 0（不凸）。「二次函數都是凸的」是錯的。


- g 在 λ=0、λ=1 與 x=y 的樣本上都滿足 Jensen，所以 g 在 [0,2] 上凸 → reject — x=0、y=2、λ=1/2：g(1)=0>−1。
- f 在 x=−1、y=4、λ=1/5 的 Jensen 實例通過，這就證明 f 在 I 上凸 → reject — 單一通過實例不能證凸（MKO a2）；結論成立是因為 S04 至 S08 覆蓋全部 x、y、λ。
- x² 在 D=[0,1]∪[2,3] 上是 MKO 意義下的凸函數 → reject — D 不是凸集合：1、2∈D 但 (1/2)·1+(1/2)·2=3/2∉D；定義要求凸定義域。
- 每個二次函數都是凸函數 → reject — g(x)=−x²+x 的 a=−1，在 x=0、y=2、λ=1/2 違反 Jensen。





## 結論與限制

I=[−1,4] 是凸集合，且對所有 x,y∈I、λ∈[0,1]，f(x)=2x²−3x+1 的 Jensen gap 等於 2λ(1−λ)(x−y)²≥0，所以 f 在 I 上是凸函數。ℓ(x)=3x−5 的 gap 恆為 0，Jensen 取等號。g(x)=−x²+x 在 J=[0,2] 上不凸：x=0、y=2、λ=1/2 時 g(1)=0>−1=(1/2)g(0)+(1/2)g(2)。


- mono_nonneg 與 ineq_add 是本稿的前提，不在本稿中由實數公理推出（mono_nonneg 在凸集合教學稿中以引理證明）。
- N7 至 N10 只核 S09 的一個實例；它們是例示，證明不依賴它們。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 3f396010579d87300f52e4a41245fcd8d02d372b3712f863225c958c4632db0c
- original source SHA-256: 3f396010579d87300f52e4a41245fcd8d02d372b3712f863225c958c4632db0c
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-convex-function-01.json)