IndisputableMonolith.Foundation.BooleanProjectionFromMark
Defines a marked two-point pair inside a carrier and the induced Boolean projection onto that pair. Shows the projection is canonical once a mark is fixed, and fails to be canonical without one. Cited by the T−1 forcing development that takes a distinction witness as primitive. Argument is definitional plus short uniqueness and non-uniqueness lemmas.
claimA marked pair is a named two-point subset of a carrier. Given such a mark, there is a canonical Boolean projection of the carrier onto that pair; without a distinguished mark, no such projection is canonical.
background
Recognition Science begins the forcing chain from a bare distinction rather than an external admissibility package. Before T0–T8 can run, one needs a minimal way to turn a two-point distinction into Boolean structure on a carrier.
This module supplies that bridge. A marked pair is a named two-point mark inside a carrier: two distinguished points together with the data that they are the mark. The Boolean projection maps the carrier onto that pair in the unique way compatible with the mark. The module also records the negative statement that, absent a mark, no projection is forced.
The local setting is pure foundation: Mathlib only, no physics constants or ladder structure yet. Downstream, T−1 Forced from a Distinction imports this module as the non-half-measure repair of the T−1 step.
proof idea
Definition module with short supporting lemmas. MarkedPair packages the two-point mark. boolProjection is the induced map onto the mark. boolProjection_canonical_given_mark is a uniqueness argument once the mark is fixed. bool_projection_not_canonical_without_mark is the corresponding non-uniqueness counterexample when no mark is supplied. A small certificate bundle (BooleanProjectionFromMarkCert) packages the positive and negative facts for downstream import.
why it matters in Recognition Science
Feeds IndisputableMonolith.Foundation.TMinus1ForcedFromDistinction, the non-half-measure T−1 repair. That module takes a distinction witness as primitive and needs a canonical Boolean projection once two points are marked; this file is exactly that interface.
In the broader forcing chain, T−1 sits before T0–T8 (J-uniqueness, phi as self-similar fixed point, eight-tick octave, D = 3). Without a clean mark-to-Boolean step, the distinction-based start of the chain is incomplete. The module closes that gap definitionally and with uniqueness, so later forcing steps can assume Boolean structure without smuggling an external admissibility package.
scope and limits
- Does not construct the full T−1 forcing theorem; only the mark-to-Boolean interface.
- Does not introduce J-cost, phi, or any later forcing-chain constants.
- Does not claim uniqueness of Boolean structure on an unmarked carrier.
- Does not address multi-point or continuous carriers beyond the two-point mark.