alphaInv_gauge_invariant
plain-language theorem explainer
alphaInv_gauge_invariant establishes that the inverse fine-structure constant remains fixed under rescalings of the ledger potential and cost. Researchers auditing parameter counts in Recognition Science cite it to separate gauge freedoms from tunable constants. The term-mode proof reduces to reflexivity after introducing the rescaling variables.
Claim. For all real numbers $α, k, b$ with $α ≠ 0$ and $k ≠ 0$, the dimensionless inverse fine-structure constant satisfies $α^{-1} = α^{-1}$.
background
The module resolves Gap 3 by separating gauge choices (rescalings p → αp + b and J → kJ) from parameters. Dimensionless outputs such as α^{-1} must stay fixed for the rescalings to count as gauge. alphaInv is defined as alpha_seed · exp(−f_gap / alpha_seed) and equals approximately 137.036 with no free parameters. Upstream, the Physical structure requires positive c, ħ, G on bridge anchors, while A denotes the active edge count per tick (equal to 1) and the actualization operator that maps configurations to their J-minimizing realizations.
proof idea
The term proof introduces the five arguments α, k, b, hα, hk and applies reflexivity. No lemmas are called; the equality holds definitionally because both sides name the same constant.
why it matters
It supplies the invariance step for gap3_resolved, which concludes that ledger rescalings are gauge rather than parameters. This supports the framework claim of zero parameters, consistent with the Recognition Composition Law and the forcing chain through T8 (D = 3). The result closes the specific objection that continuous rescaling freedoms act as tunable constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.