observable_iff_bare_for_eq
plain-language theorem explainer
Bare term distinguishability on a carrier type is exactly the observable-floor condition when the observational relation is equality. Anyone packaging the observable-floor certificate, or arguing that raw inequality is only the equality special case of a quotient-aware floor, cites this. The proof is pure definitional reflexivity after unfolding the floor predicate.
Claim. For any type $K$, the observable-floor witness on $K$ relative to equality is equivalent to bare distinguishability: $\mathrm{ObservableFloor}(K,\,=)\;\leftrightarrow\;\exists\,x,y\in K.\, x\neq y$.
background
Anil Thapa's T-1 audit flagged a physical weakness in treating raw type-theoretic inequality as the primitive 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 an observational relation $r$ is the assertion that two states are not identified by $r$: $\exists x,y\in K.,\neg r(x,y)$. In gauge theories $r$ should be physical/gauge equivalence, not raw equality of representatives. Raw inequality is recovered by specializing $r$ to equality.
The present statement records that specialization as a biconditional, so later certificate packaging can name the equality case without re-unfolding the definition.
proof idea
One-line term proof by Iff.rfl. Unfolding the observable-floor predicate at $r:=(=)$ yields $\exists x,y:,K.,\neg(x=y)$, which is definitionally $\exists x,y:,K.,x\neq y$. No lemmas are applied.
why it matters
Feeds the equality-case field of the observable-floor certificate (observableFloorCert), which packages two facts: (i) bare distinguishability is the equality special case of an observable floor, and (ii) bare inequality does not imply observable distinguishability for an arbitrary observational relation.
That certificate is the formal answer to the T-1 audit: the foundation no longer treats raw $\neq$ as the physical floor. Downstream quotient arguments (nontrivial quotient iff observable floor, setoid-derived witnesses) rest on this clean equality specialization so that gauge or observational relations can replace equality without rewriting the floor interface.
No forcing-chain landmark (T5–T8, RCL, $\varphi$) is directly at stake; the result is infrastructure hygiene for any later claim that a physical state space is observably nontrivial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.