角：對頂角相等的逐步證明

目標與範圍

直線 AB 與直線 CD 是兩條相異直線，相交於 O，且 O 在 A、B 之間，也在 C、D 之間。證明對頂角相等：m∠AOC=m∠BOD 且 m∠COB=m∠DOA；再以 m∠AOC=35° 為例算出四個角。

在 MKO 的範圍內工作：初等平面歐幾里得幾何、度數量值、0° 到 180° 的非定向角。以線性對公設為前提證明對頂角定理；不推導角度公設本身，不處理定向角或弧度；不改動 canonical MKO 或英文 edition。

已知條件與符號

• eq_refl_symm_trans
• eq_congruence
• add_inverse
• numeric_evaluation

• G1 — 初等平面歐幾里得幾何；角以度數量測，非定向，取值在 0° 到 180°（MKO 假設 a1）。
• G2 — 直線 AB 與直線 CD 相異，相交於 O；O 在 A、B 之間，也在 C、D 之間。因兩直線只交於 O，C、D 不在直線 AB 上，A、B 不在直線 CD 上。
• G3 — 例子：m∠AOC=35°。

• m\angle AOC — 角 AOC 的度數
• \alpha,\beta,\gamma,\delta — 四個角的度數名稱
• O — 交點，四個角的共同頂點
• A\text{-}O\text{-}B — O 在 A 與 B 之間，三點共線
• \overleftrightarrow{AB} — 通過 A、B 的直線

規則與來源

• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(v)。只對一邊做運算不屬於此規則。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• add_comm · prerequisite — 加法交換律：u+v=v+u。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• add_zero · prerequisite — 加法單位元：u+0=u。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_angle_def · cited — 兩條具有共同端點的射線形成一個角；共同端點稱為頂點，兩條射線稱為角的邊，本物件以度數表示 0° 到 180° 的非定向角。 · mko-angle
• linear_pair · prerequisite — 線性對公設：若 O 在 A、B 之間，且點 X 不在直線 AB 上，則 m∠AOX+m∠XOB=180°。
• angle_symmetric · prerequisite — 非定向角的度數與兩邊的書寫順序無關：m∠XOY=m∠YOX。
• L_cancel · lemma — 對實數 u、v、w：u+w=v+w ⇔ u=v。

逐步主鏈

\angle AOC,\ \angle COB,\ \angle BOD,\ \angle DOA

\alpha=m\angle AOC,\ \beta=m\angle COB,\ \gamma=m\angle BOD,\ \delta=m\angle DOA

A\text{-}O\text{-}B,\ C\notin\overleftrightarrow{AB}

\alpha+\beta=180

C\text{-}O\text{-}D,\ B\notin\overleftrightarrow{CD}

\beta+\gamma=180

\alpha+\beta=180,\ \beta+\gamma=180

\alpha+\beta=\gamma+\beta

\alpha+\beta=\gamma+\beta

\alpha=\gamma

A\text{-}O\text{-}B,\ D\notin\overleftrightarrow{AB}

\delta+\gamma=180

\beta+\gamma=180,\ \delta+\gamma=180

\beta+\gamma=\delta+\gamma

\beta+\gamma=\delta+\gamma

\beta=\delta

\alpha=\gamma,\ \beta=\delta

m\angle AOC=m\angle BOD,\ m\angle COB=m\angle DOA

\alpha=35

\beta=145,\ \gamma=35,\ \delta=145

局部子步與引理

u+w=v+w

(u+w)+(-w)=(v+w)+(-w)

(u+w)+(-w)=(v+w)+(-w)

u=v

逐步反向審查

