module module high

`IndisputableMonolith.Gravity.ILGSpatialKernel`

The ILGSpatialKernel module sets the spatial kernel amplitude to C = φ^{-2} inside the ILG gravity construction. Gravity modelers using Recognition Science would cite it for scaling spatial terms in the phi-ladder. The module is a definition block that introduces C and records its immediate algebraic properties.

claimThe spatial kernel amplitude satisfies $C = \phi^{-2}$.

background

Recognition Science builds gravity from the J-cost functional and the self-similar fixed point phi. The module imports the time quantum τ₀ = 1 tick, the Cost module that supplies J-cost, and the base ILG construction. It places the spatial kernel inside the eight-tick octave with D = 3 spatial dimensions.

The kernel amplitude C = φ^{-2} supplies the scaling factor for spatial contributions. Sibling declarations then record equalities such as C_kernel_eq_two_minus_phi and inequalities that bound C inside the allowed band.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the spatial kernel amplitude required by the ILG gravity model. It supports downstream calculations that combine the kernel with the Recognition Composition Law and the phi-ladder mass formula. The placement inside the forcing chain (T5–T8) fixes the numerical value once phi is adopted as the fixed point.

scope and limits

Does not derive C from the J functional equation.
Does not treat the temporal kernel.
Does not compute numerical predictions for G or alpha.
Does not address higher-dimensional extensions.

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