bool_projection_not_canonical_without_mark
plain-language theorem explainer
On a three-point carrier, two different marked pairs induce unequal Boolean projections. Anyone arguing that the T-1 Boolean floor is forced by non-singletonness alone must cite this negative witness. The proof is a concrete Fin 3 counterexample: swap base and alt and evaluate at a single point.
Claim. There exist a type $K$ and two marked pairs $m_1, m_2$ on $K$ (each a named ordered pair of distinct points) such that the induced Boolean projections differ: the map sending the marked base to $\mathrm{false}$ and every other point to $\mathrm{true}$ is not the same for $m_1$ and $m_2$.
background
The module fixes the status of the T-1 Boolean floor: it 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 pick that shadow uniquely.
A marked pair on a carrier $K$ is a structure with a base point, an alternative point, and a proof they are distinct. The Boolean projection of a marked pair is the function $K \to \mathrm{Bool}$ that sends the base to $\mathrm{false}$ and every non-base point to $\mathrm{true}$. The companion positive fact (same module) shows that once the mark is fixed, this projection is uniquely determined on the marked pair itself.
The present theorem is the matching negative: without a fixed mark, inequivalent projections coexist on the same carrier.
proof idea
Classical proof by explicit witness on $\mathrm{Fin},3$. Build $m_1$ with base $0$ and alt $1$, and $m_2$ with base $1$ and alt $0$ (distinctness by decide). Package the triple $(\mathrm{Fin},3, m_1, m_2)$ and assume for contradiction that the two projections agree as functions. Congruence at the point $0$, followed by simplification of the definition of the projection on each mark, yields $\mathrm{false} = \mathrm{true}$.
why it matters
Feeds the certificate booleanProjectionFromMarkCert, which packages both directions: the projection is canonical given a mark, and is not canonical without one. That certificate is the module's export for the foundation layer.
In the Recognition forcing picture this pins a T-1 prerequisite: Boolean floor structure is not free data extracted from cardinality alone; a mark must be supplied before the floor is unique. The module doc states the same point directly: a larger carrier supplies two-point shadows but does not choose among them. Without this negative lemma the positive uniqueness fact would look stronger than it is.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.