Ilg Kernel Kernel Perturbation Eq Kernel Of Ge

The perturbation kernel's agreement

The Infra-Luminous Gravity (ILG) framework works with a mathematical object called a kernel, a function that weights how much a disturbance at one scale contributes to an effect at another. The framework defines two versions of this kernel. The first, written kernel, takes a wave number k and a scale factor a and returns a positive number. The second, called the perturbation kernel, adds a lower bound k_min on the wave number, so that it only considers disturbances above a certain spatial frequency. The declaration kernel_perturbation_eq_kernel_of_ge proves that when the chosen wave number k is at least that lower bound k_min, the perturbation kernel and the base kernel give exactly the same value.

The proof is a direct algebraic simplification. Both kernels share the same defining expression, 1 + C · (a / (k · τ₀))^α, where C is an amplitude constant, τ₀ is a reference time scale, and α is the ILG exponent. The only difference is that the perturbation kernel replaces the wave number k with the maximum of k_min and k. When k_min ≤ k, that maximum is just k, so the two expressions become identical. The theorem states this equality for all real parameters, with no further conditions on the scale factor a or on the constants beyond the standard positivity assumptions built into the kernel parameters.

This equality is a consistency result. It shows that the perturbation kernel, which the framework uses to model density fluctuations, reduces to the base kernel in the regime where no infrared cutoff is active. In physical terms, it means that for modes with sufficiently high wave number, the perturbation formula and the base formula agree, so the framework treats the two descriptions as interchangeable in that range. The companion theorem kernel_perturbation_at_IR_floor covers the opposite case: when k falls below k_min, the perturbation kernel equals the base kernel evaluated at the floor k_min itself, so the floor acts as a hard cutoff on the wave number.

In Recognition Science, the framework's machine-checked library of formal theorems records this result as a proved statement. The theorem does not claim that the perturbation kernel is physically correct, that the ILG exponent α is the only possible choice, or that the kernel describes any actual gravitational system. It only establishes a formal identity between two definitions under a stated inequality. The framework's own documentation describes the kernel as well-defined and positive for physical parameter ranges, and separate theorems prove that the kernel is always at least 1 and that it grows monotonically with the scale factor, but those properties are not part of this particular declaration.

The practical consequence is that the framework can use the perturbation kernel in calculations without worrying about a discontinuity at the boundary k = k_min. The two formulas agree there, so a mode at exactly the cutoff wave number receives the same weight whether one uses the perturbed or the base expression. This smooth agreement is what makes the infrared floor a clean place to stop the mode sum, and it is the reason the framework can treat the perturbation kernel as a faithful extension of the base kernel above the floor.

/-- The perturbation kernel reduces to the original `kernel` when the
    wavenumber is at or above the IR cutoff. -/
theorem kernel_perturbation_eq_kernel_of_ge
    (P : KernelParams) {k_min k : ℝ} (a : ℝ) (h : k_min ≤ k) :
    kernel_perturbation P k_min k a = kernel P k a := by
  unfold kernel_perturbation kernel
  have hmax : max k_min k = k := max_eq_right h
  rw [hmax]

/-- The perturbation kernel collapses to the IR-saturated value when
    `k ≤ k_min`. -/
theorem kernel_perturbation_at_IR_floor
    (P : KernelParams) {k_min k : ℝ} (a : ℝ) (h : k ≤ k_min) :
    kernel_perturbation P k_min k a = kernel P k_min a := by
  unfold kernel_perturbation kernel
  have hmax : max k_min k = k_min := max_eq_left h
  rw [hmax]

/-- Kernel is at least 1. -/
theorem kernel_ge_one (P : KernelParams) (k a : ℝ) : 1 ≤ kernel P k a := by
  unfold kernel
  have hmax_pos : 0 < max 0.01 (a / (k * P.tau0)) := by
    apply lt_max_of_lt_left
    norm_num
  have hpow_nonneg : 0 ≤ (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
    mul_nonneg P.C_nonneg hpow_nonneg
  linarith

/-- Kernel is always positive for valid parameters. -/
theorem kernel_pos (P : KernelParams) (k a : ℝ) : 0 < kernel P k a := by
  unfold kernel
  have hmax_pos : 0 < max 0.01 (a / (k * P.tau0)) := by
    apply lt_max_of_lt_left
    norm_num
  have hpow_nonneg : 0 ≤ (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
    Real.rpow_nonneg (le_of_lt hmax_pos) P.alpha
  have hcorr_nonneg : 0 ≤ P.C * (max 0.01 (a / (k * P.tau0))) ^ P.alpha :=
    mul_nonneg P.C_nonneg hpow_nonneg
  linarith

What this page does not claim

The theorem does not claim that the perturbation kernel is physically correct or that it describes any actual gravitational system. The theorem does not claim that the ILG exponent α is the only possible choice for the kernel's power law. The theorem does not claim that the kernel is bounded above or that it has any particular behavior outside the stated inequality.

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: