forcedQuotientToBool_representative
plain-language theorem explainer
From any distinction witness on a type, the forced map from the observable quotient to Bool sends each distinguished Boolean representative back to that Boolean. Anyone building the quotient–Bool equivalence cites this as the right inverse. The proof is a two-case split on Bool with simplification of the two definitions.
Claim. Let $K$ be any type equipped with a distinction witness $h:\exists x,y\in K,\,x\neq y$. For every Boolean $b$, the forced quotient-to-Boolean map applied to the distinguished representative of $b$ recovers $b$: $\mathrm{quot\to Bool}_h(\mathrm{repr}_h(b))=b$.
background
Module T−1 Forced from a Distinction takes as primitive only a distinction witness $h:\exists x,y\in K,,x\neq y$, not an external admissibility package. From $h$ one constructs a marked pair, the Boolean projection generated by that distinction, the observable equivalence relation it induces, and the resulting two-class quotient.
The forced quotient-to-Boolean map assigns to each class the Boolean name of its projection. The forced Boolean representative sends each Boolean to a chosen class that carries that name. Together they are the two directions of the intended equivalence between the observable quotient and Bool.
This lemma is the right-inverse half of that pair: representatives land on the Boolean they name. The companion left-inverse (every class equals the representative of its Boolean value) is stated immediately after.
proof idea
Term-mode proof by cases on the Boolean $b$. Each branch reduces by simp unfolding the definitions of the forced quotient-to-Boolean map and the forced Boolean representative; both sides become definitionally equal on the true and false cases separately.
why it matters
This is one of the two inverse laws needed to equip the distinction-forced observable quotient with a Boolean coordinate. Downstream, forcedQuotientEquivBool packages the map, the representative section, this right inverse, and the left inverse into an equivalence $\mathrm{Quotient}(\sim_h)\simeq\mathrm{Bool}$.
In the Recognition T−1 repair, that equivalence is the non-half-measure claim: once an object-level distinction is given, the Boolean/observable floor is forced rather than assumed. The module then feeds the legacy raw floor required by RealityCertificate. The result sits below the forcing chain (T0–T8); it does not itself invoke J-uniqueness, $\varphi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.