# 角：對頂角相等的逐步證明 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-angle/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-angle-01 · production-20261019-adopted-96 ## 目標與範圍 直線 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。 ## 逐步主鏈 S01 · definition操作前 \angle AOC,\ \angle COB,\ \angle BOD,\ \angle DOA 操作後 \alpha=m\angle AOC,\ \beta=m\angle COB,\ \gamma=m\angle BOD,\ \delta=m\angle DOA 條件：無 規則：def_intro · 依賴：G1, G2 葉節點依據：def_intro + mko_angle_def 為四個以 O 為頂點的角的度數取名。依 MKO，角的大小是兩邊之間的張開量，與射線畫多長無關。∠AOC 與 ∠BOD 是一組對頂角（OA 與 OB 方向相反，OC 與 OD 方向相反），∠COB 與 ∠DOA 是另一組。 S02 · theorem_application操作前 A\text{-}O\text{-}B,\ C\notin\overleftrightarrow{AB} 操作後 \alpha+\beta=180 條件：O\ \text{between}\ A,B; C\notin\overleftrightarrow{AB} 規則：linear_pair · 依賴：S01, G2 葉節點依據：linear_pair 對直線 AB 與點 C 使用線性對公設（X=C）：m∠AOC+m∠COB=180°，即 α+β=180。公設的兩個前提「O 在 A、B 之間」與「C 不在直線 AB 上」都由 G2 提供。 S03 · theorem_application操作前 C\text{-}O\text{-}D,\ B\notin\overleftrightarrow{CD} 操作後 \beta+\gamma=180 條件：O\ \text{between}\ C,D; B\notin\overleftrightarrow{CD} 規則：linear_pair · 依賴：S01, G2 葉節點依據：linear_pair + angle_symmetric 對直線 CD 與點 B 使用線性對公設（公設中的 A、B 換成 C、D，X=B）：m∠COB+m∠BOD=180°，即 β+γ=180。 S04 · implies操作前 \alpha+\beta=180,\ \beta+\gamma=180 操作後 \alpha+\beta=\gamma+\beta 條件：無 規則：eq_refl_symm_trans · 依賴：S02, S03 葉節點依據：eq_refl_symm_trans + add_comm 兩式右邊都是 180，依等號的對稱與傳遞得 α+β=β+γ；再依加法交換律寫成 α+β=γ+β，讓相同的一項 β 位於兩邊同一位置。 S05 · equivalent操作前 \alpha+\beta=\gamma+\beta 操作後 \alpha=\gamma 條件：無 規則：L_cancel · 依賴：S04 葉節點依據：eq_congruence + add_assoc + add_inverse + add_zero 依引理 L_cancel（u=α、v=γ、w=β）消去兩邊的 β，得 α=γ，即 m∠AOC=m∠BOD。 S06 · theorem_application操作前 A\text{-}O\text{-}B,\ D\notin\overleftrightarrow{AB} 操作後 \delta+\gamma=180 條件：O\ \text{between}\ A,B; D\notin\overleftrightarrow{AB} 規則：linear_pair · 依賴：S01, G2 葉節點依據：linear_pair + angle_symmetric 對直線 AB 與點 D 使用線性對公設（X=D）：m∠AOD+m∠DOB=180°。依 angle_symmetric，m∠AOD=m∠DOA=δ，m∠DOB=m∠BOD=γ，所以 δ+γ=180。 S07 · implies操作前 \beta+\gamma=180,\ \delta+\gamma=180 操作後 \beta+\gamma=\delta+\gamma 條件：無 規則：eq_refl_symm_trans · 依賴：S03, S06 葉節點依據：eq_refl_symm_trans 兩式右邊都是 180，依等號的對稱與傳遞得 β+γ=δ+γ。 S08 · equivalent操作前 \beta+\gamma=\delta+\gamma 操作後 \beta=\delta 條件：無 規則：L_cancel · 依賴：S07 葉節點依據：eq_congruence + add_assoc + add_inverse + add_zero 依引理 L_cancel（w=γ）消去 γ，得 β=δ，即 m∠COB=m∠DOA。 S09 · implies操作前 \alpha=\gamma,\ \beta=\delta 操作後 m\angle AOC=m\angle BOD,\ m\angle COB=m\angle DOA 條件：無 規則：def_unfold · 依賴：S05, S08 葉節點依據：def_unfold + and_intro_elim 把名稱展開回角：兩組對頂角分別相等。證明沒有用到任何具體度數或圖形量測，所以對每個滿足 G2 的位置都成立。 S10 · implies操作前 \alpha=35 操作後 \beta=145,\ \gamma=35,\ \delta=145 條件：無 規則：eq_congruence · 依賴：G3, S02, S05, S08 葉節點依據：eq_congruence + eq_replace + numeric_evaluation 代入 α=35：由 S02，β=180−35=145；由 S05，γ=α=35；由 S08，δ=β=145。核對：35+145=180。 ## 局部子步與引理 S05.1 · equivalent操作前 u+w=v+w 操作後 (u+w)+(-w)=(v+w)+(-w) 條件：無 規則：eq_congruence · 依賴：eq_congruence 葉節點依據：eq_congruence + add_inverse 兩邊同加 −w。反向是兩邊同加 w，再用 S05.2 的化簡。 S05.2 · equivalent操作前 (u+w)+(-w)=(v+w)+(-w) 操作後 u=v 條件：無 規則：eq_replace · 依賴：S05.1 葉節點依據：add_assoc + add_inverse + add_zero 化簡左邊：(u+w)+(−w)=u+(w+(−w))=u+0=u；右邊同理得 v。S05.1 與 S05.2 合起來證得引理 L_cancel。 ## 逐步反向審查 - 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、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-angle-01.json)