Clag
plain-language theorem explainer
Clag is the constant 1/φ^5 that supplies the amplitude scale for the ILG time-kernel. Gravity modelers and resonance calculations cite it when instantiating Params and verifying bounds on w_t. The declaration is a direct noncomputable abbreviation that imports phi from the sibling Constants module.
Claim. Let φ be the self-similar fixed point. Define Clag := 1/φ^5.
background
The Constants.ILG module introduces Clag together with alpha_locked. Phi is the fixed point forced at T6 of the UnifiedForcingChain and satisfies the self-similarity relation used throughout the Recognition framework. Clag therefore inherits the φ^5 scale that appears in the native-unit expressions for ħ and G.
proof idea
The declaration is a direct abbreviation that sets Clag equal to the reciprocal of phi raised to the fifth power; no lemmas or tactics are applied.
why it matters
Clag populates the Clag field of the Params structure in Gravity.ILG and is required by ParamProps, w_t_nonneg, w_t_ge_one, and w_t_with. It supplies the numerical prefactor in the power-law time-kernel that connects to the eight_tick_period theorem and the T7 eight-tick octave. The definition therefore closes the constant interface between the forcing chain and the ILG gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.