forcedObservableSetoid
plain-language theorem explainer
Given any type with two distinct elements, the Boolean projection forced by that distinction induces an equivalence: points are related exactly when they share the same Boolean value. Builders of the T−1 observable floor from a bare distinction witness cite this setoid as the kernel of the projection. Equivalence is immediate from reflexivity, symmetry, and transitivity of Bool equality.
Claim. For any type $K$ and any witness that there exist $x,y\in K$ with $x\neq y$, declare $x\sim y$ if and only if the Boolean projection forced by that witness takes the same value at $x$ and at $y$. The relation $\sim$ is an equivalence relation on $K$.
background
The module rebuilds the T−1 floor from a single object-level distinction witness $\exists x,y:K,,x\neq y$, rather than from an external admissibility package. From the witness one extracts a marked pair, then the Boolean projection generated by that pair, then the observable equivalence whose classes form the two-class quotient.
The forced Boolean projection sends each point of $K$ to a Bool by comparison against the marked base and alternate. Two representatives are observationally indistinguishable precisely when that map agrees on them. Packaging the kernel as a Setoid is what lets the quotient construction produce the observable floor required by the legacy reality-certificate interface.
Upstream, the projection itself is boolProjection applied to the marked pair of the distinction; this definition only records the equality kernel of that map.
proof idea
The relation is defined pointwise as equality of the forced Boolean projection values. The equivalence proof is the standard three-constructor package for equality: reflexivity is rfl, symmetry is .symm on the Bool equality hypothesis, and transitivity is .trans. No domain-specific lemmas are invoked; the argument uses only the equality structure of Bool.
why it matters
This setoid is the carrier of the forced observable quotient used throughout the T−1 repair. Downstream it appears in the forced quotient abbreviation, the Boolean-coordinate structure, the representative section, the quotient-to-Bool equivalence, and the theorem that a distinction forces a two-class Boolean observable floor. The early closure spine DistinctionToT0_Spine records the observable floor generated by the distinction as a field built on this relation.
In the Recognition forcing narrative this is the non-half-measure T−1 step: once an object-level distinction is supplied, the Boolean/observable floor is constructed rather than assumed. Without distinction there is no object-level forcing; with it, the two-class quotient is not an extra measure. That floor is the base on which T0–T3 (and, in the fuller spine, T4) are then forced on the quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.