實數的通常順序：加法保序、正分母交叉比較、有限極值與閉區間

目標與範圍

證明對所有實數 a、b、c：a<b ⇔ a+c<b+c；q、s>0 時 p/q<r/s ⇔ ps<rq；非空有限實數集合有最小元素，且最小元素唯一。據此比較 M={−5/9, 1/3, −7/12, −1/2}（照此次序列出）的元素，求 M 的最小與最大元素，並判定兩端點與 1/2 是否屬於閉區間 [min M, max M]。

只談實數的通常全序（MKO a1），以 order_basics 中的順序公理為前提，不構造實數。比較題使用正分母有理數（a2）；極值只對非空有限集合，閉區間要求下界不大於上界（a3）。最大元素的存在以「同一論證把 ≤ 換成 ≥」帶過。不處理複數、一般偏序或無限集合的上確界；不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• frac_rules
• add_inverse
• nat_induction
• numeric_evaluation

• G1 — ℝ 上的通常順序 ≤ 自反、反對稱、傳遞，且任兩數可比較；a<b 表示 a≤b 且 a≠b。
• G2 — M={−5/9, 1/3, −7/12, −1/2}，依此次序列出；寫成正分母形式：(−5)/9、1/3、(−7)/12、(−1)/2。
• G3 — 定義：m 是集合 M 的最小元素，指 m∈M 且對所有 x∈M 有 m≤x；最大元素同理以 ≥。對 l≤u，閉區間 [l,u]={x∈ℝ ∣ l≤x 且 x≤u}。

• a\le b,\ a<b — 通常順序與嚴格順序
• \frac{p}{q} — 有理數，分母 q>0
• M — 待比較的有限集合
• \min M,\ \max M — 最小與最大元素
• [l,u] — 閉區間 {x ∣ l≤x≤u}

規則與來源

• 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。
• frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
• add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。
• nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。
• add_zero · prerequisite — 加法單位元：u+0=u。
• mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
• logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_order · cited — 實數的通常順序 ≤ 滿足自反、反對稱、傳遞及任兩數可比較；a<b 表示 a≤b 且 a≠b。任意實數 a、b、c 都有 a<b 當且僅當 a+c<b+c。非空有限實數集合有最小與最大元素；閉區間 [l,u]（l≤u）包含兩端點。 · mko-order-relation
• min_max_def · prerequisite — 最小元素：m∈M 且 ∀x∈M, m≤x；最大元素：m∈M 且 ∀x∈M, m≥x。
• interval_def · prerequisite — 閉區間：對 l≤u，x∈[l,u] ⇔ l≤x 且 x≤u。
• L_translate · lemma — 對所有實數 a、b、c：a<b ⇔ a+c<b+c。
• L_cross · lemma — 對實數 p、r 與 q>0、s>0：p/q<r/s ⇔ ps<rq。
• L_finite_min · lemma — 每個非空有限實數集合都有最小元素。
• L_min_unique · lemma — 一個實數集合至多有一個最小元素（最大元素同理）。

逐步主鏈

a,b\in\mathbb{R}

a<b\ :\iff\ a\le b\land a\neq b;\ \text{exactly one of}\ a<b,\ a=b,\ b<a

a<b

a+c<b+c

\frac{p}{q}<\frac{r}{s}

ps<rq

-\tfrac{7}{12}\ ?\ -\tfrac{5}{9}

(-7)\cdot9=-63<-60=(-5)\cdot12\ \Rightarrow\ -\tfrac{7}{12}<-\tfrac{5}{9}

-\tfrac{5}{9}\ ?\ -\tfrac{1}{2}

(-5)\cdot2=-10<-9=(-1)\cdot9\ \Rightarrow\ -\tfrac{5}{9}<-\tfrac{1}{2}

-\tfrac{1}{2}\ ?\ \tfrac{1}{3}

(-1)\cdot3=-3<2=1\cdot2\ \Rightarrow\ -\tfrac{1}{2}<\tfrac{1}{3}

-\tfrac{7}{12}<-\tfrac{5}{9},\ -\tfrac{5}{9}<-\tfrac{1}{2},\ -\tfrac{1}{2}<\tfrac{1}{3}

