pith. machine review for the scientific record. sign in
def definition def or abbrev

ilgSpatialKernelCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 273def ilgSpatialKernelCert : ILGSpatialKernelCert where
 274  closed_form := C_kernel_eq_two_minus_phi

proof body

Definition body.

 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. -/

depends on (30)

Lean names referenced from this declaration's body.