 2615. **factorization**: `C = (1/φ) · (1/φ)` (three-channel decomposition).
 2626. **competing_excluded**: `C' = φ⁻³ᐟ²` violates the budget identity.
 263-/
 264structure ILGSpatialKernelCert where
 265  closed_form : C_kernel = 2 - phi
 266  positivity : 0 < C_kernel
 267  budget : Jphi_penalty + C_kernel = 1 / 2
 268  band : (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ)
 269  factorization : C_kernel = channel_weight * channel_weight
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.