cLag_from_phi
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish any inequality bounds on the defined value.
- Does not incorporate other entries from the Constants structure such as Knet or Ceng.
- Does not perform numerical evaluation or approximation beyond the symbolic expression.
- Does not invoke the Recognition Composition Law directly.
formal statement (Lean)
28noncomputable def cLag_from_phi : ℝ :=
proof body
Definition body.
29 Constants.phi ^ (-5 : ℝ)
30
31/-- PROVEN: Both parameters are positive. -/