forcedBoolProjection
plain-language theorem explainer
From any witness that a type K carries two distinct points, one obtains a canonical map K → Bool that sends a chosen base point to false and every other point to true. Foundation workers cite this when assembling the T−1 observable floor from a pure distinction rather than an external admissibility package. The definition is a one-line composition of the marked-pair extractor with the Boolean projection of a marked pair.
Claim. Given a type $K$ and a witness $h$ that there exist $x,y\in K$ with $x\neq y$, the forced Boolean projection is the map $K\to\mathrm{Bool}$ obtained by extracting a marked pair $(b,a)$ from $h$ and sending $b$ to $\mathrm{false}$ and every other point of $K$ to $\mathrm{true}$.
background
The module rebuilds the T−1 floor from a single primitive: a distinction witness $h:\exists x,y:K,,x\neq y$. Nothing about admissibility or an external Boolean package is assumed. From $h$ one constructs a marked pair, a Boolean projection, the observable equivalence relation, the two-class quotient, and the legacy raw floor used by RealityCertificate.
A marked pair on $K$ is a base point together with a distinct alternative. The upstream extractor markedPairOfDistinction uses classical choice on $h$ to pick base and alternative and records their inequality. The upstream Boolean projection of a marked pair then maps the base to false and every non-base point to true.
The present definition simply wires those two pieces together, so the Boolean coordinate on $K$ is forced by the distinction rather than postulated.
proof idea
One-line definitional wrapper. Apply the marked-pair extractor to the distinction witness $h$, then feed the resulting marked pair into the Boolean projection of a marked pair. No further proof obligations; the body is pure composition of those two upstream definitions.
why it matters
This is the first constructed (not assumed) Boolean coordinate in the non-half-measure T−1 repair. Downstream, the base and alternative evaluation lemmas record that the forced projection sends the extracted base to false and the alternative to true. The forced observable setoid is defined by equality of values under this projection; the quotient-to-Bool lift and the Boolean representative (with its left-inverse) are built on top of it, culminating in the forced quotient equivalence with Bool.
In the Recognition forcing chain this closes the claim that once an object-level distinction exists, the Boolean/observable floor is not an extra measure. It feeds the legacy raw floor required by RealityCertificate without reintroducing an external admissibility package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.