LabeledState
plain-language theorem explainer
A labeled recognition state pairs a real cost with a binary label (L/R chirality or similar). It is the carrier type for T9 cost-sufficient weights: any admissible measure on recognition states is required to factor through cost alone. Downstream chirality no-go and Gibbs-measure forcing cite this structure as the domain of the weight map.
Claim. A labeled recognition state is a pair $(c, \ell)$ with real cost $c \in \mathbb{R}$ and binary label $\ell \in \{\mathrm{false}, \mathrm{true}\}$ (e.g. left/right chirality).
background
Module T9 closes the missing weighting rule after the T0–T8 forcing chain has fixed the shape of the law: unique cost $J$, scale $\varphi$, eight-tick period, and $D=3$. What remained open was how much of reality sits in each allowed recognition state (Born weights, chirality selection, rung occupancy, and related instance-selection problems).
The lattice layer treats recognition as discrete. Weights must factorize over independent composition and obey per-step self-similar balance $\rho = 1/(1+\rho)$, which forces $\rho = \varphi^{-1}$ and thus geometric weights $w(n) = \varphi^{-n}$. The continuum layer lifts this to real additive cost, yielding the Gibbs form $\propto \exp(-( \ln \varphi) \cdot \mathrm{cost})$.
A labeled state is the elementary object on which those continuum weights act: the scalar cost (J-cost of the recognition event or ratio) together with a binary label that can mark chirality or other discrete choice. Upstream cost notions (observer J-cost, multiplicative-recognizer derived cost, PRC quotient cost) all supply the real cost field; the label is free data not forced by cost alone.
proof idea
No proof: this is a structure definition with two fields, a real cost and a Boolean label. It is pure data packaging for the T9 weight interface.
why it matters
T9's cost-sufficiency premise is stated on this type: a weight $w$ is cost-sufficient when equal costs imply equal weights, regardless of label. That structure (CostSufficientWeight) is the immediate consumer and immediately yields the chirality no-go: any cost-sufficient weight assigns equal mass to the two mirror labels at every cost.
Without a labeled carrier, the module could not separate the forced geometric measure (which depends only on cost, pinned by $\varphi$ self-similarity) from discrete choices that look free until cost-sufficiency is imposed. The declaration therefore sits at the hinge between the forced $\varphi$-measure and the open instance-selection problems listed in the module doc (Born weights, chirality, $\delta w_0$, $\eta_B$, rung occupancy).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.