powerKernel_rung_condition_iff
plain-language theorem explainer
Within the scale-free family K_s(z)=(1+z)^{-s}, the φ-rung balance holds if and only if the exponent is exactly s=1. Cosmologists citing the forced BIT redshift kernel use this to kill volume (s=3) and spacetime (s=4) dilution ansätze. The proof is a short log-cancellation: evaluate at 1+z=φ and cancel log φ>0.
Claim. For every real exponent $s$, the power-law kernel $K_s(z)=(1+z)^{-s}$ satisfies the $\varphi$-rung condition $K_s(\varphi-1)=\varphi^{-1}$ if and only if $s=1$.
background
This module forces the shape of the BIT dark-energy kernel $K(z)$ appearing in $w(z)=-1+\delta w_0\cdot K(z)$, companion to "The Forced Redshift Kernel". Two premises drive the derivation: 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}$).
The scale-free family is $K_s(z)=(1+z)^{-s}$. The rung condition asks that one rung back, at $1+z=\varphi$, the kernel equal the forced attenuation $\varphi^{-1}$. The golden ratio satisfies $1<\varphi$ (so $\log\varphi>0$), which is the only positivity fact needed for the cancellation below. Upstream, the forced single-rung occupancy is already $\mathrm{occ},n=\varphi^{-n}$ on the lattice $1+z=\varphi^n$.
proof idea
Unfold both sides: the rung condition becomes $(1+(\varphi-1))^{-s}=\varphi^{-1}$. The ring identity $1+(\varphi-1)=\varphi$ rewrites the left side as $\varphi^{-s}$.
Forward direction: assume $\varphi^{-s}=1/\varphi$. Take real logarithms, using $\log(\varphi^{-s})=-s\log\varphi$ and $\log(1/\varphi)=-\log\varphi$, with $\log\varphi>0$ from $1<\varphi$. Cancel the nonzero factor $\log\varphi$ by right-multiplication cancellation to obtain $s=1$.
Reverse direction: substitute $s=1$ and reduce $\varphi^{-1}=1/\varphi$ by the standard power and reciprocal identities.
why it matters
This is the exponent-pinning step that excludes classical geometric dilutions inside the multiplicative Cauchy class. The module doc lists it among the zero-sorry consequences: volume dilution ($s=3$) and spacetime dilution ($s=4$) fail the rung condition, leaving only $s=1$, i.e. $K(z)=1/(1+z)$.
Downstream, bit_kernel_shape_one_statement packages the claim as the second conjunct of the one-statement summary: the BIT kernel is forced to $1/(1+z)$ by $\varphi$-rung dilution, yielding the CPL thawing segment $w_a=-(1+w_0)$ with $w_0\in(-1,-0.88)$ and no phantom crossing. That summary is what DESI Y3+/Roman/Euclid are meant to adjudicate.
Framework-wise the pin rests on $\varphi$ as the self-similar fixed point (T6) and on cost-additive composition casting a multiplicative shadow across rungs. Open items remain the BIT aging mechanism itself, the single-channel selection behind the rung condition, and the today-amplitude band $\delta w_0\in(0,J(\varphi)]$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.