latticeWeight_pos
plain-language theorem explainer
The lattice recognition weight at any finite number of steps is strictly positive. Anyone building the forced geometric φ-measure (Born weights, rung occupancy, continuum Gibbs lift) needs this positivity before taking logs or normalizing. The proof is a one-line term: the weight is a power of the single-step factor ρ = φ⁻¹, and ρ > 0.
Claim. For every natural number $n$, the lattice recognition weight $w(n)$ satisfies $0 < w(n)$. Equivalently, if $w(n) = \rho^n$ with single-step factor $\rho = \varphi^{-1}$, then $w(n) > 0$.
background
Module T9 (MeasureForcing) 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 factorizes over independent composition and obeys per-step self-similar balance $\rho = 1/(1+\rho)$, which forces $\rho = \varphi^{-1}$ by the same reciprocal fixed-point machinery that pins the BIT kernel attenuation.
The lattice weight $w(n)$ is the weight after $n$ recognition steps. Sibling facts record $w(n) = \rho^n$ and $\rho > 0$ (since $\varphi > 1$). Positivity of every finite power is the elementary arithmetic gate before the forced rule $w(n) = \varphi^{-n}$ and before continuum lifts that write probability $\propto \exp(-(\ln\varphi)\cdot\mathrm{cost})$.
proof idea
One-line term proof. The definition identifies the lattice weight at $n$ with the $n$-th power of the single-step factor $\rho$. Apply Mathlib pow_pos to the already-proved sibling $\rho > 0$: a positive real raised to any natural power stays positive. No case split on $n$, no φ-arithmetic beyond what $\rho_\mathrm{pos}$ already encodes.
why it matters
T9’s lattice layer claims any admissible recognition weight is the geometric φ-measure $w(n) = \varphi^{-n}$. Strict positivity is a standing hypothesis for factorization statements, for the conversion toRungDilution that equates this object with BIT rung dilution, and for later continuum Gibbs forms. Without $w(n) > 0$ one cannot take logarithms, form normalized probabilities, or compare costs.
Framework landmarks: T6 uniqueness of φ supplies the only admissible single-step ratio; the reciprocal self-similarity fixed point is the same balance used for θ = φ⁻⁴ and the BIT kernel. Downstream usage is not yet wired in the graph (used_by empty), but sibling RecognitionWeightRule and the module’s weight-forcing theorem are the intended consumers. This is proved scaffolding hygiene, not an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.