-\tfrac{7}{12}<-\tfrac{5}{9}<-\tfrac{1}{2}<\tfrac{1}{3}

M\subseteq\mathbb{R}\ \text{finite},\ M\neq\varnothing

M\ \text{has a minimum}

-\tfrac{7}{12}\in M,\ -\tfrac{7}{12}\le x\ \forall x\in M

\min M=-\tfrac{7}{12}

\tfrac{1}{3}\in M,\ \tfrac{1}{3}\ge x\ \forall x\in M

\max M=\tfrac{1}{3}

m,m'\ \text{both minima of}\ M

m=m'

l=-\tfrac{7}{12},\ u=\tfrac{1}{3}

l\le u

l\le l\le u,\ l\le u\le u

l\in[l,u],\ u\in[l,u],\ M\subseteq[l,u]

\tfrac{1}{3}<\tfrac{1}{2}\ \ (1\cdot2<1\cdot3)

\tfrac12\notin[l,u]

-\tfrac{7}{12}<-\tfrac{5}{9}

-\tfrac{7}{12}+\tfrac{7}{12}<-\tfrac{5}{9}+\tfrac{7}{12},\ \text{i.e.}\ 0<\tfrac{1}{36}

\text{S02 to S15}

\min M=-\tfrac{7}{12},\ \max M=\tfrac13,\ l,u\in[l,u],\ \tfrac12\notin[l,u]

局部子步與引理

a<b

a+c<b+c

a+c<b+c

(a+c)+(-c)<(b+c)+(-c),\ \text{i.e.}\ a<b

q>0,\ s>0

qs>0,\ \tfrac{1}{qs}>0

\frac{p}{q}<\frac{r}{s}

\frac{p}{q}\cdot qs<\frac{r}{s}\cdot qs,\ \text{i.e.}\ ps<rq

ps<rq

\frac{ps}{qs}<\frac{rq}{qs},\ \text{i.e.}\ \frac{p}{q}<\frac{r}{s}

M=\{a\}

\min M=a

|M|=n+1,\ a\in M,\ m'=\min(M\setminus\{a\})

\min M=m'\ \text{if}\ m'\le a,\ \ \min M=a\ \text{if}\ a<m'

m,m'\in M,\ m\le x,\ m'\le x\ \forall x\in M

m\le m',\ m'\le m\ \Rightarrow\ m=m'

逐步反向審查

