MarkedPair
plain-language theorem explainer
A marked pair packages two distinct points of a carrier type, naming one as base and one as alternative. It is the minimal data that selects a Boolean shadow on an arbitrary type. Downstream work on the T−1 floor and distinction-to-forcing spines cites it as the witness that a two-valued projection exists. As a structure definition there is no proof body; the inequality field is the only content.
Claim. A marked pair on a carrier $K$ is a triple $(b,a,h)$ with $b,a\in K$ and $h:b\neq a$. The first component is the base point; the second is a distinguished alternative.
background
The module treats the T−1 Boolean floor of Recognition Science: a two-valued projection on a carrier is canonical only after a distinguishing mark is chosen. A non-singleton carrier guarantees some two-point shadow exists, but does not pick one uniquely when $|K|\ge 3$.
A marked pair is exactly that choice: two named, unequal points of $K$. The base is the point that will map to Boolean false; the alternative witnesses that the carrier is not a singleton. No metric, order, or Recognition-cost structure is assumed; the carrier is an arbitrary type.
Related constructions extract a marked pair from a bare distinction witness $\exists x,y,,x\neq y$ by classical choice, and then build the induced map $K\to\mathrm{Bool}$.
proof idea
Pure structure definition: three fields (base, alt, and a proof of inequality). No tactics, no lemmas, no computational content beyond the Prop field distinct. Instantiation is by supplying two terms of $K$ and a proof they differ.
why it matters
This is the data type on which the Boolean-projection story hangs. The induced map boolProjection sends the base to false and every other point to true; canonicity given a mark, and non-canonicity without one, are stated relative to MarkedPair.
The certificate BooleanProjectionFromMarkCert packages those two facts. Upstream of the forcing chain, markedPairOfDistinction builds a marked pair from any distinction witness, and DistinctionToT0_Spine records a nonempty marked pair as the first field of the early T−1/T0–T3 closure. In the Recognition framework this is the concrete carrier-level mark that makes the T−1 Boolean floor well-defined before T0–T8 run.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.