C_competing_violates_budget
plain-language theorem explainer
Physicists deriving the ILG spatial kernel amplitude cite this result to show that the competing value φ^{-3/2} together with the J-penalty exceeds the half-rung budget. The declaration rules out C = φ^{-3/2} in favor of the forced value φ^{-2}. Its proof combines the half-rung equality with a strict inequality between the two amplitudes and applies linear arithmetic.
Claim. $J(φ) + φ^{-3/2} > 1/2$, where $J(φ) = φ - 3/2$ is the first-rung J-cost penalty.
background
The module derives the ILG spatial-kernel amplitude C = φ^{-2} from the half-rung budget identity J(φ) + C = 1/2, which follows from φ² = φ + 1 alone and identifies C with 2 - φ. J(φ) = φ - 3/2 is the first-rung cost penalty, while the competing amplitude is defined as C' = φ^{-3/2}. The local setting contrasts the structurally forced C with the alternative value drawn from an earlier three-channel argument.
proof idea
The proof recalls the equality Jphi_penalty + C_kernel = 1/2 from the half-rung budget lemma, invokes the strict inequality C_kernel < C_kernel_competing, and concludes via linarith.
why it matters
The theorem eliminates the competing amplitude φ^{-3/2} by budget violation and feeds the master certificate ilgSpatialKernelCert together with the consolidated one-statement theorem ilg_spatial_kernel_one_statement. It enforces the half-rung identity that selects C = φ^{-2} over φ^{-3/2}, consistent with the three-channel factorization C = φ^{-1} · φ^{-1} in D = 3 and the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.