alpha_kernel
plain-language theorem explainer
The declaration supplies the kernel exponent α = (1 - φ^{-1})/2 for the ILG Fourier correction to Newtonian gravity. Workers on Information-Limited Gravity cite it when writing the spatial kernel w_ker(k) = 1 + C (k_0/k)^α with the amplitude C derived elsewhere in the module. It is a direct algebraic definition that matches the value already obtained as alphaLock.
Claim. The kernel exponent is defined by $α = (1 - φ^{-1})/2$.
background
The module sets the ILG spatial kernel in Fourier space as w_ker(k) = 1 + C · (k_0 / k)^α, where the exponent α is supplied here and the amplitude C = φ^{-2} is obtained from the half-rung budget identity J(φ) + φ^{-2} = 1/2. This identity follows from φ² = φ + 1 and equates the J-cost penalty for crossing one φ-rung with the cost-saving from finite-latency closure. The exponent matches the value previously fixed in Gravity.GravityParameters.alpha_gravity and Constants.alphaLock. Upstream cost definitions supply the J-cost of recognition events while rung definitions fix the integer ladder positions used in mass and sector calculations.
proof idea
One-line definition that directly encodes the algebraic expression (1 - 1/phi)/2.
why it matters
It supplies the numerical exponent α ≈ 0.191 required by the ILG kernel form already stated in the module doc-comment. The value is consistent with the Recognition Science forcing chain (T5 J-uniqueness, T6 phi fixed point) and the Recognition Composition Law. It supports the module's resolution of the prior C ambiguity between φ^{-2} and φ^{-3/2} by fixing the complementary half-rung budget. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.