Cosmology Bitkernel Families Exp Kernel Pos

The exponential kernel's positivity

In cosmology, a kernel is a mathematical shape that scales an effect across cosmic time. The Recognition Science framework's BIT kernel families define three such shapes for the amplitude δw(z), a small deviation in the dark-energy equation of state. The exponential kernel K3(z) = exp(-z/z₀) is one of them. The declaration exp_kernel_pos proves that this kernel is strictly positive for every real redshift z and every scale z₀. That is, 0 < exp(-z/z₀) holds as a formal theorem, established by the fact that the real exponential function never returns zero or a negative number.

This positivity is a sanity condition, not a physical prediction. It says the exponential shape never crosses zero, which matters because a kernel that went negative would flip the sign of the amplitude δw₀ and change the model's behavior in a way the framework does not intend. The proof is one line in the machine-checked library: it unfolds the definition of the kernel and applies the standard theorem that the exponential is always positive. The same library also proves the other two kernels are positive where they are defined: the constant kernel is always 1, and the 1/(1+z) kernel is positive for z > -1.

The declaration does not claim that the exponential kernel is the correct model of dark energy, nor that it fits any particular data. It does not say the amplitude δw₀ is positive; the amplitude is a separate parameter, bounded between 0 and φ - 3/2 ≈ 0.118 by a different theorem. The positivity result is a mathematical property of the kernel shape alone. It also does not assert anything about the exponential kernel at z = -z₀ or beyond, because the real exponential is positive everywhere; the condition is unconditional. What the theorem establishes is narrow and precise: the shape K3(z) = exp(-z/z₀) is always a positive number.

In practice, this means the exponential kernel is a well-behaved input to the framework's forecasts. When the DESI Y3 analysis script uses this kernel, the positivity theorem guarantees that the model's sign structure comes only from the amplitude δw₀, never from the kernel itself. That is the consequence a modeler can rely on, and it is the only consequence the declaration claims.

/-- The exponential kernel is positive everywhere. -/
theorem exp_kernel_pos (z z0 : ℝ) :
    0 < kernel KernelFamily.exponential z z0 := by
  unfold kernel
  exact Real.exp_pos _

What this page does not claim

The exponential kernel is the true model of dark energy. The amplitude δw₀ is positive or negative. The positivity theorem applies to the other two kernels at all redshifts.

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: