複數模與共軛：證明 z·z̄=|z|² 與共軛保持運算

目標與範圍

對 z=a+bi、w=c+di（a、b、c、d 為實數）證明：（一）z·z̄=(a²+b²)+0i，即模平方的實數嵌入；（二）共軛保持加法：(z+w)‾=z̄+w̄；（三）共軛保持乘法：(zw)‾=z̄·w̄；（四）由此得 |zw|²=|z|²|w|²。再以 z=3−4i、w=1+2i 精確核對，並區分模平方與模。

一般證明對實數分量成立；例子用整數有序對（MKO 假設 a1），只算共軛與模平方，不以小數平方根近似冒充精確模。僅在 |z|²=25 為完全平方數時說明 |z|=5。不處理 argument、極式或複可微性（MKO 假設 a2）；不改動 canonical MKO 或英文 edition。

已知條件與符號

• mul_assoc
• mul_comm
• neg_mul
• square_nonneg
• numeric_evaluation

• G1 — 一般情形：z=a+bi 對應 (a,b)，w=c+di 對應 (c,d)，a、b、c、d 為實數。
• G2 — 例子：z=3−4i 對應 (3,−4)，w=1+2i 對應 (1,2)。
• G3 — 答案以精確整數或有序對表示；非完全平方數的模平方保持原樣，不寫小數近似（MKO 假設 a1）。

• z=a+bi\leftrightarrow(a,b) — 複數與其有序對
• \overline{z}=a-bi — z 的共軛
• |z|^2=a^2+b^2 — z 的模平方
• |z|=\sqrt{a^2+b^2} — z 的模（非負平方根）
• w=c+di — 第二個複數

規則與來源

• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
• square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
• 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。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• sqrt_def · prerequisite — 主平方根：對 a≥0，√a 是唯一滿足 b≥0 且 b²=a 的實數 b。負數在實數中沒有平方根。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• mko_modconj_def · cited — 對 z=a+bi，共軛為 a−bi，模平方為 a²+b²，且 z 乘共軛等於模平方的實數嵌入。共軛保持加法與乘法。 · mko-complex-modulus-conjugate
• complex_mul_formula · cited — 複數乘法由分配律與 i²=−1 導出：(a+bi)(c+di) 的實部為 ac−bd，虛部係數為 ad+bc。 · mko-complex-number
• complex_addsub · prerequisite — 逐分量加減：(a+bi)±(c+di)=(a±c)+(b±d)i。
• complex_pair_eq · prerequisite — 對實數 a、b、c、d：a+bi=c+di 當且僅當 a=c 且 b=d。
• real_embedding · prerequisite — 實數 r 嵌入為 r+0i，即有序對 (r,0)；兩個嵌入實數的乘積 (r,0)(s,0)=(rs,0)。
• modulus_def · prerequisite — 模 |z| 是模平方 a²+b² 的非負平方根：|z|=√(a²+b²)。
• L_conj_mul · lemma — 對所有複數 z、w：(zw)‾=z̄·w̄。
• L_modsq_mul · lemma — 對所有複數 z、w：|zw|²=|z|²·|w|²。

逐步主鏈

z=a+bi\leftrightarrow(a,b)

\overline{z}=a-bi\leftrightarrow(a,-b),\ |z|^2=a^2+b^2

z\overline{z}=(a,b)\cdot(a,-b)

(a^2+b^2,\,0)

z\overline{z}=(a^2+b^2,\,0)

z\overline{z}=|z|^2\in\mathbb{R},\ |z|^2\ge 0

\overline{z+w}=\overline{(a+c)+(b+d)i}

(a+c)-(b+d)i=(a-bi)+(c-di)=\overline{z}+\overline{w}

\overline{zw}

\overline{z}\cdot\overline{w}

|zw|^2

|z|^2\,|w|^2

z=3-4i\leftrightarrow(3,-4)

\overline{z}=3+4i\leftrightarrow(3,4)

