C_competing_violates_budget
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 in Recognition Science
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.
scope and limits
- Does not prove the half-rung budget identity itself.
- Does not establish the three-channel factorization.
- Does not match the amplitude to SPARC data.
- Does not constrain the kernel exponent α.
formal statement (Lean)
213theorem C_competing_violates_budget :
214 Jphi_penalty + C_kernel_competing > 1 / 2 := by
proof body
Term-mode proof.
215 have h1 : Jphi_penalty + C_kernel = 1 / 2 := half_rung_budget
216 have h2 : C_kernel < C_kernel_competing := C_competing_gt_C_kernel
217 linarith
218
219/-! ## §6. Structural three-channel factorization sketch
220
221The amplitude `C = φ⁻²` admits the structural decomposition
222 `C = (longitudinal weight) × (transverse-collective weight) = φ⁻¹ · φ⁻¹`
223in `D = 3` spatial dimensions. We record the per-channel weight and
224the product as named definitions for transparency.
225-/
226
227/-- The per-channel ladder weight: `φ⁻¹`. One step on the φ-ladder. -/