kernel_dilution_is_measure
plain-language theorem explainer
BIT-kernel rung dilution occupancy equals the forced lattice measure: after n recognition steps the weight is φ^{-n}. Cite this when identifying cosmology rung dilution with the T9 recognition measure, or when discharging lattice-layer clauses of the measure-forcing certificate. The proof is a one-line application of the already-forced occupancy law on RungDilution.
Claim. For every rung-dilution law $L$ (strictly positive occupancy with multiplicative factorization over independent rungs and self-similar single-step balance) and every $n\in\mathbb{N}$, the attenuation $L.occ(n)$ equals the forced lattice weight $\varphi^{-n}$.
background
Module T9 closes the missing weighting rule after the T0–T8 shape chain: given allowed recognition states, how much of reality sits in each? The lattice layer treats recognition as discrete (T2). An admissible weight rule must factorize over independent composition (multiplicative shadow of ledger cost additivity) and obey per-step self-similar balance $\rho=1/(1+\rho)$. That fixed point forces $\rho=\varphi^{-1}$ by the same reciprocal-shift uniqueness that pins T6, hence $w(n)=\varphi^{-n}$.
A RungDilution packages cosmic aging-charge attenuation occ : ℕ → ℝ with positivity, rung factorization, and the self-similar single-step law. Upstream occ_forced states the dilution law is forced: occ n = (1/φ)^n. Sibling latticeWeight is the recognition-side geometric measure (equivalently ρ^n with ρ=φ^{-1}). The conversion toRungDilution exhibits the two packages as the same object; this theorem is the occupancy identity that makes that identification operational.
proof idea
One-line term proof: apply the field theorem occ_forced of the given RungDilution instance at n. That upstream result proceeds by induction on n, using the zero-rung normalization and the two-rung composition law to multiply one more factor of $φ^{-1}$ at each successor. No extra algebra is needed here; the measure side is definitionally the same geometric sequence.
why it matters
This is the lattice-layer hinge of T9 measure forcing: it says the BIT kernel rung dilution is the forced recognition measure, not an independent cosmological ansatz. Downstream measureForcingCert packages lattice forcing, uniqueness, continuum Gibbs form, and nonvacuity; the lattice clauses rest on weight-forced identities of which this is the kernel-side instance.
Framework landmarks: T6 uniqueness of $φ$ supplies the only admissible per-step ratio; factorization mirrors cost additivity behind the Recognition Composition Law; the geometric weight $φ^{-n}$ is the discrete Gibbs rule with rate $\lnφ$ pinned by the self-similar ledger. The public-slice note records that a parallel continuum identity (dimension_dilution_is_measure at $θ=φ^{-4}$) lives against dark-energy dilution outside this slice; the lattice instance retained here carries the same forcing content. Immediately below, the module proves cost-blindness: the forced measure cannot select chirality without a J-asymmetry, closing one road in the mass-derivation program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.