canonicalKernel_rungScaling
plain-language theorem explainer
The canonical redshift kernel K(z)=1/(1+z) obeys the rung-scaling law: normalized at z=0, and attenuated by exactly φ^{-1} when scale advances one φ-rung. Cosmologists forcing the BIT dark-energy kernel cite this to lock lattice values to φ^{-n}. The proof is a short algebraic check: unfold, rewrite the shifted denominator, and field-simplify.
Claim. The function $K(z)=1/(1+z)$ satisfies $K(0)=1$ and, for every redshift $z\ge 0$, $K(\varphi(1+z)-1)=K(z)/\varphi$, where $\varphi$ is the golden ratio (positive self-similar fixed point).
background
In the BIT kernel shape-forcing module (companion to "The Forced Redshift Kernel"), the dark-energy deviation is written $w(z)=-1+\delta w_0\cdot K(z)$. The kernel shape is forced from two premises: rung factorization (attenuation across $m+n$ $\varphi$-rungs multiplies) and single-rung balance (one step equals the unique positive fixed point of $\rho=1/(1+\rho)$, namely $\varphi^{-1}$).
The canonical kernel is the explicit map $K(z)=1/(1+z)$ on the physical domain. The rung-scaling law packages normalization today together with the one-rung step $1+z\mapsto\varphi(1+z)$ attenuating $K$ by exactly $\varphi^{-1}$. The constant $\varphi$ is the Recognition self-similar fixed point (T6).
Upstream, $K(0)=1$ is already recorded as a simp lemma; the family of BIT kernels also includes the same $1/(1+z)$ member among constant, inverse-linear, and exponential options.
proof idea
Build the conjunction that defines the rung-scaling law. The first conjunct is the existing one-line fact $K(0)=1$. For the second, fix $z\ge 0$, record $1+z>0$ and $\varphi>0$, unfold $K$, rewrite the algebraic identity $1+(\varphi(1+z)-1)=\varphi(1+z)$ by ring, then finish with field simplification to obtain $1/(\varphi(1+z))=(1/(1+z))/\varphi$.
why it matters
Places the canonical kernel inside the rung-scaling class, which is the hypothesis of lattice uniqueness: any such kernel equals $\varphi^{-n}=1/(1+z)$ at every rung $z=\varphi^n-1$. Combined with the forced occupancy $\mathrm{occ},n=\varphi^{-n}$ from rung dilution, this identifies the BIT kernel on the $\varphi$-lattice and feeds the scale-free analysis that pins the power $s=1$, excluding volume ($s=3$) and spacetime ($s=4$) dilution.
Module consequences include the CPL thawing-line form, the sum rule $w_0+w_a=-1$, the $w_0$ band in $(-1,-0.88)$, and the no-phantom bound $w(z)\ge -1$. No external consumers are recorded yet; the lemma is internal to the forced-kernel uniqueness chain. Open items remain the BIT aging mechanism itself and the today-amplitude interval for $\delta w_0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.