# 量綱分析：以指數向量核對 ½mv²=mgh 並排除 v=2gh

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

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

derivation-mko-dimensional-analysis-01 · production-20261019-adopted-96



## 目標與範圍

以基本量綱 L、M、T 的整數指數向量 d(Q)=(a,b,c)：算出速度、加速度與兩種能量式的量綱；判定 ½mv²=mgh 量綱一致、v=2gh 不一致且無法以純數常數修正、v²=4gh 量綱一致卻在等加速度模型中錯誤；判定 m+v 不能相加；由 E=C·m^α v^β 解出 α=1、β=2；並說明量綱相同不代表單位換算因子相同。

只用 L、M、T 三個基本量綱與整數指數（MKO 假設 a1）；½、2、4 明示為無因次常數，g 是具量綱的量（假設 a2）。S11 用到的等加速度運動模型明列於 G3，不由量綱分析推出。不處理 SI 換算細節、Buckingham Pi 或無因次化；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- cartesian_product_def
- numeric_evaluation
- eq_congruence
- power_laws
- distributive


- G1 — 基本量綱 L、M、T；量 Q 的量綱 [Q]=L^a M^b T^c 以整數向量 d(Q)=(a,b,c) 表示（MKO 假設 a1）。
- G2 — d(m)=(0,1,0)，d(h)=(1,0,0)，d(t)=(0,0,1)；速度 v 是長度除以時間，加速度 g 是速度除以時間；½、2、4 與 C 是無因次純數（假設 a2）。
- G3 — 等加速度模型：自靜止以加速度 g>0 運動時間 t>0 後，速度 v=gt，移動距離 h=gt²/2。
- G4 — 待檢查的式子：(E1) ½mv²=mgh；(E2) v=2gh；(E3) v²=4gh；(E4) 和 m+v。


- d(Q)=(a,b,c) — 量 Q 的量綱指數向量，[Q]=L^a M^b T^c
- m,\ h,\ t — 質量、高度、時間
- v,\ g — 速度、加速度
- E — 能量（動能）
- C,\ \alpha,\ \beta — 無因次常數與待求指數





## 規則與來源