|z|^2=3^2+(-4)^2,\ z\overline{z}=(3,-4)(3,4)

|z|^2=25,\ z\overline{z}=(3\cdot3-(-4)\cdot4,\,3\cdot4+(-4)\cdot3)=(25,0)

|z|^2=25

|z|=\sqrt{25}=5\neq 25

w=1+2i

\overline{w}=1-2i,\ |w|^2=5,\ |w|=\sqrt5\notin\mathbb{Z}

zw=(3,-4)(1,2)

(3\cdot1-(-4)\cdot2,\,3\cdot2+(-4)\cdot1)=(11,2)

\overline{zw}\ \text{vs}\ \overline{z}\,\overline{w}=(3,4)(1,-2)

(11,-2)=(3\cdot1-4\cdot(-2),\,3\cdot(-2)+4\cdot1)

|zw|^2=11^2+2^2

125=25\cdot5=|z|^2|w|^2

\overline{z+w}=\overline{(4,-2)}

(4,2)=(3,4)+(1,-2)=\overline{z}+\overline{w}

z=a+bi,\ w=c+di

z\overline{z}=(|z|^2,0),\ \overline{z+w}=\overline{z}+\overline{w},\ \overline{zw}=\overline{z}\,\overline{w},\ |zw|^2=|z|^2|w|^2

局部子步與引理

\operatorname{Re}(z\overline{z})=a\cdot a-b\cdot(-b)

a^2+b^2

\operatorname{Im}(z\overline{z})=a\cdot(-b)+b\cdot a

0

\overline{zw}=\overline{(ac-bd)+(ad+bc)i}

(ac-bd,\,-(ad+bc))

\overline{z}\cdot\overline{w}=(a,-b)\cdot(c,-d)

(ac-(-b)(-d),\,a(-d)+(-b)c)=(ac-bd,\,-(ad+bc))

(|zw|^2,0)=(zw)\,\overline{zw}

(zw)(\overline{z}\,\overline{w})=(z\overline{z})(w\overline{w})

(z\overline{z})(w\overline{w})=(|z|^2,0)(|w|^2,0)

(|z|^2|w|^2,\,0)\ \Rightarrow\ |zw|^2=|z|^2|w|^2

逐步反向審查

• S15 · sufficient_goal_reduction · S03, S04, S05, S06, and_intro_elim — 目標 G：四個一般命題。足夠條件 H：S03、S04、S05、S06 各自已對任意 a、b、c、d 證明；H⇒G 由合取引入。沒有把 G 當作前提，也沒有用例子代替證明。
• S14 · premise_audit · S04, complex_addsub, numeric_evaluation — 實例核對，一般結論來自 S04。
• S13 · premise_audit · L_modsq_mul, numeric_evaluation — 實例只核對計算（N17）；一般結論來自 S06。
• S12 · premise_audit · S05, complex_mul_formula, numeric_evaluation — 實例只核對計算（N15、N16），一般結論來自 S05。
• S11 · inverse_equivalence · complex_mul_formula, numeric_evaluation — 公式的精確求值（N13、N14），兩邊同一個數。
• S10 · premise_audit · mko_modconj_def, order_basics, numeric_evaluation — 非完全平方的論證只分 n≤2 與 n≥3 兩種情形並涵蓋所有非負整數；本稿不宣稱 √5 的其他性質。
• S09 · premise_audit · modulus_def, sqrt_def, numeric_evaluation — 需要 25 是完全平方數，才能寫出精確整數 5；對 w 不成立（S10）。
• S08 · premise_audit · S02, complex_mul_formula, numeric_evaluation — 這是一般定理的一個實例（N6 到 N8），用來核對計算，不取代 S02 的證明。
• S07 · inverse_equivalence · mko_modconj_def — 共軛兩次回到原數：(3,4) 的共軛是 (3,−4)=z。
• S06.2 · premise_audit · S03, real_embedding, complex_pair_eq — 比較實部用到有序對相等；此步只取等式的實部，不宣稱其他推論。
• S06.1 · inverse_equivalence · S03, S05, mul_assoc, mul_comm — 等值代換與重排都是等式，反向依序還原。
• S06 · inverse_equivalence · L_modsq_mul — 兩邊是同一個實數，雙向成立。
• S05.2 · inverse_equivalence · neg_mul, complex_pair_eq, distributive — 符號規則與分配律都是恆等式（N3、N4 以多項式格點核對），雙向成立。
• S05.1 · inverse_equivalence · complex_mul_formula, mko_modconj_def — 公式與共軛定義都是等式；再取一次共軛即回到 zw。
• S05 · inverse_equivalence · L_conj_mul — 引理是等式，兩邊是同一個複數，雙向成立。
• S04 · inverse_equivalence · complex_addsub, complex_pair_eq, neg_mul — 每個等號都是恆等改寫（−(b+d)=−b−d），兩個分量相等，雙向成立。
• S03 · premise_audit · S02, real_embedding, square_nonneg — 非負性用到平方非負；此步不宣稱每個非負實數都是某個整數對的模平方。
• S02.2 · inverse_equivalence · mul_comm, neg_mul, add_inverse — 恆等式（N2），雙向成立。
• S02.1 · inverse_equivalence · neg_mul, add_inverse — 對所有實數成立的恆等式（N1 以多項式格點核對），雙向成立。
• S02 · inverse_equivalence · complex_mul_formula, complex_pair_eq — 公式是等式，兩個分量分別相等即有序對相等，雙向成立。
• S01 · premise_audit · G1, mko_modconj_def — 此步只寫出定義，不推出新事實。

