C_kernel_band
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 in Recognition Science
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.
scope and limits
- Does not derive the closed form C = 2 - phi.
- Does not establish the half-rung budget identity.
- Does not constrain the kernel exponent alpha.
- Does not address empirical data fitting beyond the stated band.
Lean usage
refine ⟨?_, ?_, C_kernel_band.1, C_kernel_band.2⟩formal statement (Lean)
130theorem C_kernel_band :
131 (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ) := by
proof body
Term-mode proof.
132 rw [C_kernel_eq_two_minus_phi]
133 have h_lo : 1.61 < phi := phi_gt_onePointSixOne
134 have h_hi : phi < 1.62 := phi_lt_onePointSixTwo
135 refine ⟨?_, ?_⟩ <;> linarith
136
137/-! ## §4. The half-rung budget identity
138
139The crown identity: `J(φ) + C = 1/2`. The penalty for one rung crossing
140plus the kernel-amplitude saving fills exactly the half-rung budget.
141-/
142
143/-- The first-rung J-cost penalty has closed form `φ - 3/2`. -/