`ilg_spatial_kernel_one_statement`

proved

show as: view math explainer →

module: IndisputableMonolith.Gravity.ILGSpatialKernel
domain: Gravity
line: 293 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gravity.ILGSpatialKernel on GitHub at line 293.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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 ∧
 304    -- (6) Competing value violates budget
 305    Jphi_penalty + C_kernel_competing > 1 / 2 :=
 306  ⟨C_kernel_eq_two_minus_phi, C_kernel_pos, half_rung_budget,
 307   C_kernel_band.1, C_kernel_band.2, three_channel_factorization,
 308   C_competing_violates_budget⟩
 309
 310end
 311
 312end ILGSpatialKernel
 313end Gravity
 314end IndisputableMonolith

papers checked against this theorem

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