markedPairOfDistinction
plain-language theorem explainer
From any witness that a carrier type K has two unequal points, classical choice extracts a concrete marked pair (base, alt) with base ≠ alt. This is the first forced object in the T−1 floor: every Boolean projection and observable quotient in the module is built on it. Downstream spine theorems cite it as the distinction-to-mark step. The body is pure choice on the existential and its specification.
Claim. Let $K$ be any type and suppose $\exists\, x,y\in K$ with $x\neq y$. Then there is a marked pair on $K$: points $b,a\in K$ with $b\neq a$, obtained by classical choice on that witness (first the base point, then the alternate).
background
The module treats T−1 as forced by a bare distinction witness $h:\exists x,y:K,,x\neq y$, not by an external admissibility package. Once such an $h$ is given, the Boolean/observable floor is constructed rather than assumed; without object-level distinction there is no object-level forcing.
A marked pair is the named two-point mark structure: fields base, alt in the carrier and a proof base ≠ alt. The Boolean projection determined by a mark sends the base point to false and the alternate to true (and extends by that dichotomy). This definition is the bridge from the raw existential to that structure.
Upstream, the only essential dependency is the MarkedPair structure itself. Other K names in the dependency graph are unrelated constants (bridge ratio, curvature functional, ledger kernels) and do not enter the construction.
proof idea
Noncomputable definition by classical choice, not a tactic proof. Apply Classical.choose to $h$ to obtain the base point. The specification of that choice is again an existential (a point unequal to the base); choose once more for the alternate. The remaining specification is exactly the inequality base ≠ alt, which fills the third field of MarkedPair. No algebraic lemmas are invoked.
why it matters
This is the non-half-measure entry point of the T−1 repair: the primitive is the distinction witness, and the marked pair is the first constructed object. Every subsequent forced object in the module hangs off it: the Boolean projection, the base/alt evaluation lemmas, the Boolean representative into the observable quotient, and the left-inverse relating quotient classes to those representatives.
Downstream, distinction_forces_T0_spine packages it as the marked_pair field of the T−1-to-T4 spine forced by a distinction. That spine is the formal link from bare inequality on a carrier up through the observable floor toward the forcing chain (T0 onward). The module thesis is preserved at the right level: the floor interface is forced by the witness, not smuggled in as an extra measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.