C_kernel_band
plain-language theorem explainer
The theorem establishes that the ILG spatial kernel amplitude C satisfies 0.380 < C < 0.390. Physicists deriving modified gravity kernels in the Recognition Science framework cite this bound to anchor the amplitude in the half-rung budget identity. The proof reduces the claim to the closed form C = 2 - phi via rewrite and applies linear arithmetic to the golden ratio interval 1.61 < phi < 1.62.
Claim. $0.380 < C < 0.390$, where $C = 2 - 1.618...$ is the spatial kernel amplitude defined by $C = 1.618...^{-2}$ and the golden ratio satisfies $1.61 < 1.618... < 1.62$.
background
The module derives the ILG spatial kernel amplitude in the Fourier modification $w_ker(k) = 1 + C · (k_0/k)^α$ with $α ≈ 0.191$. The amplitude is defined as $C = phi^{-2}$. The structural core is the half-rung budget identity $J(phi) + C = 1/2$, which follows from $phi^2 = phi + 1$ alone and states that the first-rung J-cost penalty plus the kernel saving equals the half-rung interval. Upstream lemmas supply the tight bounds $1.61 < phi$ and $phi < 1.62$.
proof idea
The term proof rewrites C_kernel to 2 - phi using the equality C_kernel_eq_two_minus_phi. It obtains the lower bound from phi_gt_onePointSixOne and the upper bound from phi_lt_onePointSixTwo. The refine tactic splits the conjunction and linarith discharges both inequalities by arithmetic on the interval.
why it matters
This numerical band populates the band field in the master certificate ilgSpatialKernelCert and is invoked in half_rung_components_band and the one-statement theorem ilg_spatial_kernel_one_statement. It supplies the numerical anchor confirming that C matches the SPARC empirical fit A_fit = 0.38 to better than 1 percent and closes the verification step for the half-rung budget identity in the ILG derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.