module module moderate

`IndisputableMonolith.Gravity.ILGSpatialKernel`

Defines the ILG spatial-kernel amplitude C = φ^{-2} and packages its elementary identities, positivity/band bounds, and the half-rung complement with the J(φ) penalty. Gravity workers cite it for local ledger accounting in Information-Limited Gravity. Proofs are short algebraic reductions from the golden-ratio equation and the J-cost definition.

claimThe spatial-kernel amplitude is $C=\varphi^{-2}$. The module records the companion $\alpha$-kernel data, the penalty $J(\varphi)$, the identity $C=2-\varphi$, the bounds $0<C<1/2$, the evaluations $J(\varphi)=\varphi-3/2=J_{\mathrm{cost}}(\varphi)$, and the half-rung budget $C+J(\varphi)=1/2$.

background

In Recognition Science gravity, ILG (Information-Limited Gravity) uses a spatial kernel whose amplitude is fixed by the golden ratio. Here $\varphi$ is the self-similar fixed point forced at T6 of the unified forcing chain, and the cost is the unique J from T5, $J(x)=(x+x^{-1})/2-1$.

The module imports Constants (for $\varphi$ and the RS time quantum), Cost (for $J$), and Gravity.ILG. It introduces $C=\varphi^{-2}$ as the spatial-kernel amplitude together with the $J(\varphi)$ penalty that pairs against it in the local half-rung ledger.

Sibling declarations cover positivity, the strict band $C<1/2$, the rewrite $C=2-\varphi$, and the complement identity that closes the half-rung budget.

proof idea

Definition-plus-lemmas module, not a single deep theorem. $C$ is defined as $\varphi^{-2}$. Identities such as $C=2-\varphi$ reduce by the golden-ratio relation $\varphi^2=\varphi+1$. Positivity and $C<1/2$ are immediate comparisons from $\varphi>1$. The penalty side equates $J(\varphi)$ to $\varphi-3/2$ and to $J_{\mathrm{cost}}(\varphi)$; the half-rung budget and the complement $C+J(\varphi)=1/2$ are then one- or two-line algebraic closures.

why it matters in Recognition Science

Supplies the numerical kernel amplitude used throughout ILG gravity constructions. The half-rung budget and the complement of $C$ against $J(\varphi)$ give the local ledger that balances spatial-kernel weight against the cost penalty at $\varphi$. No used-by edges are recorded yet in the mirror graph; the module is infrastructure for ILG force-law and rotation-curve work. It sits on the T5/T6 landmarks (J-uniqueness and $\varphi$ forced) without touching the eight-tick or $D=3$ steps.

scope and limits

Does not derive the ILG force law or Poisson structure.
Does not prove dynamical stability of the spatial kernel.
Does not fit C to observed rotation curves.
Does not address temporal, eight-tick, or D=3 structure.
Does not claim uniqueness of C beyond the φ-fixed definition.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Gravity.ILG module_import

declarations in this module (23)

def C_kernel L85
def alpha_kernel L88
def Jphi_penalty L92
theorem C_kernel_eq_two_minus_phi L98
theorem C_kernel_pos L115
theorem C_kernel_lt_half L121
theorem C_kernel_band L130
theorem Jphi_penalty_eq_phi_minus_three_halves L144
theorem Jphi_penalty_eq_Jcost_phi L148
theorem half_rung_budget L159
theorem half_rung_budget_doubled L164
theorem C_is_complement_of_Jphi L170
theorem half_rung_components_band L176
def C_kernel_competing L195
theorem C_kernel_competing_pos L198
theorem C_competing_gt_C_kernel L204
theorem C_competing_violates_budget L213
def channel_weight L228
theorem channel_weight_eq L231
theorem three_channel_factorization L245
structure ILGSpatialKernelCert L264
def ilgSpatialKernelCert L273
theorem ilg_spatial_kernel_one_statement L293