boolProjection_canonical_given_mark
plain-language theorem explainer
Given a marked pair on a carrier, the induced Boolean projection sends the marked base to false and the marked alternative to true. Anyone citing the T-1 Boolean floor or distinction-forced projections needs this evaluation lemma. The proof is a short classical split on the definition, using distinctness only for the alternative point.
Claim. For any type $K$ and any marked pair $m=(b,a)$ on $K$ with $b\neq a$, the Boolean projection $\pi_m:K\to\{\mathsf{false},\mathsf{true}\}$ determined by $m$ satisfies $\pi_m(b)=\mathsf{false}$ and $\pi_m(a)=\mathsf{true}$.
background
The module treats the T-1 Boolean floor: a non-singleton carrier supplies at least one two-point shadow, but a larger carrier does not choose that shadow uniquely. Canonicity appears only after a distinguishing mark is fixed.
A marked pair on a carrier $K$ is a named two-point mark: a base point $b$, an alternative $a$, and a proof $b\neq a$. The Boolean projection determined by that mark is the map sending the base to $\mathsf{false}$ and every non-base point to $\mathsf{true}$. This lemma records the two evaluation facts that make the mark's intended Boolean labels hold on the nose.
proof idea
Classical reasoning, then constructor on the conjunction. The base conjunct is immediate by simp on the definition of the projection (the if z = base branch). For the alternative, first rewrite distinctness to $a\neq b$, then simp with that inequality so the projection takes the non-base branch and returns $\mathsf{true}$.
why it matters
This is the positive half of the Boolean-projection-from-mark certificate: booleanProjectionFromMarkCert packages it with the companion non-canonicity result (no unique Boolean shadow without a mark). Downstream, the T-1 forcing-from-distinction layer uses it as a one-line source for the simp lemmas that evaluate the forced projection on the base and alternative of the mark extracted from a mere existence of two distinct points. In the Recognition forcing story this pins the Boolean floor once a distinction is chosen, before the later chain steps (J-uniqueness, $\varphi$, eight-tick, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.