forcedBoolProjection_base
plain-language theorem explainer
From any distinction witness on a type (two unequal elements), the forced Boolean projection maps the classically chosen base to false. Foundation authors cite this when building the T−1 observable floor from bare inequality rather than an external admissibility package. The proof is a one-line extraction of the first conjunct of the canonical marked-pair Boolean lemma.
Claim. Let $K$ be a type and suppose $\exists\, x,y\in K$ with $x\neq y$. Extract the marked pair $m$ from that witness by classical choice. Then the Boolean projection forced by the witness satisfies $\pi(m.{\rm base})=\mathsf{false}$.
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 is assumed externally. From $h$ one constructs a marked pair (base and alternative, with a proof they differ), then the Boolean projection generated by that mark, then the observable equivalence and two-class quotient used by the legacy RealityCertificate interface.
A marked pair on $K$ is a pair of distinct elements labeled base and alt. The canonical Boolean projection for a mark sends base to false and alt to true; that fact is already proved as boolProjection_canonical_given_mark. The forced projection in this module is simply that canonical map applied to the marked pair extracted from $h$ by classical choice.
Local thesis (from the module doc): once a distinction is given, the Boolean/observable floor is forced, not an extra measure. If there is no object-level distinction, there is no object-level forcing.
proof idea
One-line term proof. Instantiate the upstream lemma that a marked pair induces a Boolean projection with base $\mapsto$ false and alt $\mapsto$ true, feeding it the marked pair extracted from the distinction witness. Project out the first conjunct. No further rewriting or case analysis.
why it matters
Closes the base half of the forced Boolean coordinate on the T−1 floor: the distinguished base is pinned to false once a distinction exists. Together with the sibling that pins the alternative to true, it licenses the forced observable setoid, the two-class quotient, and the legacy raw floor required by RealityCertificate, all without smuggling in an external Boolean structure.
In the Recognition forcing narrative this is the non-half-measure T−1 repair: the Boolean projection is derived from distinction alone, so later chain steps (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) sit on a floor that is forced rather than postulated. No downstream theorems currently depend on this simp lemma by name; it is infrastructure for the sibling quotient and representative lemmas in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.