IndisputableMonolith.Foundation.ObservableFloorWitness

   1import Mathlib
   2
   3/-!
   4# Observable Floor Witness
   5
   6Anil Thapa's T-1 audit identified the physical weakness of using raw
   7type-theoretic inequality as the primitive floor: gauge-related or
   8observationally equivalent representatives can be unequal as terms while
   9physically indistinguishable.
  10
  11This module separates the two notions. An observable floor is a pair of
  12states not related by a supplied equivalence or observational relation.
  13Raw inequality is recovered as the special case where the relation is
  14equality.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Foundation
  19namespace ObservableFloor
  20
  21/-- A quotient-aware observable floor on a carrier `K`, relative to an
  22observational relation `r`. It asserts that two states are not identified by
  23`r`. For gauge theories, `r` should be the physical/gauge equivalence relation,
  24not raw equality of representatives. -/
  25def ObservableFloorWitness (K : Type*) (r : K → K → Prop) : Prop :=
  26  ∃ x y : K, ¬ r x y
  27
  28/-- Raw bare distinguishability is the equality-relation special case of an
  29observable floor. -/
  30theorem observable_iff_bare_for_eq (K : Type*) :
  31    ObservableFloorWitness K (fun x y => x = y) ↔ ∃ x y : K, x ≠ y :=
  32  Iff.rfl
  33
  34/-- Bare inequality does not imply observable distinguishability for an
  35arbitrary observational relation. Take the indiscrete relation on `ℝ`, where
  36every pair is observationally equivalent. -/
  37theorem bare_distinction_does_not_imply_observable_distinction :
  38    ∃ (K : Type) (r : K → K → Prop),
  39      (∃ x y : K, x ≠ y) ∧ ¬ ObservableFloorWitness K r := by
  40  refine ⟨ℝ, (fun _ _ => True), ⟨?_, ?_⟩⟩
  41  · exact ⟨0, 1, by norm_num⟩
  42  · rintro ⟨x, y, hxy⟩
  43    exact hxy trivial
  44
  45/-- Certificate packaging the quotient-aware floor and the gauge-blindness
  46counterexample. -/
  47structure ObservableFloorCert : Prop where
  48  /-- Equality recovers the legacy bare-distinguishability floor. -/
  49  equality_case :
  50    ∀ K : Type*, ObservableFloorWitness K (fun x y => x = y) ↔
  51      ∃ x y : K, x ≠ y
  52  /-- Bare inequality alone does not imply observable distinguishability for an
  53      arbitrary relation. -/
  54  raw_inequality_not_physical :
  55    ∃ (K : Type) (r : K → K → Prop),
  56      (∃ x y : K, x ≠ y) ∧ ¬ ObservableFloorWitness K r
  57
  58/-- A setoid witness is exactly an observable-floor witness for the setoid's
  59equivalence relation. This is intentionally a transparent bridge: the physical
  60content is in choosing the observational/gauge setoid. -/
  61theorem observableFloorWitness_of_setoid
  62    {K : Type*} (s : Setoid K) (h : ∃ x y : K, ¬ s.r x y) :
  63    ObservableFloorWitness K s.r :=
  64  h
  65
  66/-- A quotient carrier is non-singleton exactly when the original carrier has
  67an observable distinction relative to the quotienting setoid.
  68
  69This is the quotient-aware repair to the raw-inequality objection: physical
  70distinguishability lives in `Quotient s`, or equivalently in pairs of
  71representatives not identified by `s.r`. -/
  72theorem quotient_nontrivial_iff_observableFloor
  73    {K : Type*} (s : Setoid K) :
  74    (∃ a b : Quotient s, a ≠ b) ↔ ObservableFloorWitness K s.r := by
  75  constructor
  76  · rintro ⟨a, b, hne⟩
  77    refine Quotient.inductionOn₂ a b ?_ hne
  78    intro x y hne'
  79    refine ⟨x, y, ?_⟩
  80    intro hxy
  81    exact hne' (Quotient.sound hxy)
  82  · rintro ⟨x, y, hxy⟩
  83    refine ⟨Quotient.mk s x, Quotient.mk s y, ?_⟩
  84    intro hq
  85    exact hxy (Quotient.exact hq)
  86
  87/-- The observable-floor certificate is theorem-backed. -/
  88theorem observableFloorCert : ObservableFloorCert where
  89  equality_case := observable_iff_bare_for_eq
  90  raw_inequality_not_physical :=
  91    bare_distinction_does_not_imply_observable_distinction
  92
  93/-!
  94## TODO for Anil's setoid/quotient extension
  95
  96The intended next layer is the physical quotient theorem:
  97
  98* backward-compatibility bridge:
  99  the equality-relation special case recovers the existing
 100  `AbsoluteFloorClosure.AbsoluteFloorWitness` interface on inhabited
 101  carriers.
 102-/
 103
 104end ObservableFloor
 105end Foundation
 106end IndisputableMonolith
 107