Cosmology Bitkernel Families Bitkernel Families Cert

The certified kernel families

In cosmology, the dark energy equation of state is often written w(z) = -1 + δw(z), where δw(z) is a small correction that could vary with redshift z, the measure of cosmic distance and time. The Recognition Science framework's ledger (a discrete record of recognition events) suggests such a correction exists, but the exact form is not fixed by the framework alone. The declaration BITKernelFamiliesCert addresses this by certifying three specific kernel families, each a possible shape for δw(z): a constant K(z) = 1, the canonical arc-11 form K(z) = 1/(1+z), and an exponential K(z) = exp(-z/z0).

The certificate proves four properties that hold for all three families. First, every kernel equals 1 at z = 0, meaning the correction starts at its full strength today. Second, the maximum amplitude δw_0 is bounded between 0 and J(φ) = φ - 3/2 ≈ 0.118, where φ is the golden ratio. Third, this maximum is strictly less than 1, so the correction remains small. Fourth, at z = 0 the effective equation of state is exactly w_eff = -1 + δw_0 for any kernel. The certificate is not a physical prediction; it is a consistency check, a machine-checked guarantee that these three models are internally sound and share these baseline properties.

The framework's library of formal theorems (a machine-checked collection of proofs) contains the certificate as an inhabited structure, meaning it is not merely stated but actually constructed from the individual theorems. This construction is what makes the certificate trustworthy: each property is proven, not assumed. The certificate's role is to provide a solid foundation for forecasting scripts, such as the DESI Y3 analysis, by ensuring that whatever kernel shape is chosen, it respects the framework's bounds and normalizations.

What the certificate does not claim is equally important. It does not say which kernel family is correct; all three remain viable options. It does not predict the actual value of δw_0, only its allowed range. It does not establish that the BIT correction exists in nature, only that if it does, these are the permitted forms. The certificate is a toolbox, not a verdict.

/-- All three kernels equal 1 at `z = 0`. -/
theorem kernel_at_zero (k : KernelFamily) (z0 : ℝ) :
    kernel k 0 z0 = 1 := by
  cases k <;> simp [kernel]

theorem delta_w0_max_pos : 0 < delta_w0_max := by
  unfold delta_w0_max
  have := phi_gt_onePointFive
  linarith

theorem delta_w0_max_lt_one : delta_w0_max < 1 := by
  unfold delta_w0_max
  have := phi_lt_two
  linarith

/-- At `z = 0`, `w_eff = -1 + δw_0` for any kernel. -/
theorem w_eff_at_zero (k : KernelFamily) (delta_w0 z0 : ℝ) :
    w_eff k 0 delta_w0 z0 = -1 + delta_w0 := by
  unfold w_eff
  rw [kernel_at_zero]
  ring

/-- **BIT KERNEL FAMILIES MASTER CERTIFICATE.** -/
structure BITKernelFamiliesCert where
  kernel_at_zero_one :
    ∀ k : KernelFamily, ∀ z0 : ℝ, kernel k 0 z0 = 1
  delta_w0_max_pos :
    0 < delta_w0_max
  delta_w0_max_lt_one :
    delta_w0_max < 1
  w_eff_at_zero :
    ∀ k : KernelFamily, ∀ (delta_w0 z0 : ℝ),
      w_eff k 0 delta_w0 z0 = -1 + delta_w0

What this page does not claim

The certificate does not determine which kernel family is correct. The certificate does not predict the actual value of δw_0. The certificate does not prove that the BIT correction exists in nature.

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/BITKernelFamilies.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: