booleanObservableFloor_forced_from_distinction
plain-language theorem explainer
Any inhabited distinction on a type K (two unequal points) forces the observable quotient of K to be Boolean: the quotient by the forced observable setoid is equivalent to Bool. Foundation workers citing the T−1 repair use this as the existence form of that floor. The proof is a one-line term wrapper around the constructed quotient–Bool equivalence.
Claim. Let $K$ be any type and suppose there exist $x,y\in K$ with $x\neq y$. Then the quotient of $K$ by the observable equivalence relation generated by that distinction is equivalent to $\mathrm{Bool}$: the type of such equivalences is nonempty.
background
This module is the non-half-measure T−1 repair. The primitive is not an external admissibility package; it is a distinction witness $h:\exists x,y:K,,x\neq y$. From $h$ the module constructs a marked pair, the Boolean projection generated by the distinction, the observable equivalence relation generated by that projection, the two-class quotient, uniqueness of Boolean coordinates up to Boolean automorphism, and the legacy raw floor expected by RealityCertificate.
The forced observable setoid is that equivalence relation on $K$: two points are identified precisely when the Boolean projection from the distinction cannot separate them. The quotient by that setoid is therefore the coarsest observable floor compatible with $h$. An upstream sibling builds an explicit equivalence from that quotient to Bool (two-class, with canonical representatives).
Local thesis: if there is no object-level distinction there is no object-level forcing; once the distinction is given, the Boolean/observable floor is not an extra measure.
proof idea
One-line term proof. The goal is Nonempty (Quotient (forcedObservableSetoid h) ≃ Bool). It is discharged by packaging the already-constructed equivalence forcedQuotientEquivBool h as an inhabitant of that Nonempty type. No further tactics or algebraic rewriting.
why it matters
Closes the existence half of the T−1 Boolean floor in the strong form: the two-class observable quotient is forced by distinction alone, not postulated. Sits at the end of the in-module construction chain (marked pair → Boolean projection → observable setoid → quotient → Bool equivalence). Feeds the legacy RealityCertificate raw-floor interface described in the module doc.
In the broader Recognition forcing chain this is pre-T0 scaffolding: before J-uniqueness (T5), φ (T6), the eight-tick octave (T7), or D=3 (T8), one needs a minimal observable Boolean distinction. No downstream consumers are wired yet in the graph; the declaration is the public existence statement for that floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.