Pith. sign in
theorem

canonicalKernel_today

proved
show as:
module
IndisputableMonolith.Cosmology.BITKernelShapeForcing
domain
Cosmology
line
126 · github
papers citing
none yet

plain-language theorem explainer

The canonical redshift kernel equals one at the present epoch. Anyone normalizing the forced BIT dark-energy kernel, or checking the rung-scaling law, cites this as the z=0 anchor. Proof is a one-line unfolding of K(z)=1/(1+z).

Claim. The canonical kernel $K(z)=1/(1+z)$ satisfies $K(0)=1$.

background

This module forces the shape of the dark-energy deviation kernel $w(z)=-1+\delta w_0\cdot K(z)$ from two RS premises: rung factorization (attenuation multiplies across independent $\varphi$-rungs) and single-rung balance (one rung attenuates by the unique positive fixed point of $\rho=1/(1+\rho)$, namely $\varphi^{-1}$).

The canonical kernel is the physical-domain function $K(z)=1/(1+z)$. On the lattice $1+z=\varphi^n$ this is exactly the forced occupation law $\mathrm{occ},n=\varphi^{-n}$. Present-day redshift $z=0$ is the normalization point for any kernel that enters a rung-scaling law: the law asks that $K(0)=1$ and that each rung multiplies $K$ by $\varphi^{-1}$.

Upstream, the BIT kernel families already list $\mathrm{inv_one_plus_z}$ as one discrete choice; here that choice is singled out as canonical and then forced among scale-free competitors.

proof idea

One-line term proof: unfold the definition $K(z)=1/(1+z)$ and simplify at $z=0$, which yields $1/(1+0)=1$. Marked @[simp] so downstream tactics can discharge the normalization side condition automatically.

why it matters

Parent use is canonicalKernel_rungScaling: the rung-scaling law is a pair whose first component is exactly this today-normalization, after which the multiplicative step $K(\varphi(1+z)-1)=\varphi^{-1}K(z)$ is checked by algebra. That law, together with the forced occupation $\mathrm{occ},n=\varphi^{-n}$, pins the scale-free family $K_s(z)=(1+z)^{-s}$ at $s=1$, excluding volume ($s=3$) and spacetime ($s=4$) dilution.

In the paper chain this is the present-epoch anchor of the forced redshift kernel: CPL on the thawing line $w_a=-(1+w_0)$, sum rule $w_0+w_a=-1$, and the no-phantom bound $w(z)\ge-1$. It does not touch the still-open today-amplitude $\delta w_0\in(0,J(\varphi)]$, nor the hypothesis that the BIT aging channel itself is single-channel.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.