BooleanProjectionFromMarkCert
plain-language theorem explainer
Packages two foundation facts as a Prop certificate: a named two-point mark forces a unique Boolean shadow (base maps to false, alternative to true), while mere non-singletonness does not pick a unique shadow. Downstream code cites the discharged instance when the T-1 Boolean floor must be canonical. Pure structure definition; the obligations are filled by sibling lemmas.
Claim. A certificate asserting: (i) for every carrier $K$ and every marked pair $(b,a)$ on $K$ with $b\neq a$, the induced map $K\to\{\mathrm{false},\mathrm{true}\}$ sends $b\mapsto\mathrm{false}$ and $a\mapsto\mathrm{true}$; (ii) there exist a carrier and two marked pairs inducing unequal Boolean maps.
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 is a named ordered pair of distinct points $(b,a)$ inside a carrier $K$. The Boolean projection determined by that mark sends the base $b$ to $\mathrm{false}$ and every non-base point (in particular the alternative $a$) to $\mathrm{true}$. The certificate simply packages the positive canonicity claim together with the negative uniqueness claim into one Prop-valued structure.
proof idea
No proof body: this is a structure of type $\mathrm{Prop}$ with two fields. Field one is the universal statement that every marked pair induces the base/$\mathrm{false}$, alt/$\mathrm{true}$ shadow. Field two is the existential statement that two different marks can yield two different projections. Discharge is deferred to the sibling theorem that fills the fields with the lemmas on canonicity given a mark and non-canonicity without a mark.
why it matters
Sits in the foundation layer that justifies why Boolean (two-valued) structure appears only after a mark is fixed, matching the module claim that the T-1 Boolean floor is canonical solely post-mark. The sole downstream consumer is the theorem that builds a concrete instance of this certificate from the two sibling lemmas, so later development can depend on a single named package rather than on the separate facts. No forcing-chain step (T0–T8) is closed here; the role is infrastructural packaging for the Boolean-floor story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.