occ_forced
plain-language theorem explainer
On any rung-dilution structure the occupancy after n φ-rungs is forced to φ^{-n}. Cosmologists deriving the BIT redshift kernel, and anyone proving the lattice measure is unique, cite this as the discrete dilution law. The proof is induction: unit at zero rungs, single-rung value φ^{-1}, and multiplicative composition across rungs.
Claim. For every natural number $n$, the aging-charge attenuation across $n$ $\varphi$-rungs equals $\varphi^{-n}$: $\mathrm{occ}(n)=\varphi^{-n}$.
background
This module forces the shape of the BIT dark-energy kernel $K(z)$ from two premises only: rung factorization (attenuation across $m+n$ rungs is the product of the sub-attenuations) and single-rung balance (one rung attenuates by the unique positive fixed point of $\rho=1/(1+\rho)$, which is $\varphi^{-1}$).
A RungDilution structure packages a positive occupancy map occ : ℕ → ℝ together with the composition identity occ(m+n)=occ(m)·occ(n) and the one-rung self-similarity hypothesis. Zero rungs carry full charge: occ 0 = 1. The single-rung theorem already pins occ 1 = 1/φ.
On the cosmic ladder one identifies $1+z=\varphi^n$, so the discrete law occ n = φ^{-n} is exactly the redshift form $1/(1+z)$ at lattice points. That identification is the bridge from abstract dilution to the continuous kernel class used later in the module.
proof idea
Term-mode induction on $n$.
Base case $n=0$: rewrite with the zero-rung theorem (occ 0 = 1), which matches $(1/\varphi)^0$.
Successor: apply the composition law at $(k,1)$ to get occ(k+1)=occ(k)·occ(1). Substitute the inductive hypothesis and the forced single-rung value occ 1 = 1/φ, then finish by ring arithmetic to obtain $(1/\varphi)^{k+1}$.
why it matters
This is the central discrete law of the Forced Redshift Kernel paper: once occupancy is $\varphi^{-n}$ on the rung lattice, the scale-free power kernels $K_s(z)=(1+z)^{-s}$ are pinned to $s=1$, excluding volume ($s=3$) and spacetime ($s=4$) dilution.
Downstream it is quoted verbatim in the one-statement summary of the BIT kernel shape, rewritten as the redshift identity occ n = 1/(1+z) on $1+z=\varphi^n$, and reused in Foundation.MeasureForcing as both kernel_dilution_is_measure and the lattice-layer theorem weight_forced (T9: the weight rule is forced to $\varphi^{-n}$).
Framework landmarks: φ is the self-similar fixed point (T6); the same geometric ratio that forces the eight-tick octave and $D=3$ here forces the cosmological measure. Open items left untouched: the BIT aging mechanism itself, single-channel 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.