toRungDilution
plain-language theorem explainer
Any recognition weight rule is definitionally a rung-dilution law: the two structures carry identical premises (positivity, multiplicative factorization, single-step self-similar balance). The conversion is the field-for-field map that lets the BIT kernel forcing theorem apply verbatim to lattice weights. Downstream, weight_forced cites it to conclude w(n) = φ^{-n}.
Claim. Given a recognition weight rule $R$ (a positive map $w:\mathbb{N}\to\mathbb{R}$ that factorizes under independent composition and whose single-step weight satisfies the reciprocal self-similar balance), the same data define a rung-dilution law with occupancy $\mathrm{occ}:=w$.
background
Module T9 closes the missing weighting primitive left open by the T0–T8 forcing chain. That chain fixed the shape of the law (unique cost $J$, scale $\varphi$, eight-tick period, $D=3$) but not how much of reality sits in each allowed recognition state. The lattice layer treats recognition as discrete (T2), so a weight rule is a function of step count alone.
A RecognitionWeightRule packages three mathematical demands: strict positivity of $w(n)$; factorization $w(m+n)=w(m)w(n)$ (multiplicative shadow of ledger cost additivity); and per-step self-similar balance, the fixed-point equation that forces the single-step weight to $\varphi^{-1}$. Upstream, RungDilution is the identical package written for cosmic aging charge attenuation after $n$ $\varphi$-rungs: occupancy, positivity, rung factorization, and one-rung self-similarity. The module doc states the premises are field-for-field the same object.
proof idea
Pure structure coercion, not a proof. The four fields of RungDilution are filled by the four fields of the input weight rule: occupancy from $w$, positivity from $w_\mathrm{pos}$, composition from factorization, and one-rung self-similarity from step self-similarity. No lemmas are invoked; the bodies are definitional equalities of the corresponding hypotheses.
why it matters
This conversion is the hinge of the T9 lattice layer. The theorem weight_forced applies it and then invokes the already-proved rung-dilution forcing (occ_forced) to conclude $R.w,n=\varphi^{-n}$ (equivalently latticeWeight n). Without the identification, the BIT kernel result would not transfer to recognition-state weights.
Framework role: it exhibits that Born weights, chirality selection, $\delta w_0$ saturation, $\eta_B$ prefactors, and rung occupancy are projections of one forced geometric measure—weight $\varphi^{-1}$ per recognition step—rather than independent postulates. It sits downstream of T6 ($\varphi$ uniqueness) and the self-similar attenuation forcing that pins the single-step ratio, and upstream of uniqueness of the lattice measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.