forcedQuotientEquivBool
plain-language theorem explainer
Given any type with two distinct elements, the observable quotient generated by that distinction is canonically equivalent to the Booleans. Foundation work citing the T−1 floor from a bare distinction witness uses this equivalence as the coordinate identification. The definition assembles the already-proved forward map, Boolean section, and the two inverse laws into a single `Equiv`.
Claim. Let $K$ be any type and suppose $h$ witnesses $\exists\, x,y\in K$ with $x\neq y$. Write $\sim_h$ for the observable equivalence relation on $K$ generated by the Boolean projection of that distinction. Then the quotient $K/\sim_h$ is equivalent to $\mathrm{Bool}$: there is a canonical bijection $K/\sim_h\simeq\{0,1\}$.
background
The module rebuilds the T−1 floor from a single object-level distinction witness $h:\exists x,y:K,,x\neq y$, rather than from an external admissibility package. From $h$ one constructs a marked pair (base and alternate), the Boolean projection they generate, and the observable setoid whose classes are the fibers of that projection.
The forced observable setoid is the equivalence relation on $K$ that identifies points with the same Boolean mark. Its quotient is therefore at most two-classed. The forward map sends each class to the Boolean value of its mark; the section sends false to the class of the base point and true to the class of the alternate.
Upstream pieces already supply that section (forcedBoolRepresentative) and the left-inverse law that recovering the class from its Boolean mark is identity on the quotient. The companion right-inverse law recovers every Boolean from the class of its representative.
proof idea
Definitional assembly of an Equiv, not a tactic proof. The forward function is the already-defined quotient-to-Bool map. The inverse is the Boolean representative that lands base at false and alternate at true. Left invertibility is the sibling lemma that the representative of a class's Boolean mark recovers the class; right invertibility is the sibling that projecting the representative of a Boolean recovers that Boolean. No further algebraic work occurs in the body.
why it matters
This is the concrete two-sided identification that turns the forced observable quotient into Boolean coordinates. Downstream, booleanObservableFloor_forced_from_distinction packages nonemptiness of such an equivalence as the T−1 floor theorem; canonicalForcedBooleanCoordinates installs this map as the canonical coordinate field; and DistinctionToT4.forcedQuotientBoolEquiv re-exports it under the transported configuration-space name.
In the Recognition forcing chain this closes the non-half-measure T−1 repair: once a distinction exists, the Boolean/observable floor is constructed rather than assumed, feeding the later path toward T4 and the eight-tick structure. It does not itself force the distinction; it only converts a given distinction into Bool coordinates up to the equivalence assembled here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.