ObservableFloorCert
plain-language theorem explainer
Packages two facts that separate physical observability from raw type inequality: with equality as the relation, an observable floor is exactly the existence of distinct terms; for a general observational relation, bare inequality need not yield an observable floor. Foundation authors cite it when fixing the T-1 audit gap on gauge-blind floors. The structure is a Prop certificate; the inhabited instance is proved elsewhere by two sibling lemmas.
Claim. A certificate asserting (i) for every carrier $K$, there exist $x,y\in K$ with $\neg r(x,y)$ when $r$ is equality if and only if there exist unequal terms in $K$; and (ii) there exist some carrier $K$ and relation $r$ such that $K$ has unequal terms yet no pair is unrelated by $r$ (so bare inequality is not automatically physical distinguishability).
background
Anil Thapa's T-1 audit flagged raw type-theoretic inequality as a weak physical floor: gauge-related or observationally equivalent representatives can be unequal as terms while remaining physically indistinguishable. This module splits the notions. An observable floor on a carrier $K$ relative to an observational relation $r$ is the assertion that some pair of states is not identified by $r$:
$$\mathrm{ObservableFloorWitness}(K,r) :\Leftrightarrow \exists x,y\in K.,\neg r(x,y).$$
For gauge theories, $r$ should be physical/gauge equivalence, not raw equality of representatives. Raw bare distinguishability is recovered exactly when $r$ is equality. The certificate packages that recovery together with a counterexample showing that bare inequality alone does not force an observable floor for arbitrary $r$. Choosing the observational or gauge setoid is where the physical content lives; the bridge to setoids is intentionally transparent.
proof idea
This declaration is a structure (a bundled Prop), not a proved theorem. It has no proof body. The two fields are named hypotheses that any instance must supply: the equality special case, and existence of a gauge-blind counterexample. Downstream, observableFloorCert inhabits the structure by assigning the sibling lemmas observable_iff_bare_for_eq and bare_distinction_does_not_imply_observable_distinction to those fields.
why it matters
The certificate is the audit-facing packaging of the quotient-aware floor. Downstream, observableFloorCert proves the structure is theorem-backed, so later foundation work can depend on a single named Prop rather than two free-floating lemmas. That closes the T-1 weakness: physical distinguishability is stated relative to an observational relation, recovering bare inequality only for equality, and exhibiting that inequality alone is not physical. In the broader Recognition stack this keeps the observable floor honest before quotient constructions (setoids, gauge orbits) feed integers-from-logic and related carrier constructions. It does not itself force dimension, $\varphi$, or the eight-tick octave; it only fixes the meaning of "two states are observably distinct."
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.