ObservableFloorWitness
plain-language theorem explainer
An observable floor on a carrier relative to an observational relation is the existence of two states not identified by that relation. Foundation work on the T−1 audit cites it to replace raw type-theoretic inequality with a gauge-aware distinguishability predicate. The body is a one-line existential Prop. Equality recovers the legacy bare-distinction floor as the special case.
Claim. For a type $K$ and a binary relation $r$ on $K$, the observable floor holds when there exist $x,y\in K$ such that $\neg r(x,y)$. When $r$ is equality this is ordinary bare distinguishability; in gauge settings $r$ is meant to be physical/gauge equivalence, not raw equality of representatives.
background
Anil Thapa's T−1 audit flagged a physical weakness in taking 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 is a pair of states not related by a supplied equivalence or observational relation $r$ on a carrier $K$. Raw inequality is recovered when $r$ is equality. The doc-comment stresses that for gauge theories $r$ should be the physical/gauge equivalence, not equality of representatives.
Downstream lemmas make the bridge precise: the equality special case is definitionally bare distinguishability; a setoid witness is exactly an observable-floor witness for the setoid relation; and a quotient is non-singleton iff the original carrier has an observable distinction relative to the quotienting setoid.
proof idea
Definitional, not a proved theorem. The body is the single Prop ∃ x y : K, ¬ r x y. No tactics, no lemmas. Sibling results then specialize or package it: observable_iff_bare_for_eq is Iff.rfl; observableFloorWitness_of_setoid is the identity on the existential; quotient_nontrivial_iff_observableFloor runs quotient induction both ways.
why it matters
This is the quotient-aware repair that lets the early forcing spine start from physical distinction rather than bare term inequality. DistinctionToT0_Spine packages an observable_floor field generated by a supplied distinction, and records that the distinction forces the T−1 floor and T0–T3 on its own observable quotient. forcedObservableFloor in the T−1-from-distinction module consumes the same predicate.
Sibling packaging (ObservableFloorCert) certifies both the equality recovery and the gauge-blindness counterexample (indiscrete relation on ℝ: bare inequality holds, observable floor fails). That counterexample is the concrete reason the framework cannot stay with raw ≠ at the T−1 step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.