rungScaling_forces_lattice
plain-language theorem explainer
Any real kernel obeying the rung-scaling law is forced to equal φ^{-n} at every lattice point z = φ^n − 1. Cosmologists deriving the BIT redshift kernel cite this for lattice uniqueness of the attenuation. The proof is induction on the rung index, using normalization today and one-step attenuation by φ^{-1}.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ satisfy the rung-scaling law: $f(0)=1$ and $f(\varphi(1+z)-1)=f(z)/\varphi$ whenever $z\ge 0$. Then for every natural number $n$, $f(\varphi^n-1)=\varphi^{-n}$.
background
This module formalizes the forced shape of the dark-energy deviation kernel $K(z)$ 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 rung-scaling law packages those premises for a general kernel $f$: normalized today ($f(0)=1$), and advancing one $\varphi$-rung of scale ($1+z\mapsto\varphi(1+z)$) multiplies $f$ by exactly $\varphi^{-1}$. The golden ratio satisfies $1<\varphi$ (Constants.one_lt_phi), so the lattice points $z_n=\varphi^n-1$ are nonnegative and nested under the rung map.
On that lattice one has $1+z_n=\varphi^n$, hence the target value $\varphi^{-n}$ is exactly $1/(1+z_n)$. Sibling results force the occupation law $\mathrm{occ},n=\varphi^{-n}$ and pin power-law kernels to exponent $s=1$.
proof idea
Fix $f$ with the rung-scaling law and induct on $n$.
Base $n=0$: the goal is $f(\varphi^0-1)=\varphi^{0}$, i.e. $f(0)=1$, which is the first conjunct of the law.
Successor: assume $f(\varphi^k-1)=\varphi^{-k}$. Nonnegativity $\varphi^k-1\ge 0$ follows from $1\le\varphi^k$ via one_le_pow₀ and $1<\varphi$. Rewrite the next lattice point as $\varphi^{k+1}-1=\varphi(1+(\varphi^k-1))-1$, apply the second conjunct of the law, substitute the inductive hypothesis, and finish by field simplification and ring algebra to obtain $\varphi^{-(k+1)}$.
why it matters
Lattice uniqueness is one of the module's headline consequences: any kernel obeying rung scaling agrees with $\varphi^{-n}$ on the whole rung lattice, and the canonical kernel obeys the law. That pins the discrete skeleton of $K(z)$ before continuous interpolation.
Downstream in the same development, the forced kernel becomes exactly CPL on the thawing line $w_a=-(1+w_0)$ with sum rule $w_0+w_a=-1$ and $w_0\in(-1,-0.88)$, plus the sign bound $w(z)\ge -1$ (no phantom). The result sits under the Recognition landmarks $\varphi$ as self-similar fixed point (T6) and cost-additivity shadowing into multiplicative rung factorization; it does not itself invoke the eight-tick octave or $D=3$.
No external used_by edges are recorded yet. Open items remain the BIT aging mechanism hypothesis, single-channel ($d=1$) selection, 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.