Encyclopedia Ilg Ilg Kernel Kernel Perturbation Bounded Above

ARTICLE 3 claims 3 theorems

Ilg Kernel Kernel Perturbation Bounded Above

A formal proof places a hard upper limit on a cosmological correction term, guaranteeing it cannot grow without bound.

Verify this page

A ceiling on the perturbation

In the Recognition Science framework, a ledger of recognition events, the Infra-Luminous Gravity (ILG) kernel describes how a background density is perturbed by a mode of wave number k. The perturbation term, written kernel_perturbation, equals 1 + C · (a / (max k_min k · τ₀))^α, where a is the scale factor, τ₀ a reference time, α the ILG exponent (1 - 1/φ)/2, and C an amplitude constant. The theorem kernel_perturbation_bounded_above proves that for any positive k_min and a, this term is always at most 1 + C · (max 0.01 (a / (k_min · τ₀)))^α. In plain words: the perturbation cannot exceed the value it takes when the wave number is floored at k_min.

The bound matters because it is uniform in k. As k grows, the denominator (max k_min k · τ₀) grows, so the ratio a / (max k_min k · τ₀) shrinks, and the perturbation stays below its value at the infrared floor k_min. The proof is a direct consequence of the definition: replacing k by the larger of k_min and k can only decrease the ratio inside the power, and the exponent α is nonnegative. The theorem kernel_perturbation_eq_kernel_of_ge shows that when k ≥ k_min, the perturbation equals the plain kernel, and kernel_perturbation_at_IR_floor gives the matching equality at the floor itself. Together these pin the perturbation to the kernel's behavior at the infrared cutoff.

This bound is one of several facts assembled into the causality certificate, a packaged collection of kernel properties used to guarantee that the ILG model respects physical limits. The certificate also records that the perturbation is positive, at least 1, and that the background kernel is exactly 1. The bounded-above theorem supplies the missing upper side: without it, the certificate could assert positivity but not a ceiling. With it, the model has a two-sided control on the perturbation for all wave numbers.

What the theorem does not claim is equally precise. It does not say the perturbation is bounded by a constant independent of a; the upper bound still grows with the scale factor, so the theorem allows the perturbation to increase as the universe expands. It does not assert that the bound is tight, only that the perturbation never exceeds it. And it does not identify C or α with any measured cosmological quantity; those values come from separate definitions, such as rsKernelParams setting C = φ^(-3/2) or eightTickKernelParams setting C = 49/162. The theorem is a structural inequality about the kernel's form, not a numerical prediction.

THEOREM kernel_perturbation_bounded_above · IndisputableMonolith/ILG/Kernel.lean
kernel_perturbation_bounded_above · IndisputableMonolith/ILG/Kernel.lean:305 
/-- **The IR boundedness theorem.** For any positive IR cutoff `k_min > 0`,
positive scale factor `a > 0`, and any wavenumber `k`, the perturbation
kernel is bounded above by its IR-saturated value:
\[ w_{\rm pert}(k_{\min}, k, a) \le 1 + C \left(\frac{a}{k_{\min}\,\tau_0}\right)^\alpha. \]

