C_kernel
plain-language theorem explainer
The spatial-kernel amplitude in the ILG gravity model is defined as C = φ^{-2}. Researchers constructing Fourier-space modifications to Newtonian gravity in Recognition Science would cite this value when writing the kernel w_ker(k) = 1 + C (k_0/k)^α. The definition is introduced directly from the golden-ratio recurrence and is immediately used to prove the half-rung budget identity J(φ) + C = 1/2.
Claim. In the ILG framework the spatial-kernel amplitude is defined by the equation $C = varphi^{-2}$.
background
The ILG framework modifies the Newton-Poisson relation in Fourier space by the kernel w_ker(k) = 1 + C · (k_0 / k)^α, where the exponent α = (1 - 1/φ)/2 is supplied by the locked constant alphaLock. The amplitude C is fixed by the structural identity J(φ) + C = 1/2 that follows from φ² = φ + 1 alone; this identity identifies C as the cost-saving term complementary to the rung-crossing penalty J(φ) = φ - 3/2. The module imports the ILG kernel definition, the BIT kernel families, and the simplicial-continuum bridge to ensure the amplitude is consistent with the cost function J and the self-reference axioms.
proof idea
This is a direct definition C_kernel := phi ^ (-(2 : ℝ)). No lemmas are invoked inside the declaration itself; the value is supplied for immediate use in the algebraic identities proved downstream.
why it matters
The definition supplies the amplitude that appears inside the ILG kernel and is shown by downstream results (C_is_complement_of_Jphi, C_kernel_eq_two_minus_phi, C_competing_violates_budget) to be the unique value compatible with the half-rung budget. It resolves the numerical discrepancy between the entropy-paper value φ^{-2} and the earlier Gravity_From_Recognition proposal φ^{-3/2} by enforcing the identity J(φ) + C = 1/2. The choice sits after the self-similar fixed point φ is obtained in the forcing chain and before the spatial-band and positivity theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.