powerKernel_one_eq_canonical
plain-language theorem explainer
On physical redshifts z ≥ 0, the scale-free power kernel at exponent one equals the canonical kernel K(z) = 1/(1+z). Anyone citing the forced BIT redshift kernel uses this to identify the rung-pinned member of the multiplicative Cauchy family with the explicit inverse-scale form. The proof is a short unfold-and-rewrite via the real-power identity x^{-1} = 1/x.
Claim. For every real redshift $z \ge 0$, the scale-free kernel at exponent one equals the canonical kernel: $(1+z)^{-1} = 1/(1+z)$.
background
This module formalizes the paper "The Forced Redshift Kernel": the dark-energy deviation $w(z) = -1 + \delta w_0 \cdot K(z)$ no longer treats $K$ as a free modeling choice. Two premises force the shape: rung factorization (attenuation across $m+n$ $\varphi$-rungs multiplies) and single-rung balance (one rung attenuates by the unique positive fixed point of $\rho = 1/(1+\rho)$, namely $\varphi^{-1}$).
Two kernel objects appear here. The canonical kernel is $K(z) = 1/(1+z)$ on the physical domain. The scale-free (power) family is $K_s(z) = (1+z)^{-s}$, the continuous multiplicative-Cauchy class that converts products of scale factors into products of attenuations. The physical domain is $z \ge 0$ (nonnegative redshift).
Upstream, the rung lattice uses cosmic scale $\varphi^k$; the BIT kernel families already list $\mathrm{inv_one_plus_z}$ as one discrete option. This lemma is the elementary identification that the $s=1$ power member is exactly that canonical form.
proof idea
Term-style tactic proof with no external lemmas beyond Mathlib real-power facts. Unfold both definitions so the goal is $(1+z)^{-1} = 1/(1+z)$. Rewrite with Real.rpow_neg_one (which turns $x^{-1}$ into $x^{-1}$ in reciprocal form) and one_div to match $1/(1+z)$. The hypothesis $z \ge 0$ is carried for domain hygiene and is unused in the algebra.
why it matters
Closes the bridge from the rung-condition pin $s=1$ inside the scale-free class to the explicit canonical kernel used everywhere downstream. The parent one-statement summary bit_kernel_shape_one_statement packages five conjuncts; the third is exactly $\forall z \ge 0,, K_1(z) = 1/(1+z)$, and this theorem discharges it.
In the paper chain, once rung dilution forces $\mathrm{occ}, n = \varphi^{-n}$ (i.e. $1/(1+z)$ on the lattice $1+z=\varphi^n$) and the scale-free rung condition forces $s=1$, this identity names that unique power kernel as the canonical $K(z)=1/(1+z)$. That shape then yields CPL on the thawing line $w_a=-(1+w_0)$, the sum rule $w_0+w_a=-1$, the band $w_0 \in (-1,-0.88)$, and the no-phantom bound $w(z)\ge -1$. Framework landmarks in play are the $\varphi$-ladder and single-rung balance $\varphi^{-1}$; the today-amplitude $\delta w_0 \in (0,J(\varphi)]$ remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.