alphaInv_dimensionless
plain-language theorem explainer
alphaInv_dimensionless establishes that the inverse fine-structure constant equals some positive real number. Physicists checking whether Recognition Science fixes dimensionless constants without tunable parameters would cite it when rebutting gauge-freedom objections. The proof is a direct term application of the alphaInv definition, followed by rewriting to the predicted value and normalization to confirm positivity.
Claim. There exists a positive real number $n$ such that the inverse fine-structure constant satisfies $n = 4π·11 - ln φ - 103/(102π^5)$ (equivalently $α^{-1} = α_seed · exp(-f_gap / α_seed)$).
background
The Gauge Symmetries vs Parameters module distinguishes gauge freedoms (rescalings p → αp + b and J → kJ) from physical parameters. Dimensionless quantities such as α^{-1} are constructed so that all gauge factors cancel, leaving a unique number. Upstream, Constants.Alpha.alphaInv defines α^{-1} := α_seed · exp(-f_gap / α_seed) from the structural seed and gap, with no adjustable parameters; the module doc-comment notes that its components (4π·11 from geometry, ln φ from scale ratios, and 103/(102π^5) from topology) are each pure numbers.
proof idea
The proof is a one-line wrapper: it exhibits Alpha.alphaInv directly, confirms equality by reflexivity, rewrites via alphaInv_predicted_value, and applies norm_num to establish positivity.
why it matters
This declaration closes the gauge-objection gap in the module by confirming α^{-1} is a pure number, feeding the larger claim that α is gauge-invariant (see the module's main-theorem comment). It aligns with Recognition Science landmarks T5 (J-uniqueness) and the phi-forcing chain, where dimensionless constants emerge fixed rather than tunable. No open scaffolding remains here; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.