alpha_from_self_similarity
plain-language theorem explainer
The theorem establishes that any self-similar ILG kernel whose exponent is fixed to (1 - 1/phi)/2 equals the canonical locked value alphaLock. ILG cosmologists cite it to anchor the perturbation exponent from the phi fixed point. The proof is a one-line simplification that equates the hypothesis directly to the definition of alphaLock.
Claim. Let $K$ be a self-similar kernel with exponent $alpha$. If $alpha = (1 - phi^{-1})/2$, then $alpha$ equals the locked constant $alpha_{lock}$.
background
The ILG kernel takes the form $w(k,a) = 1 + C (a/(k tau_0))^alpha$, where $tau_0$ is the fundamental recognition tick. SelfSimilarKernel is the structure that encodes the scaling property: the kernel evaluated at scale factor $phi a$ equals the original kernel scaled by $phi^alpha$. The upstream constant alphaLock is defined exactly as $(1 - 1/phi)/2$, the value forced by the phi fixed-point equation $phi^2 = phi + 1$.
proof idea
The proof is a one-line term-mode simplification that substitutes the constraint hypothesis into the definition of alphaLock and verifies syntactic identity.
why it matters
This result discharges the placeholder derivation noted in the SelfSimilarKernel structure, confirming the exponent matches the locked value used throughout the kernel module. It supports downstream kernel properties such as positivity and monotonicity in scale factor. In the Recognition framework it instantiates the T6 self-similar fixed point for the ILG exponent, consistent with the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.