ratio_gauge_invariant
plain-language theorem explainer
Dimensionless ratios of real numbers remain unchanged under common nonzero scaling by α. Recognition Science researchers cite this algebraic fact to confirm that quantities like α^{-1} are independent of gauge choices in the ledger. The proof is a direct two-tactic reduction that cancels the shared factor and normalizes the equality.
Claim. For real numbers $p_1$, $p_2$ with $p_2 ≠ 0$ and scaling factor $α ≠ 0$, the ratio satisfies $ (α p_1) / (α p_2) = p_1 / p_2 $.
background
The module resolves the objection that ledger rescalings p → αp + b introduce free parameters by separating gauge freedom (physically irrelevant unit choices) from dimensionless parameters (physically meaningful). When b = b' = 0 the ratio p1/p2 is unchanged, so outputs such as α^{-1} = 4π·11 - ln φ - 103/(102π^5) are unique across gauges, matching the standard physics example where α = 1/137.036... holds in SI, Gaussian, or natural units. Upstream structures supply the ledger and mechanism contexts in which these ratios appear, but the present result is purely algebraic.
proof idea
The proof is a two-tactic term-mode script. field_simp cancels the common nonzero factor α in numerator and denominator under the given hypotheses; ring then confirms the resulting identity.
why it matters
The result supplies the algebraic core for the Gap 3 resolution, showing that gauge transformations leave dimensionless observables fixed and thereby fixing constants such as α^{-1} inside (137.030, 137.039) without tunable freedom. It directly supports sibling declarations including alphaInv_gauge_invariant and alpha_not_tunable, and aligns with the Recognition framework's requirement that rescaling symmetries cancel in all physical predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.