ilgSpatialKernelCert
plain-language theorem explainer
The master certificate for the ILG spatial-kernel amplitude is inhabited by supplying the closed form C equals 2 minus phi together with positivity, budget, band, factorization, and exclusion clauses. Researchers modeling modified Newtonian dynamics or SPARC rotation curves would cite this result to fix the kernel amplitude at approximately 0.382. The construction is a direct structure instance that assembles the six clauses from the half-rung budget identity and the relation phi squared equals phi plus one.
Claim. The ILG spatial kernel amplitude satisfies $C = 2 - ϕ$, $0 < C$, the half-rung budget identity $J(ϕ) + C = 1/2$, the numerical band $0.380 < C < 0.390$, the factorization $C = w · w$ for channel weight $w$, and excludes the competing value by violating the budget.
background
In the Information-Limited Gravity framework the Fourier-space kernel takes the form $w_{ker}(k) = 1 + C · (k_0/k)^α$ with exponent $α ≈ 0.191$. The amplitude $C$ is fixed by the half-rung budget identity $J(ϕ) + C = 1/2$, which follows from the defining relation $ϕ^2 = ϕ + 1$ and the J-cost definition $J(ϕ) = ϕ - 3/2$. This module resolves an earlier ambiguity between $C = ϕ^{-2}$ (from three-channel factorization) and $C = ϕ^{-3/2}$ by enforcing the budget constraint. Upstream results include the rung definition and the BIT kernel families that supply the functional form.
proof idea
The definition constructs an instance of the ILGSpatialKernelCert structure. It assigns the closed_form field to the theorem C_kernel_eq_two_minus_phi, which proves C equals 2 minus phi by algebraic manipulation of phi squared equals phi plus one. The remaining fields are filled by direct references to sibling theorems: positivity from C_kernel_pos, budget from half_rung_budget, band from C_kernel_band, factorization from three_channel_factorization, and exclusion from C_competing_violates_budget.
why it matters
This declaration supplies the inhabited master certificate that selects $C = ϕ^{-2}$ as the unique amplitude consistent with the Recognition Composition Law and the half-rung budget. It closes the ambiguity noted in the Entropy paper (Simons et al. 2026) versus Gravity_From_Recognition (Washburn 2026). The result anchors the ILG modification of Newtonian gravity and is consistent with the SPARC empirical fit A_fit = 0.38. No downstream uses are recorded yet; it serves as a foundational certificate for subsequent gravity derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.