C_is_complement_of_Jphi
plain-language theorem explainer
The spatial-kernel amplitude C equals one half minus the first-rung J-cost penalty J(phi). Gravity modelers cite this to anchor the ILG kernel amplitude at phi to the minus two from the half-rung budget. The proof is a one-line algebraic rearrangement of the half-rung budget identity via linarith.
Claim. $C = 1/2 - J(φ)$ where $C = φ^{-2}$ is the spatial-kernel amplitude and $J(φ) = φ - 3/2$ is the first-rung cost penalty.
background
The ILG module defines the Fourier-space kernel modification as w_ker(k) = 1 + C (k_0/k)^α with α ≈ 0.191. The amplitude C is introduced as the definition C_kernel := phi^(-2). The half-rung budget identity asserts that the J-cost penalty plus this amplitude sums exactly to one half. This identity follows directly from the golden-ratio relation φ² = φ + 1 and selects C = φ^{-2} over the alternative φ^{-3/2}.
proof idea
The proof invokes the upstream half_rung_budget theorem (Jphi_penalty + C_kernel = 1/2) and applies linarith to rearrange into the stated complement form.
why it matters
This result fixes the kernel amplitude C at φ^{-2} for the ILG spatial kernel by complementarity within the half-rung budget. It resolves the documented ambiguity between the entropy-paper value φ^{-2} and the earlier gravity-from-recognition proposal φ^{-3/2}. The identity supports downstream kernel constructions in Gravity.ILG and aligns with Recognition Science landmarks T5 (J-uniqueness) and T6 (phi fixed point).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.