bit_kernel_shape_one_statement
plain-language theorem explainer
Five forced consequences of BIT rung dilution are packaged as one conjunction: aging-charge attenuation is φ^{-n}, the scale-free kernel class is pinned to s=1 (hence K(z)=1/(1+z)), RS dark energy sits on the CPL thawing line w_a=-(1+w_0), and w(z) never crosses below -1. Cosmologists comparing DESI/Roman/Euclid to the RS prediction cite this summary. The proof is a five-component term that reuses the already-proved component lemmas.
Claim. The following hold simultaneously: (i) every rung-dilution law satisfies $\mathrm{occ}(n)=\varphi^{-n}$; (ii) a power kernel $K_s(z)=(1+z)^{-s}$ meets the $\varphi$-rung condition iff $s=1$; (iii) for $z\ge 0$, $K_1(z)=1/(1+z)$; (iv) for every amplitude $\delta w_0$, the pair $(w_0,w_a)=(-1+\delta w_0,-\delta w_0)$ lies on the thawing line $w_a=-(1+w_0)$; (v) if $\delta w_0\ge 0$ and $z>-1$, then $w_{\mathrm{RS}}(\delta w_0,z)\ge -1$.
background
The module formalizes the paper "The Forced Redshift Kernel" (2026-06-09). Dark-energy deviation is written $w(z)=-1+\delta w_0\cdot K(z)$; historically $K$ was a modeling choice. Two premises fix its shape: rung factorization (attenuation across $m+n$ $\varphi$-rungs multiplies) and single-rung balance $\rho=1/(1+\rho)$, whose unique positive fixed point is $\varphi^{-1}$.
A RungDilution packages a positive map $\mathrm{occ}:\mathbb{N}\to\mathbb{R}$ with those two axioms. The forced solution is $\mathrm{occ}(n)=\varphi^{-n}$, which on the lattice $1+z=\varphi^n$ is $1/(1+z)$. The scale-free family is $K_s(z)=(1+z)^{-s}$; the rung condition $K(\varphi-1)=\varphi^{-1}$ pins $s=1$, excluding volume ($s=3$) and spacetime ($s=4$) dilution. The canonical kernel is $K(z)=1/(1+z)$.
In the CPL plane the RS thawing line is $w_a=-(1+w_0)$. The RS equation of state $w_{\mathrm{RS}}$ is the forced-kernel realization; non-negative amplitude keeps $w\ge -1$ at every physical redshift (sign falsifier).
proof idea
Term-mode five-tuple, no new reasoning. First component: for each dilution law $L$, apply $L.\mathrm{occ_forced}$ (induction from composition and the one-rung fixed point). Second: powerKernel_rung_condition_iff, which pins the exponent by evaluating $K_s$ at $z=\varphi-1$. Third: powerKernel_one_eq_canonical, rewriting $(1+z)^{-1}=1/(1+z)$ on $z\ge 0$. Fourth: rs_on_thawing_line, the algebraic identity $w_a=-\delta w_0=-(1+w_0)$ when $w_0=-1+\delta w_0$. Fifth: no_phantom, unfolding $w_{\mathrm{RS}}$ and using non-negativity of $\delta w_0/(1+z)$ for $z>-1$.
why it matters
This is the dated one-statement summary of the BIT kernel-shape forcing chain: $\varphi$-rung dilution forces $K(z)=1/(1+z)$, and the RS dark-energy prediction is the CPL segment on $w_a=-(1+w_0)$ with $w_0\in(-1,-0.88)$ and no phantom crossing, to be tested by DESI Y3+/Roman/Euclid.
It sits at the end of the module's proved consequences (occ forced, exponent pin, canonical identification, thawing line, no phantom). Downstream use count is presently zero; the declaration is the citation handle for the paper claim rather than an intermediate lemma.
Framework context: single-rung balance uses the unique positive fixed point of reciprocal balance, consistent with $\varphi$ as the self-similar generator (forcing-chain T6). Open items remain outside this package: the BIT aging mechanism and single-channel selection are hypotheses; the today-amplitude $\delta w_0\in(0,J(\varphi)]$ is open. The related $\Omega_\Lambda$-gap explanation is already retired elsewhere in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.