Foundation Primitive Recognition Calculus Quotient Selection Observable Descends

The descent of observables

In mathematics, a quotient is a way of gluing points together. The Recognition Science declaration observable_descends proves a precise fact about such gluing in the framework's recognition calculus (a formal system where states are compared by what a set of admissible measurements returns on them). The theorem states: if you have a family of observables (functions that assign a value to each state), and you define two states as equivalent when every observable in the family returns the same value on both, then any one of those observables can be re-expressed as a function on the glued-together collection of equivalence classes. In plainer terms, the act of identifying states that no measurement can tell apart does not destroy any information that the measurements themselves carry.

The proof is short and constructive. It uses the standard quotient construction: the new function on equivalence classes simply takes a class, picks any representative state in it, and applies the original observable to that representative. The key check, which the proof performs, is that the result does not depend on which representative you happened to pick, precisely because all states in the same class return the same value on the observable. The declaration is one of three results that together form the framework's Phase 7 headline on gauge: the quotient identifies two states exactly when no admissible observable distinguishes them, every observable still descends to the quotient, and if the observables separate all states, the quotient collapses to the identity (no gluing happens at all).

What the declaration does not claim is just as important. It does not say that the quotient is physically meaningful in any particular theory; it is a purely mathematical statement about a set, a family of functions, and an equivalence relation built from them. It does not assert that the observables in the family are the only ones that exist, nor that the family is closed under composition or any other operation. It does not claim that the quotient is a smooth manifold, a vector space, or any other structure beyond a plain set of equivalence classes. And it does not say that the identification of states is forced by physics; the theorem simply shows what follows if you choose to make that identification. The framework's larger claim, that this quotient is the physically forced one, is a separate assertion that builds on this theorem but is not established by it alone.

/-- **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

/-- **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

/-- **Phase 7 headline: gauge from indistinguishability.** The physically forced
quotient identifies two states iff no admissible observable distinguishes them
(`forced_iff`); every observable still descends to it (`observable_descends`); and
when observables separate, the quotient collapses to the identity
(`proj_injective_of_separating`). Quotient is not a native operation of
distinction; it is forced exactly by the absence of a distinguishing recognition
act. -/
theorem gauge_from_indistinguishability (F : Set (X → C)) :
    (∀ x y : X, proj F x = proj F y ↔ ObsEquiv F x y)
      ∧ (∀ f ∈ F, ∃ g : PhysicalQuotient F → C, ∀ x, g (proj F x) = f x)
      ∧ ((∀ x y, ObsEquiv F x y → x = y) → Function.Injective (proj F)) :=
  ⟨forced_iff F, fun f hf => observable_descends F f hf, proj_injective_of_separating F⟩

What this page does not claim

The quotient is not claimed to be physically meaningful in any particular theory. The observable family is not claimed to be complete or closed under any operation. The identification of states is not claimed to be forced by physics; the theorem only shows what follows if the identification is made.

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: