ilg_alpha_is_alphaLock
plain-language theorem explainer
The declaration equates the ILG alpha exponent to the locked fine-structure constant defined by alphaLock = (1 - 1/phi)/2. Modelers of coercive projection gravity cite it to fix the exponent inside the Recognition Science constants without retuning. The proof is a one-line reflexivity that matches the shared algebraic expression from the Constants module.
Claim. In the ILG framework the alpha exponent satisfies $alpha = (1 - phi^{-1})/2$, where this value coincides with the canonical locked fine-structure constant.
background
The Coercive Projection Law module formalizes gravity via an energy functional whose unique minimizer yields the coercivity constant c = 49/162 and the net constant K_net = (9/7)^2 from eight-tick epsilon = 1/8. The upstream alphaLock definition supplies the locked fine-structure constant alpha_lock = (1 - 1/phi)/2 together with the algebraic bridge identity that clears the factor of 1/2 for the acceleration-parameterized exponent. The module setting assumes the ILG modified Poisson equation is equivalent to standard Poisson with effective pressure source p = w * rho_b and that the weight operator remains positive.
proof idea
The proof is a direct reflexivity that unfolds the definition of alphaLock from the Constants module and matches the ILG exponent expression exactly.
why it matters
This anchors the ILG alpha inside the Recognition Science framework, linking to the T5 J-uniqueness step and the alpha band (137.030, 137.039). It supports the pressure-equivalence and energy-minimization results of the coercive projection law, confirming consistency with the phi-ladder and eight-tick octave. No downstream uses are recorded, so the result functions as an internal consistency check rather than a lemma for further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.