錯誤控制與反例

共軛只改虛部的符號

MKO 指出的誤解之一是只改實部符號。3−4i 的共軛是 3+4i；寫成 −3−4i 改錯了分量，寫成 −3+4i 則是 −z 而非 z̄。

分清模平方與模

MKO 的另一個誤解是把模平方當成模。|3−4i|²=25 而 |3−4i|=5；|1+2i|²=5 而 |1+2i|=√5 不是整數。寫成 2.236 只是近似：2.236²=4.999696≠5（N18）。本稿依 MKO 保留精確的模平方。

z·z̄ 的實部是 a²+b²，不是 a²−b²

套用平方差 (a+bi)(a−bi)=a²−(bi)² 時，最容易漏掉 (bi)²=b²i²=−b²，於是誤得 a²−b²；對 z=3−4i 會得 9−16=−7。S02.1 顯示正號來自 −b·(−b)=+b²。

• 3−4i 的共軛是 −3−4i → reject — 共軛只改虛部係數的符號：3+4i。
• |3−4i|=25 → reject — 25 是模平方；模是 √25=5。
• |1+2i|=2.236 是精確值 → reject — 2.236²=4.999696≠5；精確的模平方是 5，模是 √5。
• (3−4i)(3+4i)=9−16=−7 → reject — i²=−1 使結果為 9+16=25，且 z·z̄ 恆非負。

結論與限制

對所有實數 a、b、c、d：z·z̄=(a²+b²)+0i 是模平方的實數嵌入且非負；共軛保持加法與乘法；|zw|²=|z|²|w|²。例子 z=3−4i、w=1+2i：z̄=3+4i，|z|²=25，z·z̄=(25,0)，|z|=5（與模平方 25 不同）；w̄=1−2i，|w|²=5（|w|=√5 不是整數，保持精確模平方）；zw=11+2i，(zw)‾=11−2i=z̄·w̄，|zw|²=125=25·5。

• ℂ 中乘法的結合與交換律（S06.1 使用）是前提，沒有在本稿由有序對定義推出；本稿不處理複數除法、argument 與極式（MKO 的 formal next）。
• N1 到 N5 是多項式恆等式的格點核對，屬交叉核對；一般結論由 S02 到 S06 的代數論證證明。

驗證及來源綁定

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

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

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