observableFloorWitness_of_setoid
plain-language theorem explainer
Given a setoid on a carrier, any pair of elements not identified by its relation is exactly an observable-floor witness for that relation. Gauge and foundation work cites this as the transparent bridge from setoid language into the observable-floor interface. The proof is purely definitional: the witness proposition is the same existential as the hypothesis.
Claim. For any type $K$ and any setoid $s$ on $K$, if there exist $x,y\in K$ such that $\neg\,s.r(x,y)$, then $K$ admits an observable-floor witness relative to the setoid relation $s.r$ (i.e., a pair of states not identified by that observational equivalence).
background
Anil Thapa's T-1 audit flagged raw type-theoretic inequality as too weak a physical floor: gauge-related or observationally equivalent representatives can be unequal as terms while remaining physically indistinguishable. This module separates the two notions. An observable floor on a carrier $K$ relative to a relation $r$ asserts that two states are not identified by $r$. For gauge theories, $r$ should be the physical or gauge equivalence, not raw equality of representatives.
Formally, the observable-floor witness is the proposition $\exists x,y:K,,\neg r,x,y$. Bare distinguishability is recovered when $r$ is equality. A setoid packages an equivalence relation on $K$; its relation field is the natural input to this interface. The physical content lives in choosing that observational or gauge setoid, not in the bridge itself.
proof idea
One-line term proof. The hypothesis is already $\exists x,y:K,,\neg s.r,x,y$, which is definitionally identical to the observable-floor witness for $s.r$. Unfolding the definition closes the goal; no lemmas are applied.
why it matters
Supplies the transparent setoid bridge into the observable-floor interface that repairs the T-1 raw-inequality objection in the foundation layer. Physical distinguishability is thereby tied to pairs of representatives not identified by the observational relation, equivalently to nontriviality of the quotient carrier. Sibling material in the same module records the quotient-aware repair: a quotient is non-singleton exactly when the original carrier has an observable distinction relative to the quotienting setoid. No downstream consumers are recorded yet; the result is infrastructure for gauge-aware distinguishability arguments rather than a forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.