T0_FromDistinction
plain-language theorem explainer
Packages T0 (recognition-work surface) on the observable quotient forced by a supplied distinction, not on global Bool. Anyone closing the T−1→T8 spine from a concrete witness cites this interface. It is a Prop structure: Boolean quotient, transported cost, zero iff consistency, and independent additivity.
Claim. Given a type $K$ and a distinction witness $h:\exists x,y\in K,\,x\neq y$, the predicate $\mathrm{T0\_FromDistinction}(h)$ asserts that the forced observable quotient $Q_h$ is Boolean-equivalent, carries a recognition-work cost $C$ with $C(\emptyset)=0$, $C(\Gamma)>0$ whenever $\Gamma$ is inconsistent, $C(\Gamma)=0\Leftrightarrow\Gamma$ is consistent, and $C$ is additive on independent joins.
background
Module DistinctionToT4 opens the closure path from a supplied distinction to the early forcing spine. The point is not to reuse the global Boolean floor while ignoring the witness. From $h:\exists x,y:K,,x\neq y$, the upstream construction builds the forced observable quotient $Q_h=\mathrm{Quotient}(\mathrm{forcedObservableSetoid},h)$ and proves it equivalent to $\mathrm{Bool}$.
A configuration space supplies empty config, join, consistency, and independence. A cost function on that space obeys dichotomy (zero cost iff consistent) and independent additivity. Here those structures are transported across the quotient–Bool equivalence, so T0 lives on the quotient generated by the distinction itself. This is Phase 1 of the full T−1→T8 closure; later T1–T4 route through this transported floor.
proof idea
No proof body: this is a Prop-valued structure (interface bundle), not a theorem. Inhabitants are assembled fieldwise. Downstream distinction_forces_T0 fills the fields by supplying the forced quotient–Bool equivalence, the transported recognition-work certificate, and the transported cost identities (empty cost zero, positive cost on inconsistency, dichotomy, independent additivity).
why it matters
This is the T0 surface threaded through the distinction-generated quotient rather than unthreaded global Bool. Downstream, distinction_forces_T0 shows any distinction forces this package; distinction_T0_to_T1 lifts it to T1 (inconsistency positive, zero cost implies consistent); distinction_T0_T2_to_T3 uses the cheap-empty field toward T3; and DistinctionToT0_Spine records the completed early slice (T−1 floor plus T0–T3 on the quotient). In the forcing chain this is the local T0 step before J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.