module module high

`IndisputableMonolith.ILG.Kernel`

The ILG kernel module supplies the parameter bundle and kernel function for the infra-luminous gravity model with values fixed by recognition science constants. Cosmologists building modified Poisson equations or growth corrections cite it to anchor the dimensionless scale and multiplier. The module consists of definitions for the kernel parameters together with direct substitution lemmas establishing positivity and monotonicity.

claimThe recognition science kernel parameters fix the multiplier $K(a)$ in the modified Poisson equation with $K(1)=1$, $K(a) > 1$ for $a > 1$, and monotonic increase in $a$, using the time quantum $τ_0 = 1$ and the eight-tick octave.

background

The module resides in the ILG domain and imports the fundamental RS time quantum $τ_0 = 1$ tick from the Constants module. It introduces the kernel parameter bundle that encodes the dimensionless variable $X = k τ_0 / a$ together with the explicit RS-derived values for the growth correction exponent and the Poisson multiplier. These objects set the scale for the infra-luminous modification while remaining inside the recognition science forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the CPM instance for ILG, the first-order growth ODE prefactor, the ISW sign logic, the Poisson kernel statement, the reciprocity variable, and the optical rescaling extension. It supplies the concrete constants required to instantiate the coercive projection framework and to close the parameter choice in the recognition science chain.

scope and limits

Does not derive the kernel form from the recognition composition law.
Does not compute numerical values outside the explicit parameter bundle.
Does not address scale-dependent or time-dependent generalizations of the kernel.

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.ILG.CPMInstance module_import
IndisputableMonolith.ILG.GrowthODE module_import
IndisputableMonolith.ILG.ISWSign module_import
IndisputableMonolith.ILG.PoissonKernel module_import
IndisputableMonolith.ILG.Reciprocity module_import
IndisputableMonolith.Relativity.Cosmology.OpticalExtension module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (37)

structure KernelParams L39
def rsKernelParams L54
def eightTickKernelParams L64
def kernel L79
def kernelAtRefK L83
lemma kernelAtRefK_eq L86
theorem kernel_pos L93
theorem kernel_ge_one L105
theorem kernel_at_ratio_one_alpha_zero L117
theorem kernel_eq_one_of_C_zero L127
theorem kernel_mono_in_a L135
theorem rsKernelParams_alpha L164
theorem rsKernelParams_C L168
theorem eightTickKernelParams_C L172
theorem kernel_ratio_dimensionless L178
structure SelfSimilarKernel L185
theorem alpha_from_self_similarity L194
def kernel_perturbation L245
def kernel_background L254
theorem kernel_background_eq_one L256
def kernel_with_Hubble L260
theorem kernel_perturbation_eq_kernel_of_ge L265
theorem kernel_perturbation_at_IR_floor L274
theorem kernel_perturbation_pos L282
theorem kernel_perturbation_ge_one L294
theorem kernel_perturbation_bounded_above L313
theorem kernel_with_Hubble_bounded_above L346
theorem kernel_background_independent_of_params L357
def mode_partition L367
theorem mode_partition_eq L370
theorem mode_partition_homogeneous L378
def kernel_dynamical_time L395
theorem kernel_dynamical_time_pos L399
theorem kernel_dynamical_time_ge_one L411
theorem kernel_dynamical_time_stationary L426
structure CausalityBoundsCert L446
def causalityBoundsCert L470