• S10 · premise_audit · G3, S02, S05, S08 — 這只是一個例子的計算，可以重算（N1、N2），但不能取代 S02 到 S09 的一般證明。
• S09 · sufficient_goal_reduction · S05, S08, def_unfold — 目標 G：兩組對頂角相等。足夠條件 H：α=γ 且 β=δ；H⇒G 由 S01 的命名。H 由 S05、S08 從 G2 與公設正向證成，沒有把 G 當作前提。
• S08 · inverse_equivalence · L_cancel — 反向：兩邊同加 γ；引理兩向都已證。
• S07 · premise_audit · S03, S06, eq_refl_symm_trans — 與 S04 相同，只用兩個等式，不宣稱反向。
• S06 · premise_audit · G2, linear_pair, angle_symmetric — 需要 O 在 A、B 之間，且 D 不在直線 AB 上，兩者都由 G2 給出；改寫角名稱只用到非定向角與書寫順序無關。
• S05.2 · inverse_equivalence · add_assoc, add_inverse, add_zero — 所用的是對所有實數成立的恆等式，換掉相等的式子不改變等式的真假，雙向成立。
• S05.1 · inverse_equivalence · eq_congruence, add_inverse — 加 −w 與加 w 互為反運算，對任何實數 w 都可做。
• S05 · inverse_equivalence · L_cancel — 反向：兩邊同加 β 回到 α+β=γ+β；引理的兩個方向都已在子步證明。
• S04 · premise_audit · S02, S03, eq_refl_symm_trans — 只需兩個等式；不宣稱反向，即不由 α+β=γ+β 推回兩者各自等於 180。
• S03 · premise_audit · G2, linear_pair — O 在 C、D 之間，且 B 不在直線 CD 上（兩直線相異、只交於 O），都由 G2 給出。
• S02 · premise_audit · G2, linear_pair — 公設要求 A、O、B 共線且 O 在中間，以及 C 不在該直線上；兩者都在 G2 中明示。只憑兩角「相鄰」不足以推出和為 180°。
• S01 · premise_audit · G1, G2, def_intro, mko_angle_def — 此步只取名，不推出新事實。四個角都有定義：例如 C 不在直線 AB 上，所以 OA 與 OC 不共線，∠AOC 是真正的角。

錯誤控制與反例

量圖不是證明

MKO 指出常見誤解是由示意圖外觀猜角度。在一張圖上量得 ∠AOC 與 ∠BOD 看起來相等，只支持那張圖，而且量角器有誤差；本稿的證明只用 G2 的位置關係與線性對公設，適用於所有滿足 G2 的位置。

相鄰角不一定互補

線性對公設需要 A、O、B 共線且 O 在中間。若從 O 出發的三條射線方向是 0°、50°、120°，相鄰的兩個角是 50° 與 70°，和為 120°，不是 180°。所以 S02、S03、S06 都必須引用 G2 的「O 在兩點之間」。

互補不必相鄰

MKO 說明互補只依量值和為 180°，不要求兩角在圖上相鄰。本證明用的是線性對這個特殊的相鄰情況來得到互補；反過來，互補的兩角不必構成線性對。

• ∠AOC 與 ∠COB 有共同邊 OC，所以 m∠AOC+m∠COB=180° → reject — 還需要 A、O、B 共線且 O 在中間；三射線方向 0°、50°、120° 給出 50°+70°=120°。
• 對頂角相等，所以相鄰的兩角也相等 → reject — α=35 時 β=145，相鄰兩角不等。
• 互補的兩角必須在圖上相鄰 → reject — 30° 與 150° 可在不同圖形中，量值和為 180° 即互補（MKO）。
• 在圖上量得 ∠AOC 約等於 ∠BOD，所以對頂角相等得證 → reject — 一次量測只支持那張圖並帶有誤差，不涵蓋所有位置。

結論與限制

在 G2 的設定下，m∠AOC=m∠BOD 且 m∠COB=m∠DOA：對頂角相等。若 m∠AOC=35°，四個角依序為 35°、145°、35°、145°。

• 線性對公設與 angle_symmetric 是本稿的前提，不在本稿中由更基本的公理推出。

驗證及來源綁定

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

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

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