forcedBoolRepresentative
plain-language theorem explainer
Given any type with two unequal elements, this map sends each Boolean to a canonical class in the two-class observable quotient forced by that distinction: false to the base class, true to the alternate. It is the inverse half of the forced quotient–Bool equivalence. Anyone proving that the observable floor is exactly Bool cites it as the section of the quotient map. The body is a pure case split on Bool using the marked pair extracted from the witness.
Claim. Let $K$ be any type and suppose there exist $x,y\in K$ with $x\neq y$. From that distinction extract a marked pair $(b,a)$ on $K$, and form the quotient of $K$ by the equivalence that identifies points with the same forced Boolean projection. Define a map $\mathrm{Bool}\to K/{\sim}$ by sending $\mathsf{false}$ to the class of $b$ and $\mathsf{true}$ to the class of $a$.
background
The module rebuilds the T−1 floor from a single object-level distinction witness $h:\exists x,y:K,,x\neq y$, rather than from an external admissibility package. From $h$ one constructs a marked pair, the Boolean projection generated by that pair, the observable equivalence relation (points equivalent iff the projection agrees), and the resulting two-class quotient.
The marked pair is obtained by classical choice on the witness: base is the first chosen element, alt the second, with a proof they differ. The forced observable setoid declares $x\sim y$ exactly when the forced Boolean projection takes the same value on $x$ and $y$. The quotient by that setoid is the observable floor this definition lands in.
Local thesis: once a distinction exists, the Boolean/observable floor is forced; without a distinction there is no object-level forcing.
proof idea
Definition by cases on Bool, not a proof. On false, form the quotient class of the base of the marked pair extracted from the distinction witness. On true, form the class of the alternate. Both classes live in the quotient by the forced observable setoid. No lemmas are applied; the construction is the data that later left- and right-inverse theorems discharge.
why it matters
This is the inverse direction of the forced quotient–Bool equivalence in the same module: that equivalence takes the quotient map as toFun and this representative map as invFun, with left inverse proved by induction on the quotient. The companion simp lemma records that the quotient map sends these two representatives back to their Boolean names.
In the Recognition T−1 repair, the strong claim is that a mere distinction forces a two-valued observable floor. The representative map exhibits the two classes concretely, so uniqueness of Boolean coordinates up to automorphism and the legacy raw floor for RealityCertificate can be stated without an extra Boolean axiom. It sits upstream of the full equivalence and of the left-inverse identity that every class equals the representative of its Boolean value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.