CostSufficientWeight
plain-language theorem explainer
A cost-sufficient weight is a real-valued assignment on labeled recognition states that depends only on cost, not on the binary label. Anyone proving T9 chirality blindness or the forced measure cites this interface: equal costs force equal weights. It is a pure structure (two fields), not a proved theorem.
Claim. A cost-sufficient weight is a pair $(w,\mathrm{cs})$ where $w$ maps each labeled state (real cost plus a Boolean label) to a real, and $\mathrm{cs}$ asserts: whenever two labeled states have the same cost, $w$ assigns them the same value. Equivalently, $w$ factors through the cost projection.
background
Module T9 closes the missing weighting rule after the T0–T8 forcing chain has fixed the shape of the law (unique $J$, $\varphi$, eight-tick period, $D=3$). The open problem is which measure sits on allowed recognition states: Born weights, chirality selection, $\delta w_0$, $\eta_B$, and rung occupancy are all projections of that single gap.
A labeled state is a pair $(\mathrm{cost},\mathrm{label})$ with real cost and a Boolean (e.g. L/R chirality). Cost itself is the Recognition $J$-cost on the underlying event or ratio; several upstream cost defs (observer $J$-cost, multiplicative-recognizer derived cost, PRC quotient cost) all feed the same additive ledger quantity.
Cost-sufficiency is the T9 premise that the weight may not see the label once cost is fixed. That is the mathematical content of the structure: $w$ is constant on equal-cost fibers.
proof idea
No proof body: this is a structure definition. It packages a weight function $w:\mathrm{LabeledState}\to\mathbb{R}$ together with the propositional field that equal costs imply equal weights. Downstream theorems apply the field directly (e.g. weight_blind_to_label instantiates the two mirror labels at fixed cost and uses reflexivity of equality on the cost component).
why it matters
This is the interface for T9's cost-sufficiency premise and the chirality no-go. The immediate consumer is weight_blind_to_label: any cost-sufficient weight equates the two mirror labels at every cost, so the forced measure cannot select chirality. That fact is packaged into the T9 master certificate MeasureForcingCert and the one-line summary t9_measure_forced ("cost-blind, no chirality selection").
In the broader framework it separates the forced geometric $\varphi$-measure (weight $\varphi^{-1}$ per step, Gibbs form $\exp(-(\ln\varphi)\cdot\mathrm{cost})$) from any label-dependent selection rule. Without cost-sufficiency, instance-selection problems could smuggle a second scale or a preferred handedness; with it, T9 forces the unique ledger measure and closes the chirality branch of the open weighting problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.