distinction_forces_T1
plain-language theorem explainer
Any type that admits two distinct elements forces the T1 recognition axioms on the observable quotient generated by that distinction. Citation target for anyone threading the early forcing spine from a raw inequality rather than from global Bool. The proof is a one-line composition: obtain T0 on the forced quotient, then apply the T0-to-T1 transport.
Claim. Let $K$ be any type and suppose $h$ witnesses $\exists x,y\in K$ with $x\neq y$. Then the forced observable quotient of $h$ satisfies T1: every inconsistent configuration $\Gamma$ has strictly positive recognition-work cost, and every zero-cost configuration is consistent.
background
This module closes Phase 1 of the T−1→T8 forcing path. Given a raw distinction witness $h:\exists x,y:K,,x\neq y$, the upstream construction builds the forced observable quotient $\mathrm{Quotient}(\mathrm{forcedObservableSetoid},h)$ and proves it equivalent to $\mathrm{Bool}$. Recognition-work cost and the Boolean configuration space are transported across that equivalence, so all early spine facts live on the quotient generated by the witness itself rather than on an unthreaded global $\mathrm{Bool}$.
T0 on that quotient (from distinction_forces_T0) packages three ingredients: the quotient–Bool equivalence, a recognition-work constraint, and a consistency-is-cheap clause. T1 is the next rung: inconsistent quotient states cost strictly positive work, and zero-cost states are consistent. The structure T1_FromDistinction records exactly those two properties on ForcedQuotient h.
proof idea
One-line term proof. First apply distinction_forces_T0 h to obtain a T0_FromDistinction package on the forced quotient. Then feed that package into distinction_T0_to_T1, which maps T0 fields to T1 fields by renaming: contradiction_expensive becomes inconsistent_positive, and the left-to-right direction of logic_emergent becomes zero_cost_consistent. No new arithmetic is performed.
why it matters
Sits on the distinction-generated floor of the early forcing spine (primer T0–T8 chain, Phase 1 of T−1→T8 closure). Downstream, distinction_forces_T2 is the identical one-step lift from this result, and distinction_forces_T0_spine packages the full T−1-to-T4 bundle that begins here. Without this lemma the spine would still rest on global Bool facts rather than on the witness-generated quotient the module is designed to thread. It does not yet reach J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), or $D=3$ (T8); those remain later chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.