latticeWeight_eq_rho_pow
plain-language theorem explainer
After n recognition steps the lattice weight equals ρⁿ, where ρ = φ⁻¹ is the forced per-step weight. Anyone using the discrete geometric measure on recognition states cites this identification. The equality is pure definitional unfolding (rfl): both sides are (1/φ)ⁿ by construction.
Claim. For every natural number $n$, the lattice weight satisfies $w(n) = \rho^n$, where $\rho = \varphi^{-1}$ is the forced per-step weight and $w(n) := (\varphi^{-1})^n$.
background
Module T9 (MeasureForcing) closes the missing weighting rule on recognition states after the T0–T8 chain has fixed the shape of the law (unique J-cost, φ-scale, eight-tick period, D = 3). The lattice layer treats recognition as discrete: a weight rule must factorize over independent composition and obey per-step self-similar balance ρ = 1/(1+ρ), which forces ρ = φ⁻¹.
The constant rho is defined as 1/φ. The lattice weight is defined directly as w(n) = (1/φ)ⁿ — equivalently the geometric measure with one factor of φ⁻¹ per recognition step. This theorem simply records that those two presentations agree: w(n) = ρⁿ.
proof idea
One-line reflexivity. Unfolding the definitions, latticeWeight n is (1/Constants.phi)^n and rho is 1/Constants.phi, so both sides of the claimed equality are definitionally identical; rfl discharges the goal with no lemmas.
why it matters
The geometric lattice measure w(n) = φ⁻ⁿ is the discrete half of the forced recognition weight rule (the continuum half is the Gibbs form ∝ exp(−(ln φ)·cost)). Recording w(n) = ρⁿ makes the per-step generator ρ interchangeable with the closed-form power, which is the form used when the module later proves the weight is forced and exhibits identity with BIT-kernel rung dilution via toRungDilution.
That identification is the same self-similar fixed-point machinery that forced J-uniqueness (T5), φ (T6), and the BIT kernel shape. It supplies the single primitive behind Born weights, chirality selection, δw₀ saturation, η_B, and rung occupancy. No downstream edges are recorded for this lemma itself; it is local glue inside the lattice layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.