distinction_T1_to_T2
plain-language theorem explainer
T1 on the forced quotient of a distinction witness upgrades to T2 on that same quotient. Anyone closing the early forcing spine from a raw distinction (not a global Bool) cites this step. The proof cases on the Bool coordinate of each quotient state, uses injectivity of the forced quotient–Bool equivalence, and transports zero versus positive cost via the recognition-cost transport lemma.
Claim. Let $K$ be a type with a distinction witness $h:\exists x\,y:K,\,x\neq y$. If T1 holds on the forced observable quotient of $h$ (inconsistent states have positive recognition-work cost; zero-cost states are consistent), then T2 holds on that quotient: every state equals one of the two Boolean-coordinate states, those two states are distinct, zero cost selects the consistent state, and positive cost selects the marked state.
background
This module is Phase 1 of the T−1→T8 closure path. Given a distinction witness $h:\exists x,y:K,,x\neq y$, one builds the forced observable quotient of $h$ and proves it equivalent to $\mathrm{Bool}$. Configuration space and recognition-work cost are then transported across that equivalence, so early forcing steps live on the quotient generated by the witness rather than on an unthreaded global Boolean chain.
The forced quotient–Bool map is an equivalence: every quotient state has a unique Boolean coordinate. Recognition-work cost on the quotient is the Boolean recognition cost pulled back along that equivalence; a transport lemma says cost of a quotient state equals cost of its Boolean image.
T1 on the distinction quotient asserts that inconsistent states have strictly positive cost and that zero-cost states are consistent. T2 strengthens this to a two-state dichotomy: every state is one of the two Boolean-coordinate lifts, those lifts are distinct, zero cost picks the consistent lift, and positive cost picks the marked lift.
proof idea
The goal is the four fields of T2 on the forced quotient, assuming T1.
For state dichotomy: take any quotient state $\Gamma$, case on its Boolean image. Injectivity of the forced quotient–Bool equivalence recovers $\Gamma$ as the corresponding Boolean lift.
For distinctness of the two lifts: if the false and true lifts agreed, their Boolean images would agree after applying the equivalence, contradicting $\mathrm{false}\neq\mathrm{true}$.
Zero-cost selects consistency: T1 already gives that a zero-cost state is consistent; rewrite that as Boolean image equal to false, then injectivity yields equality with the false lift.
Positive-cost selects the marked state: again case on the Boolean image. If $\Gamma$ were the false lift, transport plus simplification would force its cost to zero, contradicting positivity by linear arithmetic. Hence $\Gamma$ is the true lift.
why it matters
This is the T1→T2 link on the distinction-generated floor. Downstream, distinction_forces_T2 is the one-line composition of this theorem with the already-proved T1-from-distinction fact, so a raw distinction witness forces full T2 on its own observable quotient.
In the Recognition Science forcing chain, T2 is the two-state dichotomy that precedes the later spine (J-uniqueness, $\varphi$ as self-similar fixed point, eight-tick octave, $D=3$). Routing T2 through the transported quotient, rather than through global Bool facts that ignore the witness, is exactly the Phase 1 design of this module: close T−1→T4 on the floor the distinction itself generates.
The next blocks in the same file continue the spine to T3 and T4 on that same quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.