boolProjection
plain-language theorem explainer
A marked pair on a carrier induces a Boolean-valued map that sends the marked base to false and every other point to true. Anyone working the T-1 Boolean floor or distinction-forced logic cites this as the concrete shadow once a mark is fixed. The body is a classical pointwise equality test against the base.
Claim. Given a marked pair $m=(b,a)$ on a carrier $K$ with $b\neq a$, define the Boolean projection $\pi_m:K\to\{\mathsf{false},\mathsf{true}\}$ by $\pi_m(b)=\mathsf{false}$ and $\pi_m(z)=\mathsf{true}$ for all $z\neq b$.
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 is a named two-point mark inside a carrier $K$: a base point, an alternative, and a proof they are distinct. The Boolean projection is the map determined by that mark. In the Recognition forcing chain this sits under the T-1 distinction layer that precedes the later T0–T8 forcing steps.
Downstream, the same map is reused when a mere existence witness $x\neq y$ is turned into a forced Boolean projection by first packaging the witness as a marked pair.
proof idea
Definition, not a theorem. Under classical logic it is the pointwise function that returns false exactly when the argument equals the marked base, and true otherwise. No lemmas are applied; the body is a single classical exact of that conditional.
why it matters
This is the concrete shadow used throughout the Boolean-from-mark development. The certificate packages that every marked pair yields base $\mapsto$ false and alt $\mapsto$ true, and that non-singletonness alone does not pick a unique two-valued shadow. The companion theorems prove canonicity given a mark and non-canonicity without one (via a three-point carrier with two inequivalent projections).
In TMinus1ForcedFromDistinction, the forced Boolean projection is defined by feeding a distinction witness into this map after converting it to a marked pair. That closes the T-1 step: distinction forces a Boolean floor only once a mark is chosen. The construction is foundational scaffolding for later Recognition logic, not a physical constant derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.