RungDilution
plain-language theorem explainer
A rung dilution law packages attenuation of the cosmic aging charge after n φ-rungs of scale. It is fixed by two premises only: multiplicative composition across independent rungs, and single-rung reciprocal balance. Cosmology and measure-forcing results cite it as the kernel object whose unique solution is occ n = φ^{-n}. As a structure it is pure interface; uniqueness is proved downstream.
Claim. A rung dilution law is a map $\mathrm{occ}:\mathbb{N}\to\mathbb{R}$ such that (i) $\mathrm{occ}(n)>0$ for all $n$, (ii) $\mathrm{occ}(m+n)=\mathrm{occ}(m)\,\mathrm{occ}(n)$ for all $m,n$ (rung factorization), and (iii) $\mathrm{occ}(1)=1/(1+\mathrm{occ}(1))$ (single-rung self-similar balance).
background
The module forces the BIT dark-energy kernel shape from two premises rather than fitting $K(z)$. Cosmic scale is organized on the $\varphi$-ladder: after $n$ rungs one has $1+z=\varphi^n$ (with $\mathrm{scale},k=\varphi^k$). The aging charge is attenuated by a positive real $\mathrm{occ},n$ at rung $n$.
Rung factorization is the multiplicative shadow of cost additivity under independent composition: attenuation over $m+n$ rungs is the product of the sub-attenuations. This mirrors multiplicativity of $J$-automorphisms and multiplicative recognizer costs in the foundation layer.
Single-rung balance requires $\rho=1/(1+\rho)$ at one rung. The unique positive fixed point is $\varphi^{-1}$. Together the two axioms pin the entire discrete law; the continuum kernel $K(z)=1/(1+z)$ is the lattice interpolation.
proof idea
No proof body: this is a structure definition packing four fields (the map, positivity, Cauchy multiplicativity on $\mathbb{N}$, and the one-step fixed-point equation). Downstream theorems discharge uniqueness by solving the functional equation: positivity plus $\mathrm{occ}(m+n)=\mathrm{occ},m,\mathrm{occ},n$ give $\mathrm{occ},n=(\mathrm{occ},1)^n$, and the balance equation forces $\mathrm{occ},1=\varphi^{-1}$.
why it matters
This is the kernel object of "The Forced Redshift Kernel." Downstream, $\mathrm{occ}$ is forced to $\varphi^{-n}$, equivalently $1/(1+z)$ on the rung lattice, and the power-kernel class $K_s(z)=(1+z)^{-s}$ is pinned at $s=1$ (excluding volume $s=3$ and spacetime $s=4$ dilution).
The one-statement summary theorem packages the consequences: CPL on the thawing line $w_a=-(1+w_0)$, $w_0\in(-1,-0.88)$, and no phantom crossing. Measure forcing identifies the same structure with the forced lattice weight ($\mathrm{occ},n=\varphi^{-n}$ is the T9 measure), via a field-for-field coercion from recognition weight rules. Open remain the BIT aging mechanism itself, single-channel 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.