occ_eq_inv_one_plus_z
plain-language theorem explainer
At φ-rung n of cosmic scale, aging-charge attenuation equals 1/(1+z) once redshift is fixed by 1+z=φ^n. Cosmologists equating the forced BIT lattice law to the continuum kernel K(z)=1/(1+z) cite this identity. The proof rewrites the already-forced occ n=φ^{-n} by a short ring cancellation and power identities.
Claim. Let $L$ be a rung-dilution law. For every natural number $n$, the attenuation satisfies $L.\mathrm{occ}(n)=1/(1+(\varphi^n-1))$. Equivalently, on the lattice $1+z=\varphi^n$, one has $L.\mathrm{occ}(n)=1/(1+z)$.
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)$. Two premises drive the argument: rung factorization (attenuation across $m+n$ φ-rungs multiplies) and single-rung balance (one rung attenuates by the unique positive fixed point of $\rho=1/(1+\rho)$, namely $\varphi^{-1}$).
A RungDilution packages the attenuation map $\mathrm{occ}:\mathbb{N}\to\mathbb{R}$ with positivity, multiplicative composition, and the single-rung value. The upstream theorem occ_forced already concludes $\mathrm{occ}(n)=\varphi^{-n}$ for every $n$. Cosmic scale is tied to redshift on the discrete lattice by the identification $1+z=\varphi^n$, so the same law should read $1/(1+z)$.
The present result is exactly that translation: it rewrites the forced power of $\varphi$ into the redshift form used by the continuum families (in particular the inv_one_plus_z kernel).
proof idea
Rewrite the goal by the forced rung law occ_forced, which supplies $\mathrm{occ}(n)=(1/\varphi)^n$. A one-line ring identity cancels $1+(\varphi^n-1)$ down to $\varphi^n$. Then div_pow and one_pow turn $(1/\varphi)^n$ into $1/\varphi^n$, matching the simplified right-hand side. No induction or new structural hypotheses are needed; the work is pure algebra on top of occ_forced.
why it matters
The module's headline is that the continuum kernel is forced to $K(z)=1/(1+z)$, not volume dilution $(1+z)^{-3}$ or spacetime dilution $(1+z)^{-4}$. This lemma is the discrete-to-redshift bridge: once $\mathrm{occ}(n)=\varphi^{-n}$ is forced, the lattice points $1+z=\varphi^n$ carry exactly the canonical kernel value.
Downstream the same shape pins the scale-free exponent $s=1$, yields the CPL thawing line $w_a=-(1+w_0)$ with sum rule $w_0+w_a=-1$, and supports the no-phantom bound $w(z)\ge -1$. In the Recognition chain this sits after T6 (φ as self-similar fixed point) and uses the φ-ladder as the cosmic scale coordinate. The open item left by the module is the today-amplitude $\delta w_0\in(0,J(\varphi)]$, not the kernel shape itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.