canonicalForcedBooleanCoordinates
plain-language theorem explainer
Packages the forced quotient-to-Bool equivalence as the standard Boolean chart on the two-class observable quotient generated by a distinction witness. Anyone building the T−1 floor from an object-level inequality cites this as the default coordinate system. The body is a one-field structure instance: coord is set to the already-constructed equivalence.
Claim. Given a type $K$ and a distinction witness $h:\exists x,y\in K,\,x\neq y$, the canonical Boolean coordinates are the structure whose single field is the equivalence $\mathrm{Quotient}(\sim_h)\simeq\mathrm{Bool}$ induced by the forced observable setoid of $h$.
background
The module develops the non-half-measure T−1 repair: the primitive is not an external admissibility package but a distinction witness $h:\exists x,y:K,,x\neq y$. From $h$ one constructs a marked pair, a Boolean projection, the observable equivalence relation generated by that projection, and the resulting two-class quotient.
ForcedBooleanCoordinates is the structure packaging a single equivalence $\mathrm{Quotient}(\mathrm{forcedObservableSetoid},h)\simeq\mathrm{Bool}$. Sibling constructions supply the projection, the setoid, nontriviality of the quotient, a representative map, and the equivalence forcedQuotientEquivBool that identifies the quotient with $\mathrm{Bool}$.
The local thesis is that once a distinction is given, the Boolean/observable floor is forced rather than assumed; without an object-level distinction there is no object-level forcing.
proof idea
One-field structure instance. The definition sets coord equal to the already-proved equivalence forcedQuotientEquivBool h, which maps the forced observable quotient bijectively onto $\mathrm{Bool}$. No further proof obligations; the structure has only that field.
why it matters
Closes the coordinate step of the T−1 floor built from a distinction witness: after the marked pair, Boolean projection, observable setoid, and quotient equivalence are in place, this names the canonical chart. It supports the module claim that everything in the T−1 floor interface is forced by the supplied distinction, preserving the strong thesis at the correct formal level for the legacy raw floor expected by RealityCertificate.
No downstream consumers are recorded yet; the declaration is the named default instance rather than a lemma in a longer chain. Framework role is foundational (pre-T0 distinction floor), not a later forcing step such as J-uniqueness or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.