ilg_spatial_kernel_one_statement
The theorem fixes the ILG spatial-kernel amplitude at C = 2 - φ, shows it satisfies the half-rung budget J(φ) + C = 1/2, factors as the square of the per-channel weight 1/φ, lies in the interval (0.380, 0.390), and excludes the competing value φ^{-3/2}. Galaxy rotation-curve modelers fitting SPARC data would cite the result to anchor the kernel amplitude from the Recognition Science cost structure. The proof is a single term that assembles the closed-form identity, positivity, budget equality, numerical bounds, factorization, and violation from
claimLet C = φ^{-2} be the spatial-kernel amplitude in w_ker(k) = 1 + C (k_0/k)^α and let J(φ) = φ - 3/2 be the first-rung J-cost penalty. Then C = 2 - φ, 0 < C, J(φ) + C = 1/2, 0.380 < C < 0.390, C = w^2 where w = φ^{-1}, and J(φ) + C' > 1/2 for the competing amplitude C' = φ^{-3/2}.
background
The module formalizes the Information-Limited Gravity kernel modification w_ker(k) = 1 + C (k_0/k)^α with α already fixed at (1 - φ^{-1})/2. C_kernel is defined as φ^{-2} and Jphi_penalty as φ - 3/2; their sum equals 1/2 by the algebraic identity that follows from φ^2 = φ + 1 alone. Channel_weight is defined as φ^{-1}, supplying the three-channel factorization C = (φ^{-1})^2. The competing amplitude C_kernel_competing is defined as φ^{-3/2}. Upstream lemmas establish positivity of C, the band bounds, and the strict budget violation for the competing value.
proof idea
The proof is a term-mode wrapper that directly constructs the six-way conjunction from the sub-lemmas C_kernel_eq_two_minus_phi, C_kernel_pos, half_rung_budget, the two components of C_kernel_band, three_channel_factorization, and C_competing_violates_budget.
why it matters in Recognition Science
This declaration resolves the prior ambiguity between the entropy-paper value C = φ^{-2} (from three-channel factorization) and the competing C = φ^{-3/2} by enforcing the half-rung budget identity. It places the kernel amplitude inside the Recognition Science forcing chain at the J-uniqueness and φ-fixed-point steps, supplies the numerical match to SPARC fits A_fit ≈ 0.38, and removes an open parameter from ILG gravity models. No downstream theorems are recorded yet, but the result is the canonical statement for any later derivation of the full ILG Poisson equation.
scope and limits
- Does not derive the kernel exponent α.
- Does not prove the full ILG gravity field equations.
- Does not address renormalization or higher-order corrections.
- Does not connect the kernel to the eight-tick octave or spatial dimension D = 3.
formal statement (Lean)
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 :=
proof body
Term-mode proof.
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