IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientSelection

   1/-
   2  PrimitiveRecognitionCalculus/QuotientSelection.lean
   3
   4  Phase 7 of the Delta-Native Analysis frontier: when is a permitted quotient
   5  physically forced?
   6
   7  Pure distinction does not identify distinct orbits; quotients are permitted but
   8  not native. Physics, by contrast, identifies states under symmetry: gauge
   9  equivalence, phase identification, charge sectors, projective Hilbert space. The
  10  bridge is recognition. A quotient becomes forced exactly when no admissible
  11  observable can distinguish the two states.
  12
  13  This module formalizes that. Given a family of observables on a state space, two
  14  states are observationally equivalent when every observable returns the same
  15  value on them. The physically forced quotient is the quotient by that relation.
  16
  17  What is proved:
  18
  19  * `ObsEquiv` is an equivalence relation (`obsSetoid`);
  20  * `forced_iff` : two states are identified in the quotient iff observationally
  21                   equivalent (the quotient is exactly the indistinguishability
  22                   collapse, nothing more, nothing less);
  23  * `observable_descends` : every admissible observable factors through the
  24                   quotient (the universal property: the quotient loses no
  25                   observable information);
  26  * `proj_injective_of_separating` : a separating observable family forces the
  27                   trivial quotient (no gauge), so gauge appears precisely when
  28                   observables fail to separate;
  29  * `gauge_from_indistinguishability` : the headline. Indistinguishability under
  30                   all admissible observables is exactly the physically forced
  31                   identification.
  32
  33  This is the Delta origin of gauge symmetry: the quotient is not primitive, it is
  34  forced by the absence of a distinguishing recognition act.
  35
  36  No project-local axioms. No sorry.
  37-/
  38
  39import Mathlib
  40
  41namespace IndisputableMonolith
  42namespace Foundation
  43namespace PrimitiveRecognitionCalculus
  44namespace QuotientSelection
  45
  46variable {X C : Type*}
  47
  48/-- Two states are observationally equivalent under the observable family `F`
  49when every observable in `F` returns the same value on them. -/
  50def ObsEquiv (F : Set (X → C)) (x y : X) : Prop := ∀ f ∈ F, f x = f y
  51
  52theorem obsEquiv_refl (F : Set (X → C)) (x : X) : ObsEquiv F x x := fun _ _ => rfl
  53
  54theorem obsEquiv_symm (F : Set (X → C)) {x y : X} (h : ObsEquiv F x y) : ObsEquiv F y x :=
  55  fun f hf => (h f hf).symm
  56
  57theorem obsEquiv_trans (F : Set (X → C)) {x y z : X}
  58    (hxy : ObsEquiv F x y) (hyz : ObsEquiv F y z) : ObsEquiv F x z :=
  59  fun f hf => (hxy f hf).trans (hyz f hf)
  60
  61/-- Observational equivalence packaged as a `Setoid`. -/
  62def obsSetoid (F : Set (X → C)) : Setoid X where
  63  r := ObsEquiv F
  64  iseqv := ⟨obsEquiv_refl F, obsEquiv_symm F, obsEquiv_trans F⟩
  65
  66/-- The physically forced quotient: the state space modulo indistinguishability. -/
  67abbrev PhysicalQuotient (F : Set (X → C)) : Type _ := Quotient (obsSetoid F)
  68
  69/-- The projection sending a state to its physical (gauge) class. -/
  70def proj (F : Set (X → C)) : X → PhysicalQuotient F := Quotient.mk (obsSetoid F)
  71
  72/-- **The quotient is exactly the indistinguishability collapse.** Two states map
  73to the same physical class iff no admissible observable separates them. The
  74forced quotient adds no identifications beyond indistinguishability and omits
  75none. -/
  76theorem forced_iff (F : Set (X → C)) (x y : X) :
  77    proj F x = proj F y ↔ ObsEquiv F x y :=
  78  Quotient.eq
  79
  80/-- **Universal property.** Every admissible observable descends to the quotient:
  81there is a function on physical classes agreeing with the observable on every
  82state. The quotient loses no observable information. -/
  83theorem observable_descends (F : Set (X → C)) (f : X → C) (hf : f ∈ F) :
  84    ∃ g : PhysicalQuotient F → C, ∀ x, g (proj F x) = f x := by
  85  refine ⟨Quotient.lift f (fun a b hab => hab f hf), ?_⟩
  86  intro x
  87  rfl
  88
  89/-- **No gauge from a separating family.** If the observable family separates
  90states, the projection is injective: the forced quotient is trivial. Gauge
  91identification appears precisely when the observables fail to separate. -/
  92theorem proj_injective_of_separating (F : Set (X → C))
  93    (hsep : ∀ x y, ObsEquiv F x y → x = y) : Function.Injective (proj F) := by
  94  intro x y h
  95  exact hsep x y ((forced_iff F x y).mp h)
  96
  97/-- Indistinguishable states are identified in the quotient. -/
  98theorem identified_of_obsEquiv (F : Set (X → C)) {x y : X} (h : ObsEquiv F x y) :
  99    proj F x = proj F y :=
 100  (forced_iff F x y).mpr h
 101
 102/-- **Phase 7 headline: gauge from indistinguishability.** The physically forced
 103quotient identifies two states iff no admissible observable distinguishes them
 104(`forced_iff`); every observable still descends to it (`observable_descends`); and
 105when observables separate, the quotient collapses to the identity
 106(`proj_injective_of_separating`). Quotient is not a native operation of
 107distinction; it is forced exactly by the absence of a distinguishing recognition
 108act. -/
 109theorem gauge_from_indistinguishability (F : Set (X → C)) :
 110    (∀ x y : X, proj F x = proj F y ↔ ObsEquiv F x y)
 111      ∧ (∀ f ∈ F, ∃ g : PhysicalQuotient F → C, ∀ x, g (proj F x) = f x)
 112      ∧ ((∀ x y, ObsEquiv F x y → x = y) → Function.Injective (proj F)) :=
 113  ⟨forced_iff F, fun f hf => observable_descends F f hf, proj_injective_of_separating F⟩
 114
 115end QuotientSelection
 116end PrimitiveRecognitionCalculus
 117end Foundation
 118end IndisputableMonolith
 119