pith. sign in
theorem

kernel_background_eq_one

proved
show as:
module
IndisputableMonolith.ILG.Kernel
domain
ILG
line
256 · github
papers citing
none yet

plain-language theorem explainer

The ILG background kernel equals one by definition, representing the J-cost minimum on the homogeneous FRW background with zero ledger gradient flow. Cosmologists in the Recognition Science framework cite this result when the perturbation term vanishes and the Poisson equation reduces to unmodified GR. The proof is a direct reflexivity step on the explicit constant definition of kernel_background.

Claim. In the Infra-Luminous Gravity model the background kernel satisfies $w_0 = 1$, where the homogeneous Friedmann-Robertson-Walker state sits at the minimum of the shifted cost $H(x) = J(x) + 1$ with no additional recognition lag.

background

The ILG kernel is given by $w(k,a) = 1 + C · (a/(k τ₀))^α$ with α = (1 - 1/φ)/2. The background specialization sets the perturbation coefficient to zero, yielding the constant function 1. This module formalizes the Infra-Luminous Gravity kernel and records that it reduces to 1 at the reference scale a = k τ₀. The shifted cost is defined by H(x) = J(x) + 1; under this reparametrization the Recognition Composition Law becomes the d'Alembert identity H(xy) + H(x/y) = 2 H(x) H(y). The background kernel corresponds to equilibrium of the recognition operator on a homogeneous state, so the background Poisson equation remains standard GR.

proof idea

The proof is a one-line term-mode reflexivity application to the definition of kernel_background, which is declared as the constant 1.

why it matters

This result is used to construct the causality bounds certificate that certifies positivity, lower bounds and Hubble saturation of the perturbed kernel. It fills the step in the ILG formalization where the homogeneous background incurs zero J-cost and the Poisson equation is unmodified standard GR. The declaration anchors the reduction to standard cosmology inside the Recognition Science framework at the J-uniqueness fixed point.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.