Foundation Observable Floor Witness Quotient Nontrivial Iff Observable Floor

The observable floor

In mathematics, a quotient is a way of grouping together objects that are considered equivalent for a given purpose. The Recognition Science framework's machine-checked library of formal theorems contains a result, quotient_nontrivial_iff_observableFloor, that states a precise equivalence: a quotient carrier has at least two distinct elements if and only if there exist two original states that are not identified by the equivalence relation used to build the quotient. In plainer terms, it says that the act of grouping states together produces a non-trivial collection exactly when there is a genuine observable distinction between some pair of states.

This result is a repair. The library's own documentation records that an audit identified a weakness in an earlier primitive notion of a floor: two representatives could be unequal as raw terms while being physically indistinguishable, for example in a gauge theory where different mathematical descriptions correspond to the same physical situation. The new definition, an observable floor (a pair of states not related by a supplied equivalence relation), separates the two notions. The theorem shows that the physical content lives in the quotient, not in raw inequality of representatives.

The library also proves a companion result: raw inequality does not imply observable distinguishability for an arbitrary observational relation. The counterexample is the indiscrete relation on the real numbers, where every pair is observationally equivalent, yet 0 and 1 are distinct as terms. This is the precise sense in which the theorem does not overclaim: it requires an explicit equivalence relation, and it does not assert that any two distinct terms are physically distinct.

Within the framework, this theorem is a building block. It does not by itself establish any physical law or derive any constant. It is a formal, machine-checked statement about how the notion of distinguishability behaves under quotients. The framework's library uses it as a certificate, packaging the equality special case and the counterexample together, to show that the definition is coherent and that the earlier raw-inequality notion is recovered as a special case when the relation is equality.

What a reader can take away is a precise, verified statement about the relationship between quotients and distinguishability, and a clear warning that mathematical inequality is not the same as physical distinction. The theorem does not claim to solve the gauge problem or to provide a physical interpretation of any particular equivalence relation; it provides the formal scaffolding on which such an interpretation would rest.

/-- A quotient carrier is non-singleton exactly when the original carrier has
an observable distinction relative to the quotienting setoid.

This is the quotient-aware repair to the raw-inequality objection: physical
distinguishability lives in `Quotient s`, or equivalently in pairs of
representatives not identified by `s.r`. -/
theorem quotient_nontrivial_iff_observableFloor
    {K : Type*} (s : Setoid K) :
    (∃ a b : Quotient s, a ≠ b) ↔ ObservableFloorWitness K s.r := by
  constructor
  · rintro ⟨a, b, hne⟩
    refine Quotient.inductionOn₂ a b ?_ hne
    intro x y hne'
    refine ⟨x, y, ?_⟩
    intro hxy
    exact hne' (Quotient.sound hxy)
  · rintro ⟨x, y, hxy⟩
    refine ⟨Quotient.mk s x, Quotient.mk s y, ?_⟩
    intro hq
    exact hxy (Quotient.exact hq)

/-- Bare inequality does not imply observable distinguishability for an
arbitrary observational relation. Take the indiscrete relation on `ℝ`, where
every pair is observationally equivalent. -/
theorem bare_distinction_does_not_imply_observable_distinction :
    ∃ (K : Type) (r : K → K → Prop),
      (∃ x y : K, x ≠ y) ∧ ¬ ObservableFloorWitness K r := by
  refine ⟨ℝ, (fun _ _ => True), ⟨?_, ?_⟩⟩
  · exact ⟨0, 1, by norm_num⟩
  · rintro ⟨x, y, hxy⟩
    exact hxy trivial

/-- Raw bare distinguishability is the equality-relation special case of an
observable floor. -/
theorem observable_iff_bare_for_eq (K : Type*) :
    ObservableFloorWitness K (fun x y => x = y) ↔ ∃ x y : K, x ≠ y :=
  Iff.rfl

What this page does not claim

The theorem does not assert that any two distinct terms are physically distinct. The theorem does not provide a physical interpretation of any particular equivalence relation. The theorem does not by itself establish any physical law or derive any constant.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/ObservableFloorWitness.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: