# Dimensional analysis: checking ½mv²=mgh with exponent vectors and ruling out v=2gh [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-dimensional-analysis/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-dimensional-analysis-01 · production-20261019-adopted-96 ## Goal and scope With integer exponent vectors d(Q)=(a,b,c) over the base dimensions L, M, T: compute the dimensions of speed, acceleration and two energy expressions; decide that ½mv²=mgh is dimensionally consistent, that v=2gh is not and cannot be repaired by a pure-number constant, and that v²=4gh is consistent but wrong in the constant-acceleration model; decide that m+v cannot be added; solve E=C·m^α v^β for α=1 and β=2; and explain that equal dimensions do not mean equal unit conversion factors. Uses only the three base dimensions L, M, T and integer exponents (MKO assumption a1); ½, 2 and 4 are declared dimensionless, and g is a dimensioned quantity (assumption a2). The constant-acceleration model used in S11 is stated in G3 and is not derived by dimensional analysis. SI conversion details, Buckingham Pi and nondimensionalization are not treated; the canonical MKO and its English edition are not changed. ## Givens and symbols - cartesian_product_def - numeric_evaluation - eq_congruence - power_laws - distributive - G1 — Base dimensions L, M, T; the dimension [Q]=L^a M^b T^c of a quantity Q is represented by the integer vector d(Q)=(a,b,c) (MKO assumption a1). - G2 — d(m)=(0,1,0), d(h)=(1,0,0), d(t)=(0,0,1); speed v is length divided by time and acceleration g is speed divided by time; ½, 2, 4 and C are dimensionless pure numbers (assumption a2). - G3 — Constant-acceleration model: starting from rest with acceleration g>0, after time t>0 the speed is v=gt and the distance travelled is h=gt²/2. - G4 — Expressions to check: (E1) ½mv²=mgh; (E2) v=2gh; (E3) v²=4gh; (E4) the sum m+v. - d(Q)=(a,b,c) — exponent vector of the quantity Q, [Q]=L^a M^b T^c - m,\ h,\ t — mass, height, time - v,\ g — speed, acceleration - E — energy (kinetic) - C,\ \alpha,\ \beta — dimensionless constant and unknown exponents ## Rules and sources - cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule. - power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1. - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable. - add_zero · prerequisite — Additive identity: u+0=u. - contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds. - mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw). - mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ). - square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0. - order_basics · prerequisite — Order of the reals: exactly one of uv holds; u0 give uwvw. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - mko_dim · cited — Relative to basic dimensions L,M,T, write [Q]=L^a M^b T^c, represented by (a,b,c). Products add vectors, quotients subtract them and integer powers scale them. Quantities to be equated or added must have matching dimensions. · mko-dimensional-analysis - mko_dim_limits · cited — Dimensional consistency is necessary but not sufficient for a physical equation; if the two sides have different dimensions, adjusting a pure-number constant cannot fix it, and if they agree there may still be a wrong coefficient. Dimensional analysis does not track the numerical factors of unit conversion. · mko-dimensional-analysis - vec_ops · prerequisite — Componentwise operations in ℤ³: (a,b,c)±(a′,b′,c′)=(a±a′,b±b′,c±c′) and k(a,b,c)=(ka,kb,kc); two vectors are equal exactly when the three components are equal; a pure number has dimension vector (0,0,0). - L_const_factor · lemma — For a dimensionless constant k and any quantity Q, d(kQ)=d(Q). ## Main derivation S01 · definitionBefore [Q]=L^aM^bT^c After d(PQ)=d(P)+d(Q),\ d(P/Q)=d(P)-d(Q),\ d(Q^k)=k\,d(Q) Conditions: k\in\mathbb{Z} Rule: mko_dim · Uses: G1, mko_dim Leaf basis: mko_dim + power_laws + vec_ops By the MKO, write dimensions as exponent vectors; products add vectors, quotients subtract them and integer powers scale them. These three rules are the exponent laws such as L^a·L^a′=L^(a+a′) applied to each base dimension. Two quantities that are to be equated or added must have the same vector. S02 · definitionBefore m,\ h,\ t After d(m)=(0,1,0),\ d(h)=(1,0,0),\ d(t)=(0,0,1) Conditions: none Rule: def_intro · Uses: G2 Leaf basis: def_intro The dimensions of the base quantities come from G2: mass involves only M, height only L and time only T. S03 · equivalentBefore d(v)=d(h)-d(t) After d(v)=(1,0,-1) Conditions: none Rule: vec_ops · Uses: S01, S02, G2 Leaf basis: vec_ops + numeric_evaluation Speed is length divided by time, and a quotient subtracts: (1,0,0)−(0,0,1)=(1,0,−1), that is [v]=L T⁻¹. S04 · equivalentBefore d(g)=d(v)-d(t) After d(g)=(1,0,-2) Conditions: none Rule: vec_ops · Uses: S03, S02, G2 Leaf basis: vec_ops + numeric_evaluation Acceleration is speed divided by time: (1,0,−1)−(0,0,1)=(1,0,−2), that is [g]=L T⁻². g is a dimensioned quantity, not a pure number. S05 · equivalentBefore d(v^2)=2\,d(v) After d(v^2)=(2,0,-2) Conditions: k=2 Rule: vec_ops · Uses: S03, S01 Leaf basis: vec_ops + power_laws An integer power scales: 2·(1,0,−1)=(2,0,−2). S06 · equivalentBefore d(\tfrac{1}{2}mv^2)=d(\tfrac{1}{2})+d(m)+d(v^2) After d(\tfrac{1}{2}mv^2)=(2,1,-2) Conditions: d(\tfrac{1}{2})=(0,0,0) Rule: vec_ops · Uses: S02, S05, G2 Leaf basis: vec_ops + numeric_evaluation Products add: (0,0,0)+(0,1,0)+(2,0,−2)=(2,1,−2), that is [½mv²]=L² M T⁻². ½ is a pure number and does not affect the dimension. S07 · equivalentBefore d(mgh)=d(m)+d(g)+d(h) After d(mgh)=(2,1,-2) Conditions: none Rule: vec_ops · Uses: S02, S04 Leaf basis: vec_ops + numeric_evaluation (0,1,0)+(1,0,−2)+(1,0,0)=(2,1,−2). S08 · impliesBefore d(\tfrac{1}{2}mv^2)=(2,1,-2),\ d(mgh)=(2,1,-2) After \text{(E1) dimensionally consistent} Conditions: none Rule: mko_dim · Uses: S06, S07, mko_dim, mko_dim_limits Leaf basis: mko_dim + vec_ops The two vectors are the same, so (E1) passes the necessary condition of dimensional consistency. By the MKO this does not prove that (E1) is physically correct; it is merely not ruled out by dimensions. S09 · impliesBefore d(v)=(1,0,-1),\ d(2gh)=(2,0,-2) After \text{(E2) inconsistent};\ d(kgh)=(2,0,-2)\ \forall k\ \text{dimensionless} Conditions: none Rule: L_const_factor · Uses: S03, S04, S02, L_const_factor Leaf basis: L_const_factor + vec_ops d(2gh)=(0,0,0)+(1,0,−2)+(1,0,0)=(2,0,−2), while d(v)=(1,0,−1); the L components differ, 1≠2, so the vectors differ and (E2) is dimensionally inconsistent and ruled out. By Lemma L_const_factor (proved in S09.1), replacing 2 by any dimensionless constant k leaves d(kgh) unchanged, so no adjustment of a pure number can repair it. S10 · impliesBefore d(v^2)=(2,0,-2),\ d(4gh) After d(4gh)=(2,0,-2):\ \text{(E3) dimensionally consistent} Conditions: none Rule: mko_dim · Uses: S05, S04, S02, L_const_factor Leaf basis: mko_dim + L_const_factor + vec_ops By L_const_factor, d(4gh)=d(gh)=(1,0,−2)+(1,0,0)=(2,0,−2)=d(v²), so (E3) is dimensionally consistent. S11 · impliesBefore v=gt,\ h=\tfrac{1}{2}gt^2 After v^2=2gh,\ \text{so }v^2=4gh\ \text{fails for }g,t>0 Conditions: g>0,\ t>0 Rule: mko_dim_limits · Uses: G3, S10, mko_dim_limits Leaf basis: mko_dim_limits + contradiction In the model G3 we have v²=2gh (S11.1), so if (E3) also held then 2gh=4gh, that is v²=2v², giving v²=0; but v=gt>0, a contradiction (S11.2). (E3) is dimensionally consistent yet wrong in this model: consistency is necessary but not sufficient, and it cannot detect the wrong coefficient 4. S12 · impliesBefore m+v,\ d(m)=(0,1,0),\ d(v)=(1,0,-1) After d(m)\neq d(v):\ m+v\ \text{not allowed} Conditions: none Rule: mko_dim · Uses: S02, S03, mko_dim Leaf basis: mko_dim + vec_ops By the MKO, quantities to be added must have matching dimensions. (0,1,0) and (1,0,−1) differ in all three components, so m+v is not a meaningful quantity; nor is there a 'dimension of the sum' such as (1,1,−1) obtained by adding vectors, since adding vectors corresponds to products only. S13 · equivalentBefore (2,1,-2)=\alpha(0,1,0)+\beta(1,0,-1) After \alpha=1,\ \beta=2,\ E=C\,m\,v^2 Conditions: C\ \text{dimensionless} Rule: vec_ops · Uses: S06, S02, S03, G2 Leaf basis: vec_ops + eq_congruence Require the energy E=C·m^α v^β to have the dimension of ½mv²: the right side has vector (β, α, −β). Comparing components: L gives β=2, M gives α=1, and T gives −β=−2, consistent with β=2. Three equations in two unknowns, so the T component is a genuine consistency check. Hence E=C m v²; dimensional analysis cannot determine C, and C=½ must come from a physical argument. S14 · impliesBefore \mathrm{J}=\mathrm{kg\,m^2\,s^{-2}},\ \mathrm{erg}=\mathrm{g\,cm^2\,s^{-2}} After d=(2,1,-2)\ \text{for both},\ 1\,\mathrm{J}=10^7\,\mathrm{erg} Conditions: none Rule: mko_dim_limits · Uses: S06, mko_dim_limits Leaf basis: mko_dim_limits + power_laws + numeric_evaluation The joule and the erg are both units of energy with dimension vector (2,1,−2); but 1 g=10⁻³ kg and 1 cm²=10⁻⁴ m², so 1 erg=10⁻⁷ J, that is 1 J=10⁷ erg. Equal dimensions do not mean equal numbers; dimensional analysis does not track unit conversion factors, and a unit name is not the same thing as a dimension exponent. S15 · impliesBefore \text{proved facts} After \text{(E1) consistent; (E2) inconsistent; (E3) consistent but false in G3; (E4) not allowed; }E=Cmv^2 Conditions: none Rule: and_intro_elim · Uses: S08, S09, S10, S11, S12, S13 Leaf basis: and_intro_elim Combine the conclusions: (E1) is consistent; (E2) is inconsistent and cannot be repaired by a pure number; (E3) is consistent but false in the constant-acceleration model; m+v cannot be added; energy has the dimensional form C m v², with C not determined by dimensional analysis. ## Substeps and lemmas S09.1 · equivalentBefore d(kQ) After d(kQ)=d(k)+d(Q)=(0,0,0)+d(Q)=d(Q) Conditions: d(k)=(0,0,0) Rule: vec_ops · Uses: S01, G2 Leaf basis: vec_ops + add_zero Products add, and a dimensionless constant has vector (0,0,0); adding the zero vector changes nothing. This sub-step proves Lemma L_const_factor. S11.1 · equivalentBefore v^2=(gt)^2,\ 2gh=2g\cdot\tfrac{1}{2}gt^2 After v^2=g^2t^2=2gh Conditions: none Rule: power_laws · Uses: G3 Leaf basis: power_laws + mul_assoc + mul_comm (gt)²=g²t²; 2g·(½gt²)=g²t². They are equal, so v²=2gh (N5 checks this as a polynomial identity). S11.2 · impliesBefore v^2=4gh\ \text{(assumed)} After v^2=2v^2\Rightarrow v^2=0\Rightarrow v=0,\ \text{contradicting }v=gt>0 Conditions: g>0,\ t>0 Rule: contradiction · Uses: S11.1, G3 Leaf basis: square_nonneg + order_basics + contradiction Assume v²=4gh. By S11.1, 4gh=2·(2gh)=2v², so v²=2v²; subtracting v² gives v²=0, and since u²=0 ⇔ u=0, v=0. But g>0 and t>0 make v=gt>0, a contradiction. So (E3) fails in this model. ## Reverse audits - S15 · sufficient_goal_reduction · S08, S09, S10, S11, S12, S13, and_intro_elim — Goal G: the determinations in the goal. Sufficient condition H: S08 to S13, each already proved (H⇒G by conjunction introduction). H is derived forwards from the givens; G is never used as a premise. - S14 · premise_audit · mko_dim_limits, power_laws, numeric_evaluation — It needs the definitions of the two unit systems and powers of 10; the conclusion is illustrative and independent of the earlier dimensional verdicts. - S13 · inverse_equivalence · vec_ops, cartesian_product_def — Vector equality ⇔ the three components are equal; substituting α=1, β=2 gives (2,1,−2), so both directions hold. - S12 · premise_audit · S02, S03, mko_dim, vec_ops — It needs only that the two vectors differ. - S11.2 · premise_audit · S11.1, square_nonneg, order_basics, contradiction — It needs g, t>0; at t=0 (before any motion) v=h=0 and both relations hold trivially, which gives no support to (E3). - S11.1 · inverse_equivalence · power_laws, mul_assoc, mul_comm — Exponent laws and commutativity and associativity of multiplication; both sides are the same expression. - S11 · premise_audit · G3, mko_dim_limits — It needs the stated physical model and g, t>0; dimensional analysis alone cannot supply this verdict. - S10 · premise_audit · L_const_factor, vec_ops, mko_dim — As in S08, it only passes the necessary condition; S11 shows that it is still wrong. - S09.1 · inverse_equivalence · vec_ops, add_zero — An identity of adding the zero vector, valid both ways; it holds only for dimensionless k, since a dimensioned constant would change the vector. - S09 · premise_audit · L_const_factor, vec_ops, mko_dim_limits — Unequal vectors need only one differing component. The conclusion is that (E2) is certainly wrong; what the correct relation is is not claimed here and needs a physical model (S11). - S08 · premise_audit · S06, S07, mko_dim_limits — The conclusion is only 'passes the necessary condition'; the converse (consistent ⇒ correct) is not claimed. - S07 · inverse_equivalence · vec_ops, numeric_evaluation — Componentwise integer addition, valid both ways. - S06 · inverse_equivalence · vec_ops, numeric_evaluation — Componentwise integer addition; both sides are the same vector. - S05 · inverse_equivalence · vec_ops — Multiplying by 2 and halving undo each other on these even components, so both ways hold. - S04 · inverse_equivalence · vec_ops, numeric_evaluation — Componentwise integer arithmetic, valid both ways. - S03 · inverse_equivalence · vec_ops, numeric_evaluation — Componentwise integer arithmetic; backwards, (1,0,−1)+(0,0,1)=(1,0,0) restores it. - S02 · premise_audit · G2, def_intro — Taken directly from the givens; no new fact is derived. - S01 · premise_audit · G1, mko_dim, power_laws — This step only states the rules and derives no new fact; exponents are restricted to integers. ## Error controls and negative controls Dimensional consistency does not make an equation correctOne misconception named by the MKO: both sides of v²=4gh are (2,0,−2), but in the constant-acceleration model the correct relation is v²=2gh (S11). Dimensional analysis cannot detect a wrong dimensionless coefficient, a wrong direction or a wrong physical assumption; it can only rule out inconsistent expressions. A unit name is not a dimension exponentAnother misconception named by the MKO: the joule and the erg have the same dimension vector but differ by a factor of 10⁷ (S14). Notation also needs care: the m in the formulas is mass (dimension M), while the unit 'm' is the metre (dimension L); they must not be confused. Pure numbers cannot fix an inconsistency; dimensioned constants must be declaredBy L_const_factor, multiplying by any dimensionless k leaves the dimension unchanged, so v=k·gh is inconsistent for every k (S09). Conversely, g is a dimensioned quantity (1,0,−2); treating it as a pure number would spoil the check of (E1). MKO assumption a2 requires the dimensions of constants to be stated. - v²=4gh is dimensionally consistent, so it is the correct free-fall relation → reject — The constant-acceleration model gives v²=2gh; if v²=4gh also held then v=0, contradicting v=gt>0 (S11.2). - With the right dimensionless constant k, v=k·gh becomes dimensionally consistent → reject — d(k·gh)=(2,0,−2)≠(1,0,−1)=d(v), whatever k is (S09, L_const_factor). - m+v is a meaningful quantity with dimension (0,1,0)+(1,0,−1)=(1,1,−1) → reject — Only quantities with the same dimension can be added; adding vectors corresponds to the product mv, not the sum (S12). - The joule and the erg have the same dimension, so 1 J=1 erg → reject — 1 J=10⁷ erg; dimensional analysis does not track conversion factors (S14). ## Result and limitations d(v)=(1,0,−1), d(g)=(1,0,−2), and d(½mv²)=d(mgh)=(2,1,−2), so ½mv²=mgh is dimensionally consistent. v=2gh has sides (1,0,−1) and (2,0,−2), which differ, and no dimensionless constant can repair it. v²=4gh is consistent, but in the constant-acceleration model v²=2gh, so it is false: consistency is only necessary. m and v have different dimensions and cannot be added. From (2,1,−2)=α(0,1,0)+β(1,0,−1), α=1 and β=2, so E=C m v² with C not fixed by dimensions. The joule and the erg have the same dimension but 1 J=10⁷ erg. - The constant-acceleration model of S11 (v=gt, h=gt²/2) is used as a given; this guide does not derive it from mechanics. - SI conversion, the Buckingham Pi theorem and nondimensionalization belong to the MKO's formal next step. ## Verification and source binding 8 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: d37c1bae6edd943432231306417829058ff4d2192474aeccdb559f8b130beb94 - original source SHA-256: d37c1bae6edd943432231306417829058ff4d2192474aeccdb559f8b130beb94 - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-dimensional-analysis-01.json)