- cartesian_product_def · prerequisite — 笛卡兒積：A×B 是所有有序對 (a,b)（a∈A、b∈B）的集合；(a,b)=(c,d) ⇔ a=c 且 b=d。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- eq_congruence · prerequisite — 等式同用：若 u=v，對兩邊做同一個有定義的運算 f，得 f(u)=f(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。
- distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- add_zero · prerequisite — 加法單位元：u+0=u。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- mul_assoc · prerequisite — 乘法結合律：(uv)w=u(vw)。
- mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
- square_nonneg · prerequisite — 實數平方非負：對所有實數 u，u²≥0，且 u²=0 ⇔ u=0。
- 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。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_dim · cited — 相對基本量綱 L、M、T，把物理量 Q 的量綱記為 [Q]=L^a M^b T^c，亦即指數向量 (a,b,c)。乘法相加向量、除法相減、整數冪倍乘；可相等或相加的量必須量綱一致。 · mko-dimensional-analysis
- mko_dim_limits · cited — 量綱一致是候選物理方程的必要條件，不是充分條件；方程若兩側量綱不同，不能由調整純數常數修正；若一致，仍可能有錯係數。量綱分析不追蹤單位換算的數值因子。 · mko-dimensional-analysis
- vec_ops · prerequisite — ℤ³ 的逐分量運算：(a,b,c)±(a′,b′,c′)=(a±a′,b±b′,c±c′)，k(a,b,c)=(ka,kb,kc)；兩向量相等當且僅當三個分量分別相等；純數的量綱向量是 (0,0,0)。
- L_const_factor · lemma — 對無因次常數 k 與任意量 Q，d(kQ)=d(Q)。





## 逐步主鏈

S01 · definition操作前

[Q]=L^aM^bT^c

操作後

d(PQ)=d(P)+d(Q),\ d(P/Q)=d(P)-d(Q),\ d(Q^k)=k\,d(Q)

條件：k\in\mathbb{Z}

規則：mko_dim · 依賴：G1, mko_dim

葉節點依據：mko_dim + power_laws + vec_ops

依 MKO，把量綱寫成指數向量；乘積相加向量、商相減、整數冪倍乘。這三條就是指數律 L^a·L^a′=L^(a+a′) 等逐基本量綱套用的結果。要相等或相加的兩個量，向量必須相同。



S02 · definition操作前

m,\ h,\ t

操作後

d(m)=(0,1,0),\ d(h)=(1,0,0),\ d(t)=(0,0,1)

條件：無

規則：def_intro · 依賴：G2

葉節點依據：def_intro

基本量的量綱由 G2 給出：質量只含 M，高度只含 L，時間只含 T。



S03 · equivalent操作前

d(v)=d(h)-d(t)

操作後

d(v)=(1,0,-1)

條件：無

規則：vec_ops · 依賴：S01, S02, G2

葉節點依據：vec_ops + numeric_evaluation

速度是長度除以時間，商相減：(1,0,0)−(0,0,1)=(1,0,−1)，即 [v]=L T⁻¹。



S04 · equivalent操作前

d(g)=d(v)-d(t)

操作後

d(g)=(1,0,-2)

條件：無

規則：vec_ops · 依賴：S03, S02, G2

葉節點依據：vec_ops + numeric_evaluation

加速度是速度除以時間：(1,0,−1)−(0,0,1)=(1,0,−2)，即 [g]=L T⁻²。g 是具量綱的量，不是純數。



S05 · equivalent操作前

d(v^2)=2\,d(v)

操作後

d(v^2)=(2,0,-2)

條件：k=2

規則：vec_ops · 依賴：S03, S01

葉節點依據：vec_ops + power_laws

整數冪倍乘：2·(1,0,−1)=(2,0,−2)。



S06 · equivalent操作前

d(\tfrac{1}{2}mv^2)=d(\tfrac{1}{2})+d(m)+d(v^2)

操作後

d(\tfrac{1}{2}mv^2)=(2,1,-2)

條件：d(\tfrac{1}{2})=(0,0,0)

規則：vec_ops · 依賴：S02, S05, G2

葉節點依據：vec_ops + numeric_evaluation

乘積相加：(0,0,0)+(0,1,0)+(2,0,−2)=(2,1,−2)，即 [½mv²]=L² M T⁻²。½ 是純數，不影響量綱。



S07 · equivalent操作前

d(mgh)=d(m)+d(g)+d(h)

操作後

d(mgh)=(2,1,-2)

條件：無

規則：vec_ops · 依賴：S02, S04

葉節點依據：vec_ops + numeric_evaluation

(0,1,0)+(1,0,−2)+(1,0,0)=(2,1,−2)。



S08 · implies操作前

d(\tfrac{1}{2}mv^2)=(2,1,-2),\ d(mgh)=(2,1,-2)

操作後

\text{(E1) dimensionally consistent}

條件：無

規則：mko_dim · 依賴：S06, S07, mko_dim, mko_dim_limits

葉節點依據：mko_dim + vec_ops

兩邊向量相同，所以 (E1) 通過量綱一致這個必要條件。依 MKO，這不證明 (E1) 在物理上正確；它只是沒有被量綱排除。



S09 · implies操作前

d(v)=(1,0,-1),\ d(2gh)=(2,0,-2)

操作後

\text{(E2) inconsistent};\ d(kgh)=(2,0,-2)\ \forall k\ \text{dimensionless}

條件：無

規則：L_const_factor · 依賴：S03, S04, S02, L_const_factor

葉節點依據：L_const_factor + vec_ops

d(2gh)=(0,0,0)+(1,0,−2)+(1,0,0)=(2,0,−2)，而 d(v)=(1,0,−1)；L 分量 1≠2，向量不同，所以 (E2) 量綱不一致而被排除。依引理 L_const_factor（在 S09.1 證明），把 2 換成任何無因次常數 k 都不改變 d(kgh)，所以不可能靠調整純數修正。



S10 · implies操作前

d(v^2)=(2,0,-2),\ d(4gh)

操作後

d(4gh)=(2,0,-2):\ \text{(E3) dimensionally consistent}

條件：無

規則：mko_dim · 依賴：S05, S04, S02, L_const_factor

葉節點依據：mko_dim + L_const_factor + vec_ops

依 L_const_factor，d(4gh)=d(gh)=(1,0,−2)+(1,0,0)=(2,0,−2)=d(v²)，所以 (E3) 量綱一致。



S11 · implies操作前

v=gt,\ h=\tfrac{1}{2}gt^2

操作後

v^2=2gh,\ \text{so }v^2=4gh\ \text{fails for }g,t>0

條件：g>0,\ t>0

規則：mko_dim_limits · 依賴：G3, S10, mko_dim_limits

葉節點依據：mko_dim_limits + contradiction

在 G3 的模型中 v²=2gh（S11.1），所以若 (E3) 也成立，則 2gh=4gh，即 v²=2v²，得 v²=0；但 v=gt>0，矛盾（S11.2）。(E3) 量綱一致卻在這個模型中錯誤：量綱一致是必要而非充分的條件，它查不出錯的係數 4。



S12 · implies操作前

m+v,\ d(m)=(0,1,0),\ d(v)=(1,0,-1)

操作後

d(m)\neq d(v):\ m+v\ \text{not allowed}

條件：無

規則：mko_dim · 依賴：S02, S03, mko_dim

葉節點依據：mko_dim + vec_ops

依 MKO，可相加的量必須量綱一致。(0,1,0) 與 (1,0,−1) 在三個分量上都不同，所以 m+v 不是有意義的量；也沒有「(1,1,−1)」這種把向量相加得到的「和的量綱」，向量相加只對應乘積。



S13 · equivalent操作前

(2,1,-2)=\alpha(0,1,0)+\beta(1,0,-1)

操作後

\alpha=1,\ \beta=2,\ E=C\,m\,v^2

條件：C\ \text{dimensionless}

規則：vec_ops · 依賴：S06, S02, S03, G2

葉節點依據：vec_ops + eq_congruence

要求能量 E=C·m^α v^β 與 ½mv² 有相同量綱：右邊向量為 (β, α, −β)。逐分量比較：L 分量 β=2，M 分量 α=1，T 分量 −β=−2，與 β=2 一致。三個方程、兩個未知數，T 分量是真正的一致性檢查。所以 E=C m v²；量綱分析定不出 C，C=½ 要由物理論證決定。



S14 · implies操作前

\mathrm{J}=\mathrm{kg\,m^2\,s^{-2}},\ \mathrm{erg}=\mathrm{g\,cm^2\,s^{-2}}

操作後

d=(2,1,-2)\ \text{for both},\ 1\,\mathrm{J}=10^7\,\mathrm{erg}

條件：無

規則：mko_dim_limits · 依賴：S06, mko_dim_limits

葉節點依據：mko_dim_limits + power_laws + numeric_evaluation

焦耳與爾格都是能量單位，量綱向量同為 (2,1,−2)；但 1 g=10⁻³ kg、1 cm²=10⁻⁴ m²，所以 1 erg=10⁻⁷ J，即 1 J=10⁷ erg。量綱相同不代表數值相同；量綱分析不追蹤單位換算因子，單位名稱也不等於量綱指數。



S15 · implies操作前

\text{proved facts}

操作後

\text{(E1) consistent; (E2) inconsistent; (E3) consistent but false in G3; (E4) not allowed; }E=Cmv^2

條件：無

規則：and_intro_elim · 依賴：S08, S09, S10, S11, S12, S13

葉節點依據：and_intro_elim

合併結論：(E1) 量綱一致；(E2) 不一致且純數無法修正；(E3) 一致但在等加速度模型中錯誤；m+v 不能相加；能量的量綱形式是 C m v²，C 由量綱分析定不出。







## 局部子步與引理

S09.1 · equivalent操作前

d(kQ)

操作後

d(kQ)=d(k)+d(Q)=(0,0,0)+d(Q)=d(Q)

條件：d(k)=(0,0,0)

規則：vec_ops · 依賴：S01, G2

葉節點依據：vec_ops + add_zero

乘積相加，且無因次常數的向量是 (0,0,0)，加零向量不變。此子步證得引理 L_const_factor。



S11.1 · equivalent操作前

v^2=(gt)^2,\ 2gh=2g\cdot\tfrac{1}{2}gt^2

操作後

v^2=g^2t^2=2gh

條件：無

規則：power_laws · 依賴：G3

葉節點依據：power_laws + mul_assoc + mul_comm

(gt)²=g²t²；2g·(½gt²)=g²t²。兩者相等，所以 v²=2gh（N5 為多項式恆等式核對）。



S11.2 · implies操作前

v^2=4gh\ \text{(assumed)}

操作後

v^2=2v^2\Rightarrow v^2=0\Rightarrow v=0,\ \text{contradicting }v=gt>0

條件：g>0,\ t>0

規則：contradiction · 依賴：S11.1, G3

葉節點依據：square_nonneg + order_basics + contradiction

假設 v²=4gh。由 S11.1，4gh=2·(2gh)=2v²，所以 v²=2v²，兩邊減 v² 得 v²=0，再依平方非負與 u²=0 ⇔ u=0 得 v=0。但 g>0、t>0 使 v=gt>0，矛盾。所以在此模型中 (E3) 不成立。







## 逐步反向審查


- S15 · sufficient_goal_reduction · S08, S09, S10, S11, S12, S13, and_intro_elim — 目標 G：本稿目標的各項判定。足夠條件 H：S08 到 S13 各自已證（H⇒G 由合取引入）。H 由給定條件正向推出，沒有把 G 當作前提。
- S14 · premise_audit · mko_dim_limits, power_laws, numeric_evaluation — 需要兩組單位的定義與 10 的冪次計算；結論只是說明，與前面的量綱判定互不依賴。
- S13 · inverse_equivalence · vec_ops, cartesian_product_def — 向量相等 ⇔ 三個分量相等；代回 α=1、β=2 得 (2,1,−2)，雙向成立。
- S12 · premise_audit · S02, S03, mko_dim, vec_ops — 只需要兩個向量不同。
- S11.2 · premise_audit · S11.1, square_nonneg, order_basics, contradiction — 需要 g、t>0；若 t=0（尚未運動），v=h=0，兩式都成立，這不能拿來支持 (E3)。
- S11.1 · inverse_equivalence · power_laws, mul_assoc, mul_comm — 指數律與乘法交換結合律，雙向是同一個式子。
- S11 · premise_audit · G3, mko_dim_limits — 需要明示的物理模型與 g、t>0；量綱分析本身無法提供這個判斷。
- S10 · premise_audit · L_const_factor, vec_ops, mko_dim — 同 S08，只是通過必要條件；S11 會顯示它仍然錯誤。
- S09.1 · inverse_equivalence · vec_ops, add_zero — 加零向量的恆等式，雙向成立；只對無因次 k 成立，具量綱常數會改變向量。
- S09 · premise_audit · L_const_factor, vec_ops, mko_dim_limits — 向量不等只需一個分量不同。結論是 (E2) 必錯；這裡不宣稱正確的關係是什麼，那需要物理模型（S11）。
- S08 · premise_audit · S06, S07, mko_dim_limits — 結論只是「通過必要條件」，反向（一致 ⇒ 正確）不宣稱。
- S07 · inverse_equivalence · vec_ops, numeric_evaluation — 逐分量整數加法，雙向成立。
- S06 · inverse_equivalence · vec_ops, numeric_evaluation — 逐分量整數加法，雙向是同一向量。
- S05 · inverse_equivalence · vec_ops — 乘 2 與除以 2 在這些偶數分量上互逆，雙向成立。
- S04 · inverse_equivalence · vec_ops, numeric_evaluation — 逐分量整數計算，雙向成立。
- S03 · inverse_equivalence · vec_ops, numeric_evaluation — 逐分量整數計算；反向 (1,0,−1)+(0,0,1)=(1,0,0) 還原。
- S02 · premise_audit · G2, def_intro — 直接取自給定條件，不推出新事實。
- S01 · premise_audit · G1, mko_dim, power_laws — 此步只寫出規則，不推出新事實；指數限於整數。





## 錯誤控制與反例

量綱一致不等於方程正確MKO 指出的誤解之一：v²=4gh 兩邊都是 (2,0,−2)，但在等加速度模型中正確的是 v²=2gh（S11）。量綱分析查不出錯的無因次係數、錯的方向或錯的物理假設；它只能排除不一致的式子。

單位名稱不等於量綱指數MKO 指出的另一個誤解：焦耳與爾格的量綱向量相同，數值卻差 10⁷ 倍（S14）。另外要注意記號：公式中的 m 是質量（量綱 M），單位「m」是公尺（量綱 L），兩者不可混淆。

純數常數修不好不一致，具量綱常數要明示依 L_const_factor，乘上任何無因次 k 都不改變量綱，所以 v=k·gh 對每個 k 都不一致（S09）。反之，g 是具量綱的量 (1,0,−2)，若把它誤當純數，(E1) 的核對就會出錯；MKO 假設 a2 要求常數的量綱由題目明示。


- v²=4gh 量綱一致，所以它是正確的自由落體關係 → reject — 等加速度模型給出 v²=2gh；若 v²=4gh 也成立則 v=0，與 v=gt>0 矛盾（S11.2）。
- 只要選對無因次常數 k，v=k·gh 就會量綱一致 → reject — d(k·gh)=(2,0,−2)≠(1,0,−1)=d(v)，與 k 無關（S09、L_const_factor）。
- m+v 是有意義的量，量綱是 (0,1,0)+(1,0,−1)=(1,1,−1) → reject — 只有量綱相同的量才能相加；向量相加對應的是乘積 mv，不是和（S12）。
- 焦耳與爾格量綱相同，所以 1 J=1 erg → reject — 1 J=10⁷ erg；量綱分析不追蹤換算因子（S14）。





## 結論與限制

d(v)=(1,0,−1)，d(g)=(1,0,−2)，d(½mv²)=d(mgh)=(2,1,−2)，所以 ½mv²=mgh 量綱一致。v=2gh 兩邊為 (1,0,−1) 與 (2,0,−2)，不一致，且任何無因次常數都無法修正。v²=4gh 量綱一致，但在等加速度模型中 v²=2gh，所以它錯誤：量綱一致只是必要條件。m+v 量綱不同，不能相加。由 (2,1,−2)=α(0,1,0)+β(1,0,−1) 得 α=1、β=2，E=C m v²，C 不由量綱決定。焦耳與爾格量綱相同但 1 J=10⁷ erg。


- S11 的等加速度模型（v=gt、h=gt²/2）作為給定條件使用，本稿沒有從力學原理推導它。
- SI 換算、Buckingham Pi 定理與無因次化屬於 MKO 的 formal next。





## 驗證及來源綁定

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


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

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