Cosmology Bitkernel Shape Forcing Power Kernel One Eq Canonical

The forced kernel shape

In the Recognition Science framework, the canonical function 1/(1+z), where z is redshift, describes how the density of matter dilutes as the universe expands. The declaration powerKernel_one_eq_canonical proves that when the power-law kernel (1+z)^(-s) is evaluated at s = 1, it equals this canonical function exactly, for all non-negative z.

The proof is short: the definition of the power-law kernel with s = 1 gives (1+z)^(-1), and the canonical function is defined as 1/(1+z) for non-negative z, so the two coincide by the algebraic identity (1+z)^(-1) = 1/(1+z). The theorem's role is to close a gap: earlier work had taken 1/(1+z) as a physical modeling choice, but now it is shown to be the unique single-channel scale-free dilution law, pinned by the same self-similarity condition that forces the golden ratio elsewhere in the framework.

In Recognition Science, this is part of a chain that derives the dark-energy equation of state. The framework models the aging of the universe as a discrete ledger of recognition events, and the kernel shape governs how the dark-energy density parameter w(z) evolves. The theorem establishes the mathematical identity, not the physical premise: it does not claim that the universe actually dilutes through exactly one channel, nor does it fix the today-amplitude of the deviation from w = -1.

The practical consequence is a testable prediction. With the kernel shape forced, the framework's dark-energy equation of state becomes w(z) = -1 + δw₀/(1+z), which is exactly the CPL parametrization with w₀ = -1 + δw₀ and wₐ = -δw₀. This predicts a line segment in the (w₀, wₐ) plane, with wₐ = -(1+w₀) and w₀ between -1 and -0.88. The DESI Y3+ survey, Roman, and Euclid can falsify this by measuring a posterior that excludes this line at high confidence.

The theorem itself is a formal statement in a machine-checked library of mathematical proofs. It is axiom-clean, meaning it relies only on the standard axioms of the ambient type theory. The physical interpretation, however, depends on hypotheses that are not proved: the single-channel selection and the BIT mechanism itself remain named premises with explicit falsifiers.

/-- The pinned kernel equals the canonical `DeltaWKernel` shape pointwise on
the physical redshift domain: `(1+z)^(−1) = f_canonical(z)` for `z ≥ 0`. -/
theorem powerKernel_one_eq_canonical (z : ℝ) (hz : 0 ≤ z) :
    powerKernel 1 z = f_canonical z := by
  unfold powerKernel f_canonical
  rw [if_neg (not_lt.mpr hz), Real.rpow_neg_one, one_div]

/-- The pinned kernel equals the canonical `DeltaWKernel` shape pointwise on
the physical redshift domain: `(1+z)^(−1) = f_canonical(z)` for `z ≥ 0`. -/
theorem powerKernel_one_eq_canonical (z : ℝ) (hz : 0 ≤ z) :
    powerKernel 1 z = f_canonical z := by
  unfold powerKernel f_canonical
  rw [if_neg (not_lt.mpr hz), Real.rpow_neg_one, one_div]

/-- **The forced kernel is exactly CPL** with `w₀ = −1 + δw₀`, `wₐ = −δw₀`. -/
theorem w_RS_is_CPL (dw0 z : ℝ) (hz : -1 < z) :
    w_RS dw0 z = w_CPL (-1 + dw0) (-dw0) z := by
  have h1z : (0 : ℝ) < 1 + z := by linarith
  unfold w_RS w_CPL
  field_simp
  ring

What this page does not claim

The theorem does not prove that the universe's dark energy dilutes through exactly one channel; that remains a named hypothesis with a falsifier. The theorem does not determine the today-amplitude δw₀, which remains an open parameter bounded by the framework's ceiling. The theorem does not claim the framework's dark-energy prediction matches any specific survey data; it only states the mathematical form of the prediction.

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/Cosmology/BITKernelShapeForcing.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: