forcedQuotientBoolEquiv
plain-language theorem explainer
Given any type with two distinct points, the observable quotient forced by that distinction is canonically equivalent to Bool. Anyone threading the T−1→T4 spine from a concrete witness cites this coordinate map. The definition is a one-line alias of the upstream forced-quotient-to-Bool equivalence under the local ForcedQuotient abbreviation.
Claim. For any type $K$ and witness $h:\exists x,y\in K.\, x\neq y$, there is a canonical equivalence $\mathrm{ForcedQuotient}(h)\simeq\mathrm{Bool}$, where $\mathrm{ForcedQuotient}(h)$ is the quotient of $K$ by the forced observable setoid generated by $h$.
background
The module DistinctionToT4 opens the closure path from a supplied distinction witness to the early forcing spine (Phase 1 of T−1→T8). The input is not a global Boolean chain: it is a concrete pair of unequal points $h:\exists x,y:K.,x\neq y$.
Upstream, TMinus1ForcedFromDistinction builds the forced observable setoid on $K$ and the quotient $\mathrm{Quotient}(\mathrm{forcedObservableSetoid},h)$, then proves that quotient equivalent to $\mathrm{Bool}$ via forcedQuotientEquivBool. Locally, ForcedQuotient h is the abbreviation of that same quotient: "the observable quotient generated by a distinction witness."
This definition simply re-exports the upstream equivalence under that abbreviation, so later transport of configuration space and recognition-work cost can be stated on the distinction-generated floor rather than on bare global Bool facts.
proof idea
One-line wrapper: the body is exactly the upstream definition forcedQuotientEquivBool h from TMinus1ForcedFromDistinction. No new construction; the type matches because ForcedQuotient h abbreviates Quotient (forcedObservableSetoid h), which is the domain of the upstream equivalence.
why it matters
This coordinate map is the Bool bridge used throughout the distinction-to-T4 spine. Downstream, distinction_forces_T0 packages it as the quotient_bool field of T0_FromDistinction ("A supplied distinction forces T0 on its own observable quotient"), and distinction_forces_T0_spine does the same for the full T−1-to-T4 spine bundle. Simp lemmas forcedQuotientBoolEquiv_emp and forcedQuotientBoolEquiv_join pin empty and join configurations to false and Boolean or, enabling transport of ConfigSpace and recognition cost onto the forced quotient.
In the forcing chain this is the T−1/T0 floor: distinction forces a two-point observable algebra before J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), or $D=3$ (T8). Without threading through this equivalence, later T0–T4 steps would rest on unthreaded global Bool facts rather than on the witness itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.