forcedBoolRepresentative_left_inv
plain-language theorem explainer
On the two-class observable quotient forced by a distinction witness, every class equals the canonical representative of its Boolean coordinate. Anyone assembling the Bool equivalence for the T−1 floor cites this left-inverse identity. The proof is quotient induction plus a Boolean case split, discharging equality by Quotient.sound against the marked base or alt.
Claim. Let $K$ be any type admitting a distinction witness $h:\exists x,y\in K.\,x\neq y$. Let $Q$ be the quotient of $K$ by the observable equivalence relation generated by the Boolean projection forced by $h$. For every class $q\in Q$, the canonical representative of the Boolean value of $q$ recovers $q$: $\mathrm{repr}_h(\mathrm{toBool}_h(q))=q$.
background
Module T−1 Forced from a Distinction takes as primitive only a distinction witness $h:\exists x,y:K.,x\neq y$, not an external admissibility package. From $h$ one constructs a marked pair (base and alt), the Boolean projection that sends base to false and alt to true (and collapses everything else by that same projection), and the observable setoid whose classes are the fibers of that projection.
The quotient $Q$ therefore has at most two classes. The map $\mathrm{toBool}_h:Q\to\mathrm{Bool}$ reads the Boolean coordinate of a class; the section $\mathrm{repr}_h:\mathrm{Bool}\to Q$ sends false to the class of the marked base and true to the class of the marked alt. This lemma is the left-inverse half of that section–retraction pair.
Upstream scaffolding is ordinary quotient soundness (as in the integer and rational constructions from logic) together with the in-module definitions of the forced projection, representative, and setoid; no external cost or curvature functional is used here.
proof idea
Apply Quotient.inductionOn to reduce to a representative $z:K$. Case-split on whether the forced Boolean projection of $z$ is false.
If false, unfold toBool and repr and apply Quotient.sound: the setoid equates $z$ with the marked base because both project to false.
If not false, deduce the projection is true (Bool is two-valued), unfold again, and apply Quotient.sound equating $z$ with the marked alt. Both branches are pure setoid transport; no arithmetic lemmas are needed.
why it matters
This is the left-inverse field of forcedQuotientEquivBool, the in-module equivalence asserting that the observable quotient generated by a distinction is equivalent to Bool. That equivalence is the non-half-measure T−1 repair: once any object-level distinction exists, the two-class Boolean/observable floor is forced rather than postulated, and feeds the legacy raw floor expected by RealityCertificate.
In the broader Recognition forcing chain this sits below T0–T8: it supplies the discrete Boolean coordinate structure that later steps (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) refine into continuous and geometric content. Closing the left inverse removes any residual choice in how quotient classes are labeled by Bool.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.