DistinctionToT0_Spine
plain-language theorem explainer
Packages the early forcing spine forced by a bare distinction on a carrier K: a marked pair, the T−1 observable floor, Boolean quotient, and T0–T3 on that quotient. Downstream theorems cite it as the Prop that a distinction witness must inhabit. It is a pure structure definition, not a proved theorem; the inhabiting construction lives in distinction_forces_T0_spine.
Claim. For a type $K$ and a distinction witness $h:\exists x,y\in K,\,x\neq y$, the early spine is the conjunction of: a nonempty marked pair in $K$; an observable-floor witness for the forced observable setoid of $h$; a nonempty equivalence between the forced quotient and $\mathrm{Bool}$; and the distinction-relative statements of T0, T1, T2, and T3 on that quotient.
background
The module closes Phase 1 of the T−1→T8 path: start from a supplied distinction $h:\exists x,y\in K,,x\neq y$, build the forced observable quotient, and transport Boolean configuration space and recognition-work cost onto it, rather than quoting a global Bool chain that ignores the witness.
ForcedQuotient h is the quotient of $K$ by the forced observable setoid of $h$; upstream work already shows it is equivalent to $\mathrm{Bool}$. A MarkedPair is a named two-point mark (base, alt, distinct) that seeds Boolean projection. The sibling structures T0_FromDistinction through T3_FromDistinction restate the usual early forcing claims (recognition-work surface, positive cost on inconsistent states, two-state dichotomy, empty-join neutrality) on that quotient rather than on a free Boolean floor.
This structure simply bundles those pieces plus the T−1 floor witness into one Prop, so later theorems can assert the whole early spine in one go.
proof idea
No proof body: this is a structure (Prop bundle). Fields are named hypotheses, not derived conclusions. Inhabitation is deferred to distinction_forces_T0_spine, which fills each field from upstream constructors (markedPairOfDistinction, forcedObservableFloor, forcedQuotientBoolEquiv, and the corresponding T0–T3-from-distinction theorems).
why it matters
This is the public interface for the completed early slice of the distinction-to-T4 closure. The parent theorems distinction_forces_T0_spine and distinction_forces_T0_to_T3 inhabit it: any distinction forces the T−1 floor and T0–T3 on its own observable quotient. That matches the module goal of Phase 1 of the full T−1→T8 forcing chain (primer landmarks T0 onward), routing later steps through a witness-threaded floor instead of unthreaded global Boolean facts. The doc-comment notes that the /reality path also carries T4 via the recognition-operator layer; this structure stops at T3 and leaves that extension outside its fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.