booleanProjectionFromMarkCert
plain-language theorem explainer
Packages the two marked-pair Boolean-projection facts into a single certificate: every marked pair induces a canonical two-valued shadow (base→false, alt→true), and non-singletonness alone does not pick a unique shadow. Foundation readers of the T-1 Boolean floor cite this. Term-mode structure inhabitant that plugs in the two supporting lemmas.
Claim. There is a certificate asserting: (i) for every marked pair $m$ on a carrier $K$, the induced Boolean projection sends the base point to $\mathrm{false}$ and the alternative to $\mathrm{true}$; (ii) there exist a carrier and two marked pairs on it whose induced Boolean projections are unequal.
background
The module treats the T-1 Boolean floor: a two-valued shadow of a carrier is canonical only after a distinguishing mark is chosen. A non-singleton carrier always admits at least one two-point shadow, but a larger carrier does not select that shadow uniquely.
A marked pair on $K$ is a pair of distinct points (base and alternative). The induced Boolean projection collapses the carrier onto ${\mathrm{false},\mathrm{true}}$ by sending the base to false and everything else (in particular the alternative) to true, once the mark is fixed.
Upstream, boolProjection_canonical_given_mark proves the base/alt evaluation for any marked pair, and bool_projection_not_canonical_without_mark exhibits two inequivalent projections on a three-point carrier, witnessing that non-singletonness alone is not a canonical selector.
proof idea
Short term-mode inhabitant of the certificate structure. The first field is filled by the lemma that every marked pair projects base to false and alt to true. The second field is filled by the existence lemma that a three-point carrier admits two marked pairs with unequal Boolean projections. No extra tactics or rewriting.
why it matters
Closes the local certificate for Boolean projection from a mark in the Foundation layer. The module framing is that the T-1 Boolean floor becomes canonical only after a distinguishing mark is chosen; this declaration packages both the positive canonicity-with-mark fact and the negative non-canonicity-without-mark fact into one Prop-level certificate. No downstream consumers are wired yet in the graph, so it stands as a self-contained foundation token rather than a step inside the T0–T8 forcing chain, the RCL, or the phi-ladder mass formula. It records the discrete choice that any later Boolean-floor argument must either supply a mark or accept non-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.