Pith. sign in
module module moderate

IndisputableMonolith.Gravity.ILGSpatialKernel

show as:
view Lean formalization →

Defines the ILG spatial-kernel amplitude C = φ⁻² together with the companion penalty J_φ and half-rung budget identities used in galactic rotation-curve modeling. Gravity and ILG workers cite it for the numerical band on C and the exact link C + J(φ) = 1. Most statements are short algebraic rewrites from the golden-ratio minimal polynomial and the J-cost definition.

claimThe spatial-kernel amplitude is the constant $C = \varphi^{-2}$. Companion objects are the kernel weight $\alpha$, the penalty $J_\varphi := J(\varphi)$, and the half-rung budget. The module records $C = 2 - \varphi$, $0 < C < 1/2$, the exact identity $C + J(\varphi) = 1$, and $J(\varphi) = \varphi - 3/2$.

background

Information-Limited Gravity (ILG) replaces a dark-matter halo with a recognition kernel whose spatial amplitude is fixed by the golden ratio $\varphi$, the unique positive solution of $\varphi^2 = \varphi + 1$. In RS-native units the cost functional is $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced unique by the T5 step of the unified forcing chain.

This module sits downstream of Constants (which supplies $\varphi$ and the tick $\tau_0$) and Cost (which supplies $J$). It specialises those primitives to the radial kernel that multiplies the baryonic acceleration in the ILG force law. The sibling definitions introduce $C_{\mathrm{kernel}} = \varphi^{-2}$, an auxiliary $\alpha_{\mathrm{kernel}}$, the penalty $J_\varphi$, and the half-rung budget that appears when the eight-tick octave is halved.

proof idea

Definition module with a thin layer of algebraic lemmas. $C = \varphi^{-2}$ is unfolded via $\varphi^2 = \varphi + 1$ to obtain the closed form $C = 2 - \varphi$. Positivity and the strict bound $C < 1/2$ are immediate from $1 < \varphi < 2$. The penalty identities rewrite $J(\varphi)$ by direct substitution into the cost formula, yielding $J(\varphi) = \varphi - 3/2$. The complement relation $C + J(\varphi) = 1$ is then a one-line arithmetic check. Half-rung budget statements double or halve the same constants; no analytic estimates or external analysis are required.

why it matters in Recognition Science

Supplies the numerical kernel amplitude that every ILG rotation-curve prediction multiplies against baryonic surface density. The exact band $0 < C < 1/2$ and the complement identity $C = 1 - J(\varphi)$ let downstream gravity theorems replace floating parameters by pure $\varphi$-expressions, keeping the theory inside the RS forcing chain (T5 J-uniqueness, T6 $\varphi$ fixed point). Although the module currently has no recorded reverse edges, its siblings are the natural inputs to any theorem that assembles the full ILG acceleration law or compares the kernel against SPARC-style data. The construction is closed: every identity is proved from the golden-ratio equation and the definition of $J$, with no remaining sorry.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (23)