This resolves Beltracchi's concern (2): the kernel does not run away as
`k → 0`. The homogeneous mode is bounded by a finite ceiling fixed by
the recognition horizon. -/
theorem kernel_perturbation_bounded_above
    (P : KernelParams) {k_min : ℝ} (hkmin : 0 < k_min) {a : ℝ} (ha : 0 < a)
    (k : ℝ) :
    kernel_perturbation P k_min k a
      ≤ 1 + P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
  unfold kernel_perturbation
  -- max k_min k ≥ k_min, so 1/(max k_min k) ≤ 1/k_min, so
  -- a/(max k_min k * tau0) ≤ a/(k_min * tau0).
  have h_max_ge : k_min ≤ max k_min k := le_max_left _ _
  have h_max_pos : 0 < max k_min k := lt_of_lt_of_le hkmin h_max_ge
  have h_kmin_tau_pos : 0 < k_min * P.tau0 := mul_pos hkmin P.tau0_pos
  have h_max_tau_pos : 0 < max k_min k * P.tau0 := mul_pos h_max_pos P.tau0_pos
  have h_arg_le : a / (max k_min k * P.tau0) ≤ a / (k_min * P.tau0) := by
    apply div_le_div_of_nonneg_left (le_of_lt ha) h_kmin_tau_pos
    exact mul_le_mul_of_nonneg_right h_max_ge P.tau0_pos.le
  -- Now max 0.01 is monotone, and rpow is monotone for positive base + nonneg exponent.
  have h_max_le : max 0.01 (a / (max k_min k * P.tau0))
        ≤ max 0.01 (a / (k_min * P.tau0)) := by
    exact max_le_max (le_refl _) h_arg_le
  have h_lhs_pos : 0 < max 0.01 (a / (max k_min k * P.tau0)) := by
    apply lt_max_of_lt_left; norm_num
  have h_rpow_le : (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha
        ≤ (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
    apply Real.rpow_le_rpow (le_of_lt h_lhs_pos) h_max_le P.alpha_nonneg
  have h_mul_le : P.C * (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha
        ≤ P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
    exact mul_le_mul_of_nonneg_left h_rpow_le P.C_nonneg
  linarith
THEOREM kernel_perturbation_eq_kernel_of_ge · IndisputableMonolith/ILG/Kernel.lean
kernel_perturbation_eq_kernel_of_ge · IndisputableMonolith/ILG/Kernel.lean:263 
/-- 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]
THEOREM kernel_perturbation_bounded_above · IndisputableMonolith/ILG/Kernel.lean
kernel_perturbation_bounded_above · IndisputableMonolith/ILG/Kernel.lean:305 
/-- **The IR boundedness theorem.** For any positive IR cutoff `k_min > 0`,
positive scale factor `a > 0`, and any wavenumber `k`, the perturbation
kernel is bounded above by its IR-saturated value:
\[ w_{\rm pert}(k_{\min}, k, a) \le 1 + C \left(\frac{a}{k_{\min}\,\tau_0}\right)^\alpha. \]

This resolves Beltracchi's concern (2): the kernel does not run away as
`k → 0`. The homogeneous mode is bounded by a finite ceiling fixed by
the recognition horizon. -/
theorem kernel_perturbation_bounded_above
    (P : KernelParams) {k_min : ℝ} (hkmin : 0 < k_min) {a : ℝ} (ha : 0 < a)
    (k : ℝ) :
    kernel_perturbation P k_min k a
      ≤ 1 + P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
  unfold kernel_perturbation
  -- max k_min k ≥ k_min, so 1/(max k_min k) ≤ 1/k_min, so
  -- a/(max k_min k * tau0) ≤ a/(k_min * tau0).
  have h_max_ge : k_min ≤ max k_min k := le_max_left _ _
  have h_max_pos : 0 < max k_min k := lt_of_lt_of_le hkmin h_max_ge
  have h_kmin_tau_pos : 0 < k_min * P.tau0 := mul_pos hkmin P.tau0_pos
  have h_max_tau_pos : 0 < max k_min k * P.tau0 := mul_pos h_max_pos P.tau0_pos
  have h_arg_le : a / (max k_min k * P.tau0) ≤ a / (k_min * P.tau0) := by
    apply div_le_div_of_nonneg_left (le_of_lt ha) h_kmin_tau_pos
    exact mul_le_mul_of_nonneg_right h_max_ge P.tau0_pos.le
  -- Now max 0.01 is monotone, and rpow is monotone for positive base + nonneg exponent.
  have h_max_le : max 0.01 (a / (max k_min k * P.tau0))
        ≤ max 0.01 (a / (k_min * P.tau0)) := by
    exact max_le_max (le_refl _) h_arg_le
  have h_lhs_pos : 0 < max 0.01 (a / (max k_min k * P.tau0)) := by
    apply lt_max_of_lt_left; norm_num
  have h_rpow_le : (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha
        ≤ (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
    apply Real.rpow_le_rpow (le_of_lt h_lhs_pos) h_max_le P.alpha_nonneg
  have h_mul_le : P.C * (max 0.01 (a / (max k_min k * P.tau0))) ^ P.alpha
        ≤ P.C * (max 0.01 (a / (k_min * P.tau0))) ^ P.alpha := by
    exact mul_le_mul_of_nonneg_left h_rpow_le P.C_nonneg
  linarith

What this page does not claim

The theorem does not claim a bound independent of the scale factor a. It does not assert that the upper bound is attained or tight. It does not identify the kernel parameters with measured cosmological values.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND