ForcedBooleanCoordinates
plain-language theorem explainer
Packages a Boolean coordinate chart on the two-class observable quotient forced by a distinction witness ∃x≠y on a type K. Anyone citing the T−1 floor (canonical coordinates, coordinate change, uniqueness up to Bool automorphism) uses this carrier. It is a pure structure definition: one field, an equivalence Quotient ≃ Bool.
Claim. Given a type $K$ and a distinction witness $h:\exists x,y\in K,\, x\neq y$, a forced Boolean coordinate system is an equivalence $\mathrm{coord}: K/{\sim_h}\simeq\mathrm{Bool}$, where ${\sim_h}$ is the observable equivalence relation generated by the Boolean projection of $h$.
background
The module rebuilds the T−1 floor from a single object-level distinction rather than an external admissibility package. From $h:\exists x,y:K,,x\neq y$ one constructs a marked pair, the Boolean projection it generates, the observable setoid of that projection, and the resulting two-class quotient.
Sibling constructions supply the pieces named in the field type: the forced observable setoid of $h$, the nontrivial two-class quotient, and the equivalence of that quotient with $\mathrm{Bool}$. The structure does not invent new data; it names the coordinate chart as a first-class object so later lemmas can quantify over all such charts.
Local thesis (module doc): once a distinction is given, the Boolean/observable floor is forced, not an extra measure. If there is no distinction, there is no object-level forcing.
proof idea
Definitional packaging only. The structure has a single field coord of type equivalence between the forced observable quotient of $h$ and $\mathrm{Bool}$. No proof obligations; inhabitants are supplied downstream by wrapping the already-built quotient-to-Bool equivalence.
why it matters
Gives the typed carrier for the T−1 Boolean floor forced by distinction. Downstream, the canonical inhabitant fills coord with the forced quotient–Bool equivalence; coordinate change between any two charts is the composite of one inverse with the other; uniqueness up to Boolean automorphism is the identity relating any two charts through that change.
In the Recognition forcing chain this sits below the usual T0–T8 ladder: it is the repaired T−1 step, ensuring the observable Boolean floor is generated by distinction rather than postulated. That floor is what later RealityCertificate-style interfaces expect as the legacy raw floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.