forcedObservableFloor
plain-language theorem explainer
Given any carrier with two unequal points, the Boolean projection generated by that distinction yields an observational equivalence that still separates those points. Anyone assembling the T−1 floor from a bare distinction cites this. The proof is a short term construction: feed the marked pair into the floor witness and discharge non-relatedness by unfolding the setoid.
Claim. If $K$ is any type and $h$ asserts $\exists x,y\in K$ with $x\neq y$, then there exist $a,b\in K$ that are not related by the observational equivalence forced by $h$ (equality of the Boolean projection generated by the distinction). Equivalently, the forced observable relation admits an observable floor witness on $K$.
background
The module rebuilds the T−1 interface from one primitive: a distinction witness $\exists x,y:K,,x\neq y$. No external admissibility package is assumed. From that witness one constructs a marked pair, the Boolean projection it generates, the observational equivalence (same Boolean value), the two-class quotient, and the legacy raw floor used by RealityCertificate.
An observable floor witness relative to a relation $r$ is $\exists x,y:K,,\neg r,x,y$. In gauge-style settings $r$ is physical equivalence, not raw equality of representatives. Here $r$ is the forced observational setoid: two points are related exactly when the Boolean projection generated by the distinction assigns them the same bit.
The marked pair extracted from the distinction supplies the two representatives the floor needs. Upstream, that setoid is defined so relatedness is equality of forced Boolean values.
proof idea
Term-mode proof via refine. The floor witness is an existential; instantiate it by the base and alt of the marked pair forced by the distinction. The residual goal is that those two points fail the forced observational relation. Unfolding the setoid turns relatedness into equality of Boolean projections; the marked-pair construction already makes those projections differ, so a single simp on the setoid definition closes the goal.
why it matters
This is the non-half-measure T−1 repair: the legacy raw floor demanded by RealityCertificate is forced rather than postulated once a distinction exists. Downstream, distinction_forces_T0_spine packages it as the observable_floor field of the T−1-to-T4 spine ("A distinction witness forces the T−1-to-T4 spine"), and forcedQuotientNontrivial converts it into nontriviality of the two-class quotient via the standard floor↔quotient equivalence.
In the Recognition forcing chain this sits at T−1, before T0–T8 (J-uniqueness, $\varphi$, eight-tick octave, $D=3$). The strong thesis is preserved: no object-level distinction means no object-level forcing; with a distinction, the Boolean/observable floor is not an extra measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.