Foundation Primitive Recognition Calculus Quotient Examples

Quotient examples

A quotient is a way of saying two things are the same for all practical purposes. In mathematics, when you divide a set by an equivalence relation, you merge elements that the relation considers equal. The examples here show three ways this plays out when the relation comes from recognition, the framework's word for a discrete record of events that distinguishes states.

First, take a phase state, a toy integer label for a possible configuration. If the set of admitted observables, the functions that read a state and return a value, is empty, then no observable can tell any two states apart. The theorem empty_observable_phase_quotient proves that the quotient identifies every pair of states: the whole space collapses to a single physical class. This is the extreme case where recognition is impossible, so nothing is distinguishable.

Second, admit all integer-valued observables on integer states. Now the identity function is available, and it separates every pair of distinct integers. The theorem separating_gauge_family_injective proves the quotient map is injective, meaning no two distinct states are merged. This is the opposite extreme: with full information, the quotient is trivial and the physical classes are just the original states.

Third, the general rule. The theorem projective_state_display states that two states have the same physical class exactly when the admitted observables cannot distinguish them. This is the quotient theorem specialized to projective observables, and it ties the examples together: the quotient is always the set of states modulo the relation “indistinguishable by the observables you allow.”

In Recognition Science, these examples establish the basic behavior of the quotient construction that underlies physical identification. The empty case shows that without observables, everything is one; the full case shows that with enough observables, nothing is lost. The general theorem is the definition made precise, and it is what later framework results build on.

/-- If the admitted observable family is empty, every phase state is
indistinguishable and therefore identified by the physical quotient. -/
theorem empty_observable_phase_quotient (x y : PhaseState) :
    proj (X := PhaseState) (C := ℤ) (∅ : Set (PhaseState → ℤ)) x
      = proj (X := PhaseState) (C := ℤ) (∅ : Set (PhaseState → ℤ)) y := by
  apply identified_of_obsEquiv
  intro f hf
  cases hf

/-- If all integer-valued observables are admitted, they separate integer states,
so the quotient is trivial. -/
theorem separating_gauge_family_injective :
    Function.Injective (proj (X := ℤ) (C := ℤ) (Set.univ : Set (ℤ → ℤ))) := by
  apply proj_injective_of_separating
  intro x y h
  exact h (fun z => z) (by simp)

/-- A generic projective-state quotient: two states have the same physical class
exactly when the admitted projective observables cannot distinguish them. -/
theorem projective_state_display {State Obs : Type*} (F : Set (State → Obs)) (x y : State) :
    proj F x = proj F y ↔ ObsEquiv F x y :=
  forced_iff F x y

What this page does not claim

The quotient examples do not derive the cost function J or any constants of the framework. The empty-observable collapse does not imply that physical states are always indistinguishable in the full framework. The injectivity result holds only for the specific family of all integer-valued observables on integer states.

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/PrimitiveRecognitionCalculus/QuotientExamples.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: