Foundation Primitive Recognition Calculus Quotient Selection

The quotient of indistinguishability

In the Recognition Science framework, a recognition event is a discrete act of distinguishing one state from another. The framework's primitive recognition calculus begins with a set of states and a family of observables, functions that assign a value to each state. The central question is when two states should be considered physically distinct. The answer this construction establishes is exact: two states are the same physical state precisely when no observable in the family returns a different value on them. This relation, called observational equivalence, is what the framework uses to build its physical state space.

The construction is a quotient, a standard mathematical operation that groups equivalent states into single classes. The framework defines this quotient for any family of observables and proves three properties that together make the construction trustworthy. First, the quotient identifies two states if and only if they are observationally equivalent; it adds no identifications beyond indistinguishability and omits none. Second, every observable descends to the quotient, meaning each measurement still gives a well-defined value on the grouped physical classes, so no observable information is lost. Third, if the observable family separates states, meaning every pair of distinct states is distinguished by some observable, then the quotient is trivial: it collapses nothing.

The framework's library, a machine-checked collection of formal theorems, records these results as proved statements. The key theorem, gauge_from_indistinguishability, bundles all three properties into one assertion. The name reflects the physical interpretation: gauge freedom, the idea that multiple mathematical states represent the same physical situation, arises here not as a choice but as a forced consequence of limited observation. When observables cannot tell two states apart, the framework's calculus has no ground to keep them separate.

In Recognition Science, this quotient selection is a foundational step. It establishes that the physical state space is not an arbitrary mathematical object but is determined by the observable family one starts with. The framework models gauge identification as the absence of a distinguishing recognition act, not as a symmetry one imposes by hand. This makes the quotient a structural feature of the theory: it is what the observables force, and nothing more.

/-- **The quotient is exactly the indistinguishability collapse.** Two states map
to the same physical class iff no admissible observable separates them. The
forced quotient adds no identifications beyond indistinguishability and omits
none. -/
theorem forced_iff (F : Set (X → C)) (x y : X) :
    proj F x = proj F y ↔ ObsEquiv F x y :=
  Quotient.eq

/-- **Universal property.** Every admissible observable descends to the quotient:
there is a function on physical classes agreeing with the observable on every
state. The quotient loses no observable information. -/
theorem observable_descends (F : Set (X → C)) (f : X → C) (hf : f ∈ F) :
    ∃ g : PhysicalQuotient F → C, ∀ x, g (proj F x) = f x := by
  refine ⟨Quotient.lift f (fun a b hab => hab f hf), ?_⟩
  intro x
  rfl

/-- **No gauge from a separating family.** If the observable family separates
states, the projection is injective: the forced quotient is trivial. Gauge
identification appears precisely when the observables fail to separate. -/
theorem proj_injective_of_separating (F : Set (X → C))
    (hsep : ∀ x y, ObsEquiv F x y → x = y) : Function.Injective (proj F) := by
  intro x y h
  exact hsep x y ((forced_iff F x y).mp h)

What this page does not claim

This page does not claim the framework has derived any specific physical gauge group, such as the standard model's gauge symmetries. This page does not claim the quotient construction is unique to Recognition Science; it is a standard mathematical operation applied within the framework.

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/QuotientSelection.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: