IndisputableMonolith.Foundation.BooleanProjectionFromMark
Defines a marked two-point pair on a carrier and the induced map to Booleans. With a named mark the projection is canonical; without it, no canonical Boolean structure exists. Foundation material for forcing T−1 from a bare distinction witness. Argument is definitional plus short uniqueness/non-canonicity lemmas and a certificate bundle.
claimA marked pair is a carrier $X$ with a named two-point subset $\{a,b\}\subseteq X$, $a\neq b$. From such a mark one obtains a canonical projection $X\to\{0,1\}$ sending the two marked points to the two Boolean values. Absent a mark, no canonical Boolean projection on $X$ is forced.
background
Recognition Science begins the forcing chain below T0 by treating distinction, not an external admissibility package, as primitive. This module supplies the minimal combinatorial gadget for that step: a named two-point mark inside an arbitrary carrier.
A marked pair packages a type together with two distinguished, unequal elements. The Boolean projection sends those two points to the two values of $\mathrm{Bool}$ (or ${0,1}$) and thereby induces a two-valued labeling. The companion statements record that the projection is unique once the mark is fixed, and that without a mark there is no canonical choice of Boolean structure on the carrier.
The module sits in Foundation and is imported by the T−1 repair that rebuilds the first forcing step from a distinction witness alone.
proof idea
Definition module with thin lemmas. MarkedPair is a structure (carrier plus two named unequal points). boolProjection is the induced map to Bool. Canonicity given a mark is a short uniqueness argument; non-canonicity without a mark is a counterexample-style non-existence claim. BooleanProjectionFromMarkCert packages the definitions and lemmas for downstream import. No deep tactic proof; the content is the interface.
why it matters in Recognition Science
Feeds IndisputableMonolith.Foundation.TMinus1ForcedFromDistinction, the non-half-measure T−1 repair whose primitive is a distinction witness rather than an external admissibility package. By isolating Boolean projection as something that appears only after a named two-point mark, the module makes precise how a bare distinction yields a two-valued structure and nothing more. That is the combinatorial seed for the rest of the forcing chain (T0 onward) without smuggling classical Boolean assumptions into the foundation.
scope and limits
- Does not construct the full T−1 theorem; only the mark and Boolean projection interface.
- Does not force dimension, phi, or the eight-tick octave; those live later in the chain.
- Does not claim every type carries a canonical Bool structure.
- Does not address continuous or measure-theoretic projections.