forcedQuotientNontrivial
plain-language theorem explainer
Given any type with two distinct elements, the observable quotient forced by that distinction is non-singleton: it carries two unequal classes. Anyone citing the T−1 repair from a bare distinction witness needs this to rule out a collapsed quotient. The proof is a one-line right-to-left application of the quotient-nontriviality equivalence to the forced observable floor.
Claim. If $K$ is any type and there exist $x,y\in K$ with $x\neq y$, then the quotient of $K$ by the forced observable equivalence relation generated from that distinction contains at least two distinct classes.
background
The module treats T−1 as forced from a distinction, not assumed as an external admissibility package. The sole primitive is a witness that $K$ has two unequal elements. From that witness one constructs a marked pair, the Boolean projection it generates, the observable setoid induced by the projection, and the resulting quotient.
Physical distinguishability is phrased at the quotient level. An observable floor witness for a relation $r$ is a pair of points not identified by $r$. Upstream, the equivalence quotient_nontrivial_iff_observableFloor states that a quotient carrier is non-singleton exactly when the original carrier admits such an observable distinction relative to the setoid. The sibling forcedObservableFloor already produces two representatives not related by the forced observable setoid of the given distinction.
proof idea
Term-mode one-liner. Instantiate the equivalence between quotient nontriviality and an observable floor witness at the forced observable setoid of $h$, then take the right-to-left direction. The required floor witness is exactly forcedObservableFloor h, which exhibits the marked base and alternate points as non-related under the forced relation.
why it matters
This is the nontriviality half of the T−1 floor under the strong thesis of the module: once a distinction is supplied, the Boolean/observable floor is forced rather than an extra measure. A singleton quotient would make Boolean coordinates vacuous and collapse the later forced maps to Bool. Sibling constructions (quotient-to-Bool, Boolean representatives, the forced Bool equivalence) sit on this non-degeneracy. In the Recognition chain this is pre-T0 infrastructure: object-level distinction must yield a genuine two-class observable before cost, $\varphi$, or the eight-tick structure can attach. No downstream consumers are recorded yet; the declaration is the local non-degeneracy certificate for the forced quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.