alpha_from_phi
plain-language theorem explainer
ILG exponent α is defined from the Recognition Science phi fixed point as (1 - phi inverse)/2. This locks the coupling in the GR limit parameters without free parameters. Researchers on inflation from J-cost or SPARC falsifiers cite it to enforce global-only policy. The definition is a direct one-line expression using the Constants structure.
Claim. $α = (1 - φ^{-1})/2$, where φ is the self-similar fixed point of the Recognition Composition Law.
background
The module on Parameter Limits derives ILG parameters directly from RS geometry to show they are small and perturbative. The Constants structure bundles CPM constants with phi and nonnegativity. The from theorem in PrimitiveDistinction supplies four structural conditions plus three definitional facts from seven axioms. C_lag is defined separately as phi to the minus five.
proof idea
This is a direct definition that sets the value to the algebraic expression (1 - 1/Constants.phi)/2. No tactics or lemmas are applied; it functions as a one-line wrapper for unfolding in downstream results.
why it matters
The definition supplies the locked alpha value in GlobalOnlyPolicy for the SPARC falsifier and in InflationFromJCostCert to certify zero free parameters in the inflationary chain. It realizes T5 J-uniqueness and T6 phi fixed point from the forcing chain, placing α ≈ 0.191 in the perturbative regime for the GR limit as stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.