distinction_forces_T2
plain-language theorem explainer
A distinction witness (two unequal elements of a type) forces T2 on the observable quotient that witness generates: every quotient state is one of the two forced Boolean-coordinate states, and those two states are distinct. Anyone closing the early forcing spine from a raw distinction rather than global Bool cites this. Proof is a one-line composition of the T1 force with the T1-to-T2 step.
Claim. Let $K$ be any type and let $h$ witness two unequal elements of $K$. Then the forced observable quotient of $h$ satisfies T2: every quotient state equals one of the two Boolean-coordinate states under the forced equivalence with $\mathrm{Bool}$, and those two states are distinct.
background
This module opens Phase 1 of the T−1→T8 closure: start from a supplied distinction witness $h:\exists x,y:K,,x\neq y$, build the forced observable quotient $\mathrm{Quotient}(\mathrm{forcedObservableSetoid},h)$, and prove it equivalent to $\mathrm{Bool}$. Configuration space and recognition-work cost are then transported across that equivalence, so later T-steps live on the quotient generated by the distinction itself rather than on unthreaded global Boolean facts.
T2 on that quotient is the structure asserting state dichotomy (every quotient state is one of the two forced Boolean-coordinate states) together with distinctness of those two states. Upstream, a parallel theorem already forces T1 on the same quotient; a sibling lemma then lifts any such T1 instance to T2 by unpacking the dichotomy from the T1 data and the forced Bool equivalence.
proof idea
One-line term proof. Apply the sibling lift distinction_T1_to_T2 to the already-proved force distinction_forces_T1 h. The lift fills the T2 structure fields (state dichotomy and distinctness of the two Boolean-coordinate states) from the T1 package on the forced quotient; no extra case analysis is done at this site.
why it matters
Sits on the distinction-threaded path that replaces bare global Bool appeals in the early forcing spine. Downstream, distinction_forces_T3 composes this result with the T0 force to obtain T3 on the same quotient, and distinction_forces_T0_spine packages the full T−1-to-T4 spine (marked pair, observable floor, quotient-Bool equivalence, and the T0–T4 packages) from a single distinction witness. That spine is Phase 1 toward the UnifiedForcingChain landmarks T5 (J-uniqueness), T6 ($\varphi$ fixed point), T7 (eight-tick octave), and T8 ($D=3$). Without this step the T1-to-T2 link would still be global rather than witness-generated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.