Ilg Kernel Kernel With Hubble Bounded Above

A bound on the Hubble kernel

In cosmology, the Hubble parameter H measures how fast the universe is expanding at a given moment. The Recognition Science framework uses a mathematical object called a kernel, a weighting function that describes how a perturbation, a small disturbance in density, is amplified at different scales. The declaration kernel_with_Hubble_bounded_above is a proved theorem in the framework's machine-checked library of formal theorems. It states that when the expansion rate H is positive, the kernel that includes Hubble's effect is always less than or equal to a specific upper bound. That bound is 1 plus a constant times a power of the ratio a / (a * H * tau0), where a is the scale factor, tau0 is a reference time scale, and the exponent alpha is derived from self-similarity.

To see what this means, consider the expression inside the bound. The term a / (a * H * tau0) simplifies to 1 / (H * tau0), so the bound depends on the expansion rate H and the reference time tau0. The theorem says that the kernel, which starts at 1 and grows with the perturbation, cannot exceed this value. It is a formal guarantee of stability: for any positive expansion rate and scale factor, the Hubble-modified kernel stays within a known envelope. The proof is a direct consequence of a more general bound on the perturbation kernel, which holds when the minimum wave number is positive. The theorem requires only that the scale factor a and the Hubble parameter H be positive; it holds for any wave number k.

The result is part of a larger formalized structure. The same library proves the kernel is always positive and at least 1, and it defines a certificate called CausalityBoundsCert that packages these bounds together. The certificate includes the Hubble bound as one of its fields, alongside bounds on the perturbation kernel and a statement that the background kernel is exactly 1. These facts support the framework's model of how density perturbations evolve, but the theorem itself does not claim that the bound is tight, that it matches any specific observation, or that the kernel describes actual cosmic expansion. It is a mathematical statement about a defined function, not a physical law.

In Recognition Science, this bound is one piece of a larger derivation. The exponent alpha is locked to a value derived from self-similarity, and the amplitude constant C is set to specific values in different parameter choices. The bound's role is to show that the framework's kernel, when modified by Hubble expansion, remains controlled. It does not, by itself, prove that the framework's model of gravity is correct or that its constants match measurements. Those are separate claims, and the theorem does not address them.

/-- **The Hubble ceiling theorem.** The Hubble-saturated kernel is bounded
above by the value attained at the Hubble wavenumber `k = a H`. This is
a specialization of `kernel_perturbation_bounded_above` to the canonical
RS choice `k_min = a H / c`. -/
theorem kernel_with_Hubble_bounded_above
    (P : KernelParams) {a H : ℝ} (ha : 0 < a) (hH : 0 < H) (k : ℝ) :
    kernel_with_Hubble P a H k
      ≤ 1 + P.C * (max 0.01 (a / (a * H * P.tau0))) ^ P.alpha := by
  unfold kernel_with_Hubble
  exact kernel_perturbation_bounded_above P (mul_pos ha hH) ha k

/-- **The Hubble ceiling theorem.** The Hubble-saturated kernel is bounded
above by the value attained at the Hubble wavenumber `k = a H`. This is
a specialization of `kernel_perturbation_bounded_above` to the canonical
RS choice `k_min = a H / c`. -/
theorem kernel_with_Hubble_bounded_above
    (P : KernelParams) {a H : ℝ} (ha : 0 < a) (hH : 0 < H) (k : ℝ) :
    kernel_with_Hubble P a H k
      ≤ 1 + P.C * (max 0.01 (a / (a * H * P.tau0))) ^ P.alpha := by
  unfold kernel_with_Hubble
  exact kernel_perturbation_bounded_above P (mul_pos ha hH) ha k

/-- **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 the bound is tight or that the kernel equals the bound at any point. The theorem does not claim the kernel represents actual cosmic expansion or matches any observational data. The theorem does not prove that the framework's model of gravity is physically correct.

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: