Ilg Kernel Kernel Background Independent Of Params

The constant background

The Infra-Luminous Gravity (ILG) kernel is a function used to model how density fluctuations in the early universe grow. It takes a wave number k, a scale factor a, and a reference time scale τ₀, and returns a positive number that multiplies the background density. The kernel is written as w(k, a) = 1 + C · (a / (k τ₀))^α, where C is an amplitude constant and α is the ILG exponent, derived from self-similarity as α = (1 - 1/φ)/2. The leading 1 in this expression is the kernel background, a discrete record of the baseline value the kernel takes when the perturbation term vanishes.

The declaration kernel_background_independent_of_params is a theorem in the framework's machine-checked library of formal theorems. It states that for any choice of KernelParams, a structure holding the kernel's parameters, the kernel background equals 1. The proof is immediate: the background is defined to be 1, so the theorem holds by definition. This is not a numerical approximation or a fitted value; it is an exact identity that holds for every parameter set the model can express, including the Recognition Science parameter set where C = φ^(-3/2) and the eight-tick set where C = 49/162.

What the theorem does not claim is more interesting than what it does. It does not say the full kernel is independent of parameters; the perturbation term C · (a / (k τ₀))^α certainly depends on C, α, and the scale ratio. It does not say the background is physically derived from the forcing chain; it is a definitional choice, a modeling decision that the baseline is 1. The theorem only certifies that this baseline does not shift when parameters change, a property the framework uses to build the mode partition, the sum of a background density and a perturbation, and to prove homogeneity: when the perturbation density δρ is zero, the partition returns exactly the background density ρ̄.

The practical consequence is that the framework can separate the constant part of the kernel from the scale-dependent part without fear of cross-contamination. Any change in the kernel as the universe expands comes entirely from the perturbation term, never from a drifting baseline. This makes the model's predictions about growth easier to interpret and test, since the background is a fixed reference point against which all fluctuations are measured.

/-- The background mode is independent of every kernel parameter: the
homogeneous density does not source any ILG enhancement. This formalizes
the perturbation/background split that resolves Beltracchi's concern (2)
on the Lean side. -/
theorem kernel_background_independent_of_params (P : KernelParams) :
    kernel_background = 1 := rfl

@[simp] theorem kernel_background_eq_one : kernel_background = 1 := rfl

/-- The ILG kernel function:
  w(k, a) = 1 + C · (a / (k τ₀))^α

We use max with a small ε to avoid division issues when k τ₀ = 0. -/
noncomputable def kernel (P : KernelParams) (k a : ℝ) : ℝ :=
  1 + P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha

/-- The ILG background kernel: identically `1`.

The homogeneous Friedmann–Robertson–Walker background sits at the J-cost
minimum `J(1) = 0` with zero ledger gradient flow. The recognition operator
is at equilibrium on a homogeneous state, so there is no lag and no
enhancement. The background Poisson equation is unmodified standard GR. -/
@[simp] noncomputable def kernel_background : ℝ := 1

What this page does not claim

The kernel background being 1 is not a derived physical law; it is a definitional choice. The full kernel w(k, a) is not constant; it depends on the scale factor and wave number through the perturbation term. This theorem does not establish that the ILG kernel itself is correct or physically realized.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/ILG/Kernel.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: