cLag_from_phi
plain-language theorem explainer
cLag_from_phi supplies the explicit expression for the ILG lag constant as the fifth negative power of the golden ratio phi, yielding a value near 0.09. Researchers deriving general relativity limits from Recognition Science would reference this when bounding perturbative couplings in the ILG model. The definition is a direct assignment drawn from the Constants structure with no additional computation or lemmas required.
Claim. Let $C_{lag} := phi^{-5}$, where $phi$ is the golden ratio fixed point satisfying the self-similar equation from the Recognition Composition Law.
background
The module proves that ILG parameters alpha and C_lag derived from Recognition Science remain small enough to support perturbative treatment in the general relativity limit. The lag constant originates from the coherence quantum energy scale stated as phi to the negative five in the source derivation. Upstream results in the Constants structure establish positivity of phi together with the fact that phi exceeds one, which together guarantee that the negative exponent produces a positive real strictly less than one.
proof idea
This is a direct definition that assigns the real number obtained by raising Constants.phi to the real power negative five. No tactics are invoked beyond the constant lookup and real exponentiation.
why it matters
This definition supplies the concrete value of C_lag required by GRLimitParameterFacts and the theorems proving rs_params_small_proven together with coupling_product_small_proven. It realizes the RS-native unit choice in which the lag derives from the phi-ladder at rung negative five, consistent with the self-similar fixed point and eight-tick octave in the forcing chain. The module documentation records that tighter bounds on the product of alpha and C_lag below 0.02 remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.