Foundation Observable Floor Witness

The observable floor

In mathematics, two objects are usually considered distinct if they are not equal. But in physics, two descriptions of the same physical situation, such as two gauge-related field configurations, can be different as formal terms while being completely indistinguishable by any measurement. The observable floor, a discrete record of what counts as genuinely different, is the framework's way of separating these two notions.

The core definition is simple. Given a set of states K and an observational relation r that says which states are physically equivalent, an observable floor witness is the statement that there exist two states x and y that are not related by r. This is a formal, machine-checked definition in the framework's library of formal theorems. The plain-language meaning: there is at least one pair of states that physics can tell apart.

The module proves two key facts. First, the old, simpler notion of bare inequality is exactly the special case where the observational relation is equality. If two states are not equal, and the relation is equality itself, then they are observably distinct. This is the theorem observable_iff_bare_for_eq, which is a direct restatement of the definition.

Second, and more importantly, the module shows that bare inequality does not imply observable distinction for an arbitrary relation. The proof gives a concrete counterexample: take the real numbers and let every pair be observationally equivalent. Then 0 and 1 are not equal, but they are not observably distinct, because the relation identifies them. This is the theorem bare_distinction_does_not_imply_observable_distinction. The counterexample is the real line with the indiscrete relation, where every pair is equivalent.

These two results are packaged into a single certificate, a structure that holds both facts. The certificate is itself a theorem, meaning it is fully proved in the machine-checked library. The module also includes a bridge: a quotient carrier is non-singleton exactly when the original carrier has an observable distinction relative to the quotienting relation. This is the quotient-aware repair to the raw-inequality objection.

What this establishes in plain language: the framework's notion of a physical floor, the minimum amount of distinction that must exist, is not about formal inequality of names. It is about observational inequivalence under the right physical relation. For gauge theories, that relation is the gauge equivalence, not raw equality of representatives. The module gives the formal tools to say when two states are truly, physically different, and it proves that the naive notion of inequality is insufficient on its own.

/-- A quotient-aware observable floor on a carrier `K`, relative to an
observational relation `r`. It asserts that two states are not identified by
`r`. For gauge theories, `r` should be the physical/gauge equivalence relation,
not raw equality of representatives. -/
def ObservableFloorWitness (K : Type*) (r : K → K → Prop) : Prop :=
  ∃ x y : K, ¬ r x y

/-- 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

/-- 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

/-- 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)

What this page does not claim

This module does not define what the observational relation should be for any specific physical theory. This module does not prove that any particular pair of states in a real gauge theory is observably distinct.

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: