IndisputableMonolith.Foundation.ObservableFloorWitness
Defines a quotient-aware observable floor: two states on a carrier are observably distinct relative to a relation r, not merely unequal as bare representatives. Gauge and recognition settings take r as physical equivalence. Downstream T−1 forcing imports this as the distinction primitive. The module packages the witness type, certificates, and quotient-nontriviality equivalences.
claimAn observable floor on a carrier $K$ relative to an observational relation $r$ is a witness that two states of $K$ are not identified by $r$. When $r$ is equality, this reduces to bare inequality; in general $r$ is meant to be gauge or physical equivalence. The module also supplies certificates and the equivalence between a nontrivial quotient $K/r$ and existence of such a floor.
background
Recognition Science begins the forcing chain from a distinction, not from an external admissibility package. Bare inequality of representatives is too weak once states are identified up to gauge or observational equivalence: two different labels can name the same physical configuration.
This module introduces the observable floor as that refined distinction. On a carrier $K$ with relation $r$, the floor asserts that two states fail to be $r$-related. The doc-comment is explicit that for gauge theories $r$ should be physical equivalence, not raw equality of representatives.
Supporting material ties the floor to setoids and quotients: a nontrivial quotient is equivalent to existence of an observable floor, and certificates package the witness for later forcing steps.
proof idea
Definition and interface module rather than a single deep proof. It introduces the observable-floor witness relative to $r$, the certificate wrapper, and lemmas connecting bare equality, setoid quotients, and nontriviality of $K/r$. One direction shows bare distinction does not imply observable distinction when $r$ is coarser than equality; another equates quotient nontriviality with existence of a floor witness.
why it matters in Recognition Science
Feeds TMinus1ForcedFromDistinction, the non-half-measure T−1 repair whose primitive is a distinction witness rather than an external admissibility package. Without a quotient-aware floor, forcing from "there exist two states" collapses under gauge identification and cannot launch the T0–T8 chain (J-uniqueness, $\varphi$, eight-tick octave, $D=3$). This module is the Foundation cut-point that makes "distinction" mean observationally real before cost, $\varphi$-ladder, or dimension arguments begin.
scope and limits
- Does not construct a concrete physical carrier or choose a specific gauge relation r.
- Does not prove T−1 or any later forcing step T0–T8.
- Does not assert that bare inequality of representatives is observationally meaningful.
- Does not define J-cost, phi, or mass-ladder structure.
- Does not certify uniqueness of the observational relation r.