IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientExamples

   1/-
   2  PrimitiveRecognitionCalculus/QuotientExamples.lean
   3
   4  Worked quotient examples for the Delta-native analysis plan.
   5
   6  `QuotientSelection.lean` proves the general theorem: a quotient is physically
   7  forced exactly by indistinguishability under admitted observables. This file
   8  records three paper-facing examples:
   9
  10  * empty-observable phase quotient: if no observable can read phase, all phases
  11    are identified;
  12  * separating gauge family: if observables separate states, the quotient is
  13    trivial;
  14  * projective-state display: projective equality is just the quotient theorem
  15    specialized to a state space and observable family.
  16
  17  No project-local axioms. No sorry.
  18-/
  19
  20import Mathlib
  21import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientSelection
  22
  23namespace IndisputableMonolith
  24namespace Foundation
  25namespace PrimitiveRecognitionCalculus
  26namespace QuotientExamples
  27
  28open QuotientSelection
  29
  30/-- Toy phase states for the phase-quotient example. -/
  31abbrev PhaseState := ℤ
  32
  33/-- If the admitted observable family is empty, every phase state is
  34indistinguishable and therefore identified by the physical quotient. -/
  35theorem empty_observable_phase_quotient (x y : PhaseState) :
  36    proj (X := PhaseState) (C := ℤ) (∅ : Set (PhaseState → ℤ)) x
  37      = proj (X := PhaseState) (C := ℤ) (∅ : Set (PhaseState → ℤ)) y := by
  38  apply identified_of_obsEquiv
  39  intro f hf
  40  cases hf
  41
  42/-- If all integer-valued observables are admitted, they separate integer states,
  43so the quotient is trivial. -/
  44theorem separating_gauge_family_injective :
  45    Function.Injective (proj (X := ℤ) (C := ℤ) (Set.univ : Set (ℤ → ℤ))) := by
  46  apply proj_injective_of_separating
  47  intro x y h
  48  exact h (fun z => z) (by simp)
  49
  50/-- A generic projective-state quotient: two states have the same physical class
  51exactly when the admitted projective observables cannot distinguish them. -/
  52theorem projective_state_display {State Obs : Type*} (F : Set (State → Obs)) (x y : State) :
  53    proj F x = proj F y ↔ ObsEquiv F x y :=
  54  forced_iff F x y
  55
  56/-- **Quotient examples headline.** Phase with no readable observable collapses,
  57a separating gauge family has trivial quotient, and projective-state display is
  58the quotient theorem specialized to projective observables. -/
  59theorem quotient_examples_headline :
  60    (∀ x y : PhaseState,
  61      proj (X := PhaseState) (C := ℤ) (∅ : Set (PhaseState → ℤ)) x
  62        = proj (X := PhaseState) (C := ℤ) (∅ : Set (PhaseState → ℤ)) y)
  63      ∧ Function.Injective (proj (X := ℤ) (C := ℤ) (Set.univ : Set (ℤ → ℤ)))
  64      ∧ (∀ {State Obs : Type*} (F : Set (State → Obs)) (x y : State),
  65          proj F x = proj F y ↔ ObsEquiv F x y) :=
  66  ⟨empty_observable_phase_quotient, separating_gauge_family_injective,
  67    fun {State} {Obs} F x y => projective_state_display (State := State) (Obs := Obs) F x y⟩
  68
  69end QuotientExamples
  70end PrimitiveRecognitionCalculus
  71end Foundation
  72end IndisputableMonolith
  73