forcedQuotientToBool
plain-language theorem explainer
From any type carrying a distinction witness, the forced Boolean projection descends to a well-defined map from the observable quotient to Bool. Anyone assembling the T−1 floor equivalence (quotient ≃ Bool) cites this map as the forward direction. It is a one-line Quotient.lift: the setoid is equality of projections, so well-definedness is immediate.
Claim. Given a type $K$ and a distinction witness $\exists x,y\in K$ with $x\neq y$, there is a well-defined map $Q(K)\to\mathbf{Bool}$ obtained by lifting the forced Boolean projection through the observable quotient of $K$ (the quotient by the equivalence relation that identifies points with the same forced Boolean value).
background
Module setting is the non-half-measure T−1 repair: the primitive is not an external admissibility package but a distinction witness $h:\exists x,y:K,,x\neq y$. From $h$ one constructs a marked pair, the Boolean projection generated by that distinction, the observable equivalence relation generated by the projection, and the resulting two-class quotient.
The forced Boolean projection sends each point of $K$ to a Boolean by comparing it against the marked pair. The forced observable setoid identifies $x\sim y$ precisely when those Boolean values agree. The quotient by that setoid is therefore the coarsest space on which the projection is constant on classes.
This definition is the canonical descent of that projection to the quotient. Downstream it pairs with a Boolean-to-quotient representative section to give the equivalence of the observable quotient with $\mathbf{Bool}$.
proof idea
One-line wrapper via Quotient.lift. Apply the forced Boolean projection as the underlying function on $K$. The well-definedness obligation is: if $x$ and $y$ are related in the forced observable setoid, then their projections agree. That is exactly the definition of the setoid relation, so the proof is intro x y hxy; exact hxy.
why it matters
This is the forward half of the T−1 claim that a single object-level distinction forces a Boolean observable floor. It is the toFun of the equivalence between the forced observable quotient and Bool, and it is the map inverted by the left-inverse theorem that every quotient class equals the representative of its Boolean value. The companion simp lemma records that distinguished Boolean representatives map back to their names.
In the Recognition forcing chain this sits at the T−1 floor: once a distinction exists, the two-class Boolean coordinate system is constructed rather than assumed, preserving the strong thesis that nothing in the floor interface is an extra measure. It does not itself touch T5–T8 (J-uniqueness, $\varphi$, eight-tick, $D=3$), but it supplies the Boolean substrate those later steps presuppose when they speak of observable yes/no distinctions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.