RungScalingLaw
plain-language theorem explainer
The rung-scaling law is the predicate on a real kernel f requiring normalization today (f(0)=1) and one-rung attenuation: advancing cosmic scale by one φ-step multiplies the kernel by φ⁻¹. Cosmologists forcing the BIT redshift kernel cite it as the functional equation that pins values on the φ-rung lattice. It is a pure Prop definition (normalization conjoined with a recurrence), not a proved claim.
Claim. A function $f:\mathbb{R}\to\mathbb{R}$ obeys the rung-scaling law when $f(0)=1$ and, for every redshift $z\ge 0$, $f(\varphi(1+z)-1)=f(z)/\varphi$, where $\varphi$ is the golden-ratio fixed point.
background
This module formalizes the paper "The Forced Redshift Kernel": the dark-energy deviation $w(z)=-1+\delta w_0\cdot K(z)$ once treated $K$ as a modeling choice. Two premises force the shape. Rung factorization says aging-charge attenuation across $m+n$ $\varphi$-rungs of cosmic scale factors as a product (multiplicative shadow of cost additivity). Single-rung balance says one rung attenuates by the unique positive fixed point of $\rho=1/(1+\rho)$, which is $\varphi^{-1}$.
The rung lattice is $1+z=\varphi^n$, so $z=\varphi^n-1$. On that lattice the forced occupation is $\mathrm{occ},n=\varphi^{-n}$, equivalently $1/(1+z)$. The present definition packages the continuous functional form of that one-rung step: normalize at $z=0$, and under the scale map $1+z\mapsto\varphi(1+z)$ divide the kernel by $\varphi$. Sibling objects include the canonical kernel, power-law kernels $K_s(z)=(1+z)^{-s}$, and the scale-free class used to exclude volume ($s=3$) and spacetime ($s=4$) dilution.
proof idea
Definitional, not a proof. The body is the conjunction of two clauses: the normalization $f,0=1$, and the universal recurrence that for every $z\ge 0$ the value at the image point $\varphi(1+z)-1$ equals $f,z$ divided by $\varphi$. No lemmas are applied; downstream theorems discharge or exploit this Prop.
why it matters
Parent uses are immediate. canonicalKernel_rungScaling shows the module's canonical kernel satisfies the law. rungScaling_forces_lattice then gives lattice uniqueness: any $f$ obeying the law equals $\varphi^{-n}=1/(1+z)$ at every rung $z=\varphi^n-1$. That uniqueness, with the scale-free Cauchy class, pins the power $s=1$ and excludes volume and spacetime dilution. Downstream the forced kernel is 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 falsifier $w(z)\ge -1$. Framework landmarks: $\varphi$ as the T6 self-similar fixed point, and the $\varphi$-ladder mass/scale structure. Open remain the BIT aging mechanism itself, the single-channel ($d=1$) selection, and the today-amplitude $\delta w_0\in(0,J(\varphi)]$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.