observableFloorCert
plain-language theorem explainer
The observable-floor certificate packages two facts: bare distinguishability is exactly the equality special case of an observational floor, and raw inequality alone does not force physical distinguishability under an arbitrary relation. Foundation auditors cite it when replacing the absolute bare-floor witness with a quotient-aware floor. The proof is a two-field structure instance filled by the equality-case biconditional and the indiscrete-relation counterexample.
Claim. There is a certificate asserting: (i) for every type $K$, an observational floor under the equality relation holds if and only if there exist $x,y\in K$ with $x\neq y$; (ii) there exist a type $K$ and a binary relation $r$ on $K$ such that $K$ has unequal elements yet no $r$-distinguishable pair (so bare inequality is not automatically physical).
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 indistinguishable. This module separates the notions. An observable floor on a carrier $K$ relative to a supplied relation $r$ is the existence of a pair not related by $r$. Bare inequality is recovered when $r$ is equality.
The legacy absolute-floor witness (on an inhabited carrier) packages meta-level distinguishability of propositions together with a nontrivial specification of $K$, and forces bare distinguishability. The certificate here upgrades that picture: it records both the equality special case and a gauge-blindness counterexample showing that bare inequality does not imply an observable floor for arbitrary $r$.
Upstream, the equality-case biconditional is definitional (reflexivity of $\leftrightarrow$), and the counterexample takes the indiscrete relation on $\mathbb{R}$ (every pair observationally equivalent) while $0\neq 1$.
proof idea
Term-mode structure construction of the certificate proposition. The equality-case field is filled by the in-module biconditional that an observational floor under equality is definitionally the same as existence of unequal elements (proved by Iff.rfl). The raw-inequality field is filled by the sibling counterexample theorem: choose $K=\mathbb{R}$ and $r$ the constantly-true relation, exhibit $0\neq 1$, and note that no pair can witness an $r$-floor because every pair is related. No further tactics or rewriting are required.
why it matters
Closes the T-1 audit gap in the Foundation layer: physical distinguishability must be stated relative to an observational (or gauge) relation, not bare term inequality. The certificate is the theorem-backed packaging of that separation. Downstream use sites are not yet wired in this graph (used-by count is zero), but the module TODO names the intended next layer: a physical quotient theorem whose equality-relation special case recovers the existing absolute-floor witness interface on inhabited carriers, plus Anil's setoid/quotient extension. That bridge would connect this certificate to the logic-native integer setoid and orbit-quotient machinery already present in the foundation stack. No forcing-chain landmark (T5–T8) is directly at stake; the stake is the correctness of the primitive floor before recognition calculus and cost minimality are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.