T2_FromDistinction
plain-language theorem explainer
Defines the T2 interface on the observable quotient forced by a distinction witness: exactly two states, distinct, with zero recognition cost selecting the consistent state and positive cost selecting the marked one. Downstream spine theorems cite this as the T2 floor before T3. It is a Prop structure (four fields), not a proved theorem.
Claim. Given a type $K$ and a distinction witness $h:\exists x,y\in K,\, x\neq y$, write $Q_h$ for the forced observable quotient of $h$ and $C$ for the recognition cost transported to $Q_h$. The T2 property on $Q_h$ asserts: (i) every $\Gamma\in Q_h$ equals one of the two Boolean-coordinate states $\Gamma_{\mathrm{cons}}$ or $\Gamma_{\mathrm{mark}}$; (ii) those two states are distinct; (iii) $C(\Gamma)=0$ forces $\Gamma=\Gamma_{\mathrm{cons}}$; (iv) $C(\Gamma)>0$ forces $\Gamma=\Gamma_{\mathrm{mark}}$.
background
The module closes the early forcing spine from a raw distinction witness rather than from a free-floating global Bool. Given $h:\exists x,y\in K,,x\neq y$, the upstream construction builds the forced observable quotient $Q_h=\mathrm{Quotient}(\text{forcedObservableSetoid},h)$ and an equivalence $Q_h\simeq\mathrm{Bool}$. Configuration space and recognition-work cost are transported across that equivalence, so T0–T4 live on the quotient generated by the witness itself.
$Q_h$ (ForcedQuotient) is that quotient. The Boolean-coordinate equivalence supplies two distinguished points: the consistent state (image of false) and the marked state (image of true). The transported recognition cost $C$ is the cost surface used by the T0/T1 floor on $Q_h$.
T2 is the classical two-state cost dichotomy, restated entirely in $Q_h$ coordinates: dichotomy, distinctness, and the zero/positive cost selection rules that tag consistency versus the mark.
proof idea
No proof body: this is a Prop-valued structure (four named fields). Inhabitants are built downstream. The main constructor is the one-step implication from T1 on the same quotient: that theorem fills state_dichotomy by case analysis on the Boolean coordinate of $\Gamma$, obtains states_distinct from injectivity of the equivalence inverse, and discharges the two cost-selection fields from the T1 cost axioms on the transported surface. The top-level forcing theorem then composes that step with the already-forced T1 instance.
why it matters
This is the T2 rung of Phase 1 of the T−1→T8 closure, threaded through the distinction-generated quotient instead of unthreaded global Boolean facts. Parent results: the implication from T1 builds an instance; the forcing theorem packages “distinction ⇒ T2 on $Q_h$”; T0+T2 then force T3 on the same quotient; the early spine structure records T0–T3 together with the observable floor. In the broader chain this is the two-state cost dichotomy that later feeds the eight-tick and dimension steps (T7, T8), but only after the witness-local floor is secured.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.