forcedBoolProjection_alt
plain-language theorem explainer
From any distinction witness on a type K, the forced Boolean projection sends the alternative of the induced marked pair to true. Researchers building or citing the T−1 floor from a bare object-level distinction use this as a simp fact. The proof is a one-line extraction of the second conjunct of the canonical marked-pair Boolean-projection lemma.
Claim. Let $K$ be any type and let $h$ be a witness that there exist distinct $x,y\in K$. Let $m$ be the marked pair constructed from $h$. Then the Boolean projection forced by $h$ evaluates to $\mathrm{true}$ on the alternative element of $m$.
background
The module develops 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 that witness one constructs a marked pair, the Boolean projection it generates, the observable equivalence relation, the two-class quotient, and the legacy raw floor expected by RealityCertificate.
A marked pair on $K$ is a base/alternative pair of distinct elements. The upstream lemma boolProjection_canonical_given_mark states that the induced Boolean projection sends the marked base to false and the marked alternative to true. The forced Boolean projection and the marked pair of a distinction are the corresponding objects built directly from $h$, so the same orientation holds without an extra assumption.
Sibling facts cover the base case (maps to false), the observable setoid, the quotient, and the equivalence with Bool. The present statement is the alternative half of that orientation package.
proof idea
Term-mode one-liner. Instantiate the upstream theorem boolProjection_canonical_given_mark at the marked pair produced by markedPairOfDistinction from $h$, then project the second conjunct of the resulting conjunction (base maps to false and alt maps to true). No extra rewriting or case analysis is required; the canonical orientation already supplies the claim.
why it matters
This lemma closes the alternative half of the forced Boolean orientation in the T−1-from-distinction construction. The module thesis is that once an object-level distinction is supplied, the Boolean/observable floor is forced rather than assumed: marked pair, projection, setoid, two-class quotient, and legacy floor all follow. The base companion and the quotient-to-Bool equivalence sit beside it; together they underwrite uniqueness of Boolean coordinates up to Boolean automorphism and feed the RealityCertificate floor interface.
In the broader Recognition forcing chain this is pre-T0 infrastructure: without a distinction there is no object-level forcing, but with one the Boolean floor is not an extra measure. No downstream dependents are recorded yet; the declaration is a local simp hinge inside the T−1 package rather than a cited parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.