C_kernel_pos
Positivity of the spatial-kernel amplitude C = phi^{-2} is established by this theorem. It is required when assembling the master certificate for the ILG spatial kernel and the consolidated one-statement summary. The proof rewrites C via its closed form 2 - phi, invokes the upstream inequality phi < 2, and concludes by linear arithmetic.
claimThe spatial-kernel amplitude satisfies $0 < C$ where $C = phi^{-2}$.
background
The module derives the ILG spatial-kernel amplitude from the half-rung budget identity. The kernel is written w_ker(k) = 1 + C (k_0/k)^alpha with amplitude C = phi^{-2}. The algebraic identity J(phi) + phi^{-2} = 1/2 follows from phi^2 = phi + 1 alone; it equates the J-cost penalty for one rung crossing to the cost-saving from finite-latency closure, so that the two contributions sum to the half-rung interval. C_kernel is defined as phi to the power -2. The positivity claim depends on the upstream lemma phi_lt_two, which states phi < 2 and is proved by comparing square roots in the explicit formula for phi.
proof idea
The proof rewrites the goal using the equality C_kernel_eq_two_minus_phi to obtain 0 < 2 - phi. It then applies the lemma phi_lt_two to obtain phi < 2 and finishes with linarith.
why it matters in Recognition Science
This result supplies the positivity component of the master certificate ilgSpatialKernelCert, which also records the closed form, half-rung budget, numerical band, and three-channel factorization. It is invoked by the one-statement theorem that consolidates the ILG spatial-kernel properties. The positivity confirms that the structurally forced value C = phi^{-2} is admissible in the Recognition Science framework, consistent with the phi-ladder and the half-rung budget identity derived from the golden-ratio relation.
scope and limits
- Does not derive the closed-form expression for C.
- Does not prove the half-rung budget identity itself.
- Does not address the kernel exponent alpha.
- Does not compare the value to SPARC empirical fits.
formal statement (Lean)
115theorem C_kernel_pos : 0 < C_kernel := by
proof body
Term-mode proof.
116 rw [C_kernel_eq_two_minus_phi]
117 have h := phi_lt_two
118 linarith
119
120/-- `C < 1/2` (strictly less than the half-rung budget). -/