ilgSpatialKernelCert

formal source

 270  competing_excluded : Jphi_penalty + C_kernel_competing > 1 / 2
 271
 272/-- The master certificate is inhabited. -/
 273def ilgSpatialKernelCert : ILGSpatialKernelCert where
 274  closed_form := C_kernel_eq_two_minus_phi
 275  positivity := C_kernel_pos
 276  budget := half_rung_budget
 277  band := C_kernel_band
 278  factorization := three_channel_factorization
 279  competing_excluded := C_competing_violates_budget
 280
 281/-! ## §8. Single-statement summary -/
 282
 283/-- **ILG SPATIAL-KERNEL AMPLITUDE: ONE-STATEMENT THEOREM.**
 284
 285The spatial-kernel amplitude `C = φ⁻²` in
 286`w_ker(k) = 1 + C · (k_0/k)^α` is structurally forced by the half-rung
 287budget identity `J(φ) + C = 1/2`, has the closed form `C = 2 - φ`,
 288admits the three-channel factorization `C = (1/φ)·(1/φ)`, lies in
 289the numerical band `(0.380, 0.385)` from `φ ∈ (1.61, 1.62)`, and
 290matches the SPARC empirical fit `A_fit = 0.38` to better than 1%.
 291The competing value `C' = φ⁻³ᐟ² ≈ 0.486` violates the budget
 292identity and is excluded. -/
 293theorem ilg_spatial_kernel_one_statement :
 294    -- (1) Closed form
 295    C_kernel = 2 - phi ∧
 296    -- (2) Positivity
 297    0 < C_kernel ∧
 298    -- (3) Half-rung budget identity
 299    Jphi_penalty + C_kernel = 1 / 2 ∧
 300    -- (4) Numerical band
 301    (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ) ∧
 302    -- (5) Three-channel factorization
 303    C_kernel = channel_weight * channel_weight ∧