• S16 · sufficient_goal_reduction · S02, S03, S08, S09, S10, S11, S13, S14, and_intro_elim — 目標 G 為 goal 中的證明與判定；足夠條件 H 為各步結論的合取，皆已正向證成，H⇒G 只用合取引入。
• S15 · inverse_equivalence · L_translate, frac_rules, numeric_evaluation — L_translate 是等價，兩邊同加 7/12 或同減 7/12 互為反向。
• S14 · premise_audit · L_cross, interval_def, contradiction — 成員條件是兩個不等式的合取，否定其中一個就足以排除。
• S13 · premise_audit · interval_def, S12, mko_order — 端點屬於閉區間只用到自反性與 l≤u；開區間是另一個物件，不在此討論。
• S12 · premise_audit · S07, order_basics — 由 l<u 得 l≤u 是嚴格順序的定義。
• S11.1 · premise_audit · min_max_def, mko_order — 只用到兩個最小元素都屬於 M 以及反對稱性。
• S11 · premise_audit · L_min_unique — 唯一性依賴反對稱性。
• S10 · premise_audit · S07, min_max_def — 與 S09 對稱。
• S09 · premise_audit · S07, min_max_def, order_basics — 兩個條件（屬於 M、不大於每個元素）都已檢查；由 x<y 得 x≤y 是嚴格順序的定義。
• S08.2 · premise_audit · nat_induction, case_analysis, order_basics, min_max_def — 需要 n≥1 使 M′ 非空，歸納假設才適用；兩個情形由全序性窮盡。
• S08.1 · premise_audit · min_max_def, order_basics — 只用到自反性；單元素集合的兩個極值相同。
• S08 · premise_audit · L_finite_min — 非空是必要的：歸納從 n=1 開始，空集合不在範圍內，也沒有最小元素。
• S07 · premise_audit · S04, S05, S06, order_basics — 需要的是三個相鄰比較與傳遞性；不需要再做其餘三對的交叉相乘。
• S06 · inverse_equivalence · L_cross, numeric_evaluation — 同 S04，分母為正，等價成立。
• S05 · inverse_equivalence · L_cross, numeric_evaluation — 同 S04，分母為正，等價成立。
• S04 · inverse_equivalence · L_cross, numeric_evaluation — L_cross 是等價，條件 12、9>0 成立，所以分數比較與整數比較同真同假。
• S03.3 · premise_audit · S03.1, order_basics, frac_rules — 需要 1/(qs)>0，由 S03.1 提供。
• S03.2 · premise_audit · S03.1, order_basics, frac_rules — 需要 qs>0；若 qs<0，乘法會使不等號反向。
• S03.1 · premise_audit · order_basics, mul_inverse_nonzero, contradiction — 兩個正數的積為正，正數的倒數為正；兩者都依賴 q、s>0。
• S03 · inverse_equivalence · L_cross — ⇒ 與 ⇐ 分別在子步中證明，條件 q、s>0 兩個方向都要用。
• S02.2 · premise_audit · order_basics, add_assoc, add_inverse, add_zero — 每個實數 c 都有加法反元素 −c，所以這個方向不需附加條件。
• S02.1 · premise_audit · order_basics — 直接套用公理，對任何實數 c 成立。
• S02 · inverse_equivalence · L_translate — 兩個方向都有證明，所以是等價。
• S01 · premise_audit · G1, mko_order, order_basics — 只是定義與公理的重述；三分律在 order_basics 中也列為前提。

錯誤控制與反例

交叉相乘前分母須為正

MKO 的誤解之一是忽略分母正負。比較 1/(−2) 與 1/3 時直接交叉相乘得 1·3=3>−2=1·(−2)，會誤判 1/(−2)>1/3；實際上 1/(−2)=−1/2<1/3。原因是乘上負數 (−2)·3 使不等號反向。先寫成正分母 (−1)/2 再比較：(−1)·3=−3<2，結論正確。

閉區間包含端點

另一個誤解是漏掉閉區間的端點。l≤l≤u 成立，所以 l∈[l,u]（S13）。l=u 時 [l,u] 只含一個值，例如 [2,2]={2}；不含端點的是開區間，那是另一個物件。

極值看值不看次序，空集合沒有極值

M 列出時 −5/9 在第一個，但最小元素是 −7/12（S09）。空集合沒有最小元素，因為不存在 m∈∅；S08 的歸納從 n=1 開始，不涵蓋空集合，不能替空集合指定任意極值。

• 1/(−2) 與 1/3 交叉相乘得 1·3=3>−2=1·(−2)，所以 1/(−2)>1/3 → reject — 分母 −2 為負，L_cross 不適用；1/(−2)=−1/2<1/3。
• −7/12 是端點，所以不屬於 [−7/12,1/3] → reject — −7/12≤−7/12≤1/3 成立，閉區間包含端點。
• M 的最小元素是 −5/9，因為它列在第一個 → reject — −7/12<−5/9（S04），最小元素由值決定，是 −7/12。
• 空集合的最小元素是 0 → reject — 最小元素必須屬於該集合，而 0∉∅；空集合沒有最小元素。

結論與限制

對所有實數 a、b、c，a<b ⇔ a+c<b+c；q、s>0 時 p/q<r/s ⇔ ps<rq；非空有限實數集合有唯一的最小元素（最大元素同理）。M 的元素排成 −7/12<−5/9<−1/2<1/3，所以 min M=−7/12、max M=1/3（與列出次序無關）；[−7/12,1/3] 是合法閉區間，包含兩端點與 M 的全部元素，不包含 1/2。

• 順序公理（order_basics）作為前提使用，本稿不從實數的構造推導它們。
• 最大元素的存在只以「同一論證把 ≤ 換成 ≥」說明，未逐步寫出。

驗證及來源綁定

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

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

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