alpha_kernel
plain-language theorem explainer
alpha_kernel supplies the kernel exponent α = (1 - φ^{-1})/2 for the Fourier modification in Information-Limited Gravity. Modelers writing w_ker(k) = 1 + C (k_0/k)^α cite it to fix the exponent at ≈0.191. The declaration is a direct definition that transcribes the closed-form expression already present in Constants.alphaLock.
Claim. The kernel exponent is defined by $α := (1 - φ^{-1})/2$.
background
The ILG module writes the Newton-Poisson source-potential relation in Fourier space as w_ker(k) = 1 + C · (k_0/k)^α. Here α is the kernel exponent while C = φ^{-2} is the amplitude fixed by the half-rung budget identity J(φ) + φ^{-2} = 1/2. The identity follows from φ² = φ + 1 alone and shows that the J-cost penalty for one rung and the finite-latency saving C are complementary contributions to the rung budget. Upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost that enters rung calculations; rung definitions from AnchorPolicy and RSBridge.Anchor label the discrete levels on the φ-ladder.
proof idea
Direct definition that transcribes the algebraic expression (1 - 1/phi)/2.
why it matters
The declaration fixes the exponent that appears in the ILG kernel w_ker(k) and cross-references the value already established in Constants.alphaLock. The surrounding module uses the half-rung budget to select C = φ^{-2} over the alternative φ^{-3/2} from earlier three-channel arguments. It participates in the forcing chain that derives the spatial kernel from J-uniqueness (T5) and the self-similar fixed point φ (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.