module module high

`IndisputableMonolith.Gravity.ILGSpatialKernel`

The module defines the spatial kernel amplitude C as phi to the minus two for use in ILG gravity defect calculations. Researchers modeling spatial components of Recognition Science gravity would reference it when assembling kernel amplitudes from the phi ladder. The module consists of definitions together with short algebraic verifications of positivity and complementarity properties.

claim$C = phi^{-2}$, where $phi$ denotes the self-similar fixed point of the Recognition Composition Law.

background

Recognition Science obtains all constants from the J-cost function obeying the Recognition Composition Law. The module imports the base time quantum tau_0 = 1 tick from Constants, the cost machinery from Cost, and the ILG framework. It introduces the spatial kernel amplitude C together with auxiliary objects such as alpha_kernel and Jphi_penalty that express penalties in terms of J-cost evaluated at phi.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The kernel supplies the spatial amplitude required by ILG gravity constructions and feeds sibling lemmas that relate C to two minus phi and to J-cost at phi. It anchors the spatial sector of the phi-ladder mass formula and the eight-tick octave structure.

scope and limits

Does not derive C from the T0-T8 forcing chain.
Does not treat time-dependent or vector kernels.
Does not compute numerical values outside the phi band.

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