ilg_alpha_eq_rs
plain-language theorem explainer
The declaration shows that the fine-structure exponent alpha extracted from ILG kernel parameters at any positive tick duration tau0 equals the RS-locked value alphaLock. Researchers verifying consistency of the CPM coercive model for infra-luminous gravity would cite this equality when confirming constant alignment with Recognition Science. The proof is a direct reflexivity reduction after the kernel parameters are unfolded.
Claim. Let $tau_0 > 0$. The fine-structure exponent $alpha$ in the ILG kernel parameters at $tau_0$ equals the canonical locked value $alpha_{lock} = (1 - phi^{-1})/2$.
background
The module supplies a concrete CPM.Model instance for the ILG gravitational modification, using the abstract coercive projection framework from CPM/LawOfExistence. It fixes eight-tick aligned constants: K_net = (9/7)^2 from covering number at epsilon = 1/8, C_proj = 2 from the second derivative J''(1) = 1, C_eng = 1, and c_min = 49/162. The function rsKernelParams builds the ILG kernel from the fundamental tick duration tau0 (defined as 1 in RS-native units) and the positivity hypothesis. Upstream, alphaLock is the algebraic definition (1 - 1/phi)/2 that serves as the canonical bridge value for the fine-structure constant in RS units.
proof idea
The proof is a one-line reflexivity wrapper. It holds immediately once rsKernelParams tau0 h is unfolded to expose the alpha field and alphaLock is recognized as the matching constant definition.
why it matters
The equality closes the constant-matching step required for the ILG instantiation of the CPM model, directly supporting the module's main results ilgModel and ilg_coercivity. It aligns the ILG exponent with the RS eight-tick octave and the alphaLock bridge identity, ensuring the kernel satisfies the Recognition Composition Law constraints on J-cost. No open scaffolding remains for this particular matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.