weight_blind_to_label
plain-language theorem explainer
Any cost-sufficient weight on labeled recognition states is chirality-blind: the two mirror labels at a fixed cost receive identical weight. Cited by anyone using the T9 measure-forcing package or the chirality no-go inside it. The proof is a one-line application of the cost-sufficiency field, using reflexivity on the shared cost.
Claim. For any cost-sufficient weight $W$ on labeled states and any real cost $c$, the weight of the true-labeled state at cost $c$ equals the weight of the false-labeled state at cost $c$: $W(\langle c,\mathrm{true}\rangle)=W(\langle c,\mathrm{false}\rangle)$.
background
The module closes T9. The T0–T8 chain already forces the shape of the law (unique cost $J$, scale $\varphi$, eight-tick period, $D=3$). What remained open was the weighting of allowed recognition states: Born weights, chirality selection, $\delta w_0$ saturation, $\eta_B$, and rung occupancy are all projections of that missing primitive. T9 forces the geometric $\varphi$-measure (weight $\varphi^{-1}$ per recognition step; continuum form $\propto\exp(-(ln\varphi)\cdot\mathrm{cost})$).
A cost-sufficient weight is a map from labeled states to reals that factors through cost alone: equal costs imply equal weights. Labeled states pair a real cost with a boolean mirror label (the two chiralities). Cost-sufficiency is exactly T9's premise that the weight sees only the ledger cost, not the label.
proof idea
One-line term proof. The two labeled states share cost component $c$, so reflexivity supplies cost equality. The structure field requiring that equal costs yield equal weights then gives the result directly; no further lemmas are needed.
why it matters
This is the chirality no-go recorded in the module: cost-sufficient weights cannot prefer one mirror label. It is consumed by the master measure-forcing certificate and by the consolidated T9 theorem, which states that reality weights recognition states by one unique rule and is cost-blind (no chirality selection), with partition function $\varphi^2$, mean rung $\varphi$, and the BIT amplitude reduced to one integer in the equilibrium band $w_0\in(-0.896,-0.88)$ for $N\ge 8$.
Within the forcing chain this closes one of the recurring instance-selection gaps left after T5–T8 (J-uniqueness, $\varphi$, eight-tick octave, $D=3$). Chirality is not a free parameter of the measure once cost-sufficiency is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.