canonicalKernel
plain-language theorem explainer
Defines the canonical redshift kernel K(z) = 1/(1+z) on the physical domain. Cosmologists working the BIT dark-energy deviation w(z) = −1 + δw₀·K(z) cite it as the forced shape. It is a one-line definition; uniqueness and rung-scaling are proved elsewhere against this reference object.
Claim. The canonical kernel is the real function $K(z) = 1/(1+z)$ for redshift $z$.
background
The module formalizes "The Forced Redshift Kernel": the dark-energy deviation $w(z) = -1 + \delta w_0 \cdot K(z)$ once treated $K$ as a free modeling choice. Two premises pin the shape. Rung factorization says aging-charge attenuation across $m+n$ $\varphi$-rungs multiplies (the multiplicative shadow of cost additivity). Single-rung balance forces one rung to attenuate by the unique positive fixed point of $\rho = 1/(1+\rho)$, namely $\varphi^{-1}$.
On the lattice $1+z = \varphi^n$ this yields occupation $\mathrm{occ}, n = \varphi^{-n}$, i.e. $1/(1+z)$. The scale-free family $K_s(z) = (1+z)^{-s}$ is then pinned at $s=1$, excluding volume ($s=3$) and spacetime ($s=4$) dilution. The present definition is the continuum reference object that matches that lattice law.
proof idea
Pure definition: the body is the closed form $1/(1+z)$. No tactics, lemmas, or axioms. Downstream theorems unfold this abbreviation and compare it to power kernels and rung-scaling predicates.
why it matters
This is the forced BIT kernel shape that the module's one-statement summary packages: $K(z)=1/(1+z)$ by $\varphi$-rung dilution, giving the CPL thawing segment $w_a=-(1+w_0)$ with $w_0\in(-1,-0.88)$ and no phantom crossing. Downstream, canonicalKernel_today records $K(0)=1$; powerKernel_one_eq_canonical identifies the $s=1$ power kernel with this $K$ on $z\ge 0$; canonicalKernel_rungScaling shows it obeys the rung-scaling law used for lattice uniqueness. The open piece remains the today-amplitude $\delta w_0\in(0,J(\varphi)]$; the shape itself is closed under the two stated premises.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.