rsKernelParams_alpha
plain-language theorem explainer
The declaration shows that for any positive real τ₀ the alpha field inside the RS kernel parameters equals the locked constant (1 − 1/φ)/2. Workers on infra-luminous gravity models cite it to confirm the exponent matches the self-similar derivation from the Recognition forcing chain. The proof reduces to reflexivity because rsKernelParams is constructed to carry exactly this alpha value.
Claim. For every positive real number $τ_0$, the exponent $α$ extracted from the RS kernel parameters equals $(1 - 1/φ)/2$.
background
The ILG kernel is the function w(k, a) = 1 + C · (a / (k τ₀))^α. The module fixes α to the RS-canonical value derived from self-similarity. Upstream, alphaLock is defined as (1 − 1/φ)/2 and tau0 supplies the fundamental tick duration in RS-native units. The sibling definition rsKernelParams packages these constants together with the positivity hypothesis on τ₀.
proof idea
The proof is a one-line term-mode reflexivity that applies the definition of rsKernelParams directly to its alpha component.
why it matters
It locks the kernel exponent to the value required by the Recognition Science self-similarity step (T5 J-uniqueness and T6 phi fixed point). The result supports the module's listed properties on kernel positivity, reduction to unity at reference scale, and monotonicity. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.