C_kernel_pos
plain-language theorem explainer
The declaration proves that the ILG spatial kernel amplitude C = φ^{-2} is strictly positive. Gravity modelers using the modified Poisson kernel w_ker(k) = 1 + C (k0/k)^α cite it to confirm the correction term stays positive. The argument rewrites via the closed form C = 2 - φ, invokes the bound φ < 2, and concludes by linear arithmetic.
Claim. $0 < C$ where $C = ϕ^{-2}$ and $ϕ$ is the golden ratio fixed point satisfying $ϕ^2 = ϕ + 1$.
background
The module formalizes the ILG spatial-kernel amplitude in the Fourier modification w_ker(k) = 1 + C (k0/k)^α, deriving C = φ^{-2} from the half-rung budget identity J(φ) + C = 1/2. This identity follows from φ^2 = φ + 1 alone and shows complementarity between the rung-crossing cost J(φ) = φ - 3/2 and the latency-closure saving C = 2 - φ. The upstream lemma phi_lt_two states φ < 2 and is proved from the quadratic definition of φ by comparing square roots.
proof idea
The proof is a short reduction that rewrites the goal with the sibling equality C_kernel_eq_two_minus_phi, applies the imported lemma phi_lt_two, and finishes with linarith.
why it matters
Positivity of C is required by the master certificate ilgSpatialKernelCert and by the consolidated theorem ilg_spatial_kernel_one_statement, which lists it among the five properties of the amplitude. It confirms that the value forced by the half-rung budget (T5 J-uniqueness and T6 phi fixed point) lies in the admissible range and matches the three-channel factorization C = φ^{-1} · φ^{-1}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.