Recog Geom Quotient

The recognition quotient

A recognition quotient, written C_R = C/~, is a standard mathematical move applied to a recognition problem. Start with a set C of possible configurations and a recognizer R that assigns each configuration an event. Two configurations are called indistinguishable when R gives them the same event. The quotient simply groups all mutually indistinguishable configurations into one class, and the resulting set of classes is C_R. The canonical projection π sends each configuration to its class.

The construction is classical: it is the same idea as quotienting a group by a normal subgroup or a topological space by an equivalence relation. In the framework, the recognizer R : C → E is the primitive, and the quotient is built from it. The module defines the quotient as the set of equivalence classes under the indistinguishability relation, and the canonical projection as the map taking each configuration to its class.

The module proves three structural facts. First, two configurations have the same quotient class if and only if they are indistinguishable. Second, the event map factors through the quotient: there is a well-defined map R̄ : C_R → E, and applying R̄ to the class of c gives exactly R(c). Third, this induced map R̄ is injective, meaning distinct quotient classes always yield distinct events. The quotient is therefore isomorphic to the image of R, the set of events the recognizer can actually produce.

In Recognition Science, the payoff is that the quotient captures exactly the observable structure. The framework proves that the projection is surjective and the event map is injective, so no information is lost and no spurious distinctions are introduced. The module also shows how to lift any function that respects indistinguishability to the quotient, and how to project local neighborhood structures, so locality survives the collapse. The summary theorem states plainly: the recognition quotient captures exactly the observable structure.

This is a definitional and structural result, not a physical law. The quotient is a tool for organizing what a recognizer can see, and the theorems guarantee the tool behaves correctly. The framework models the recognizer as the primitive and the quotient as the derived object; the theorems are machine-checked in the framework's library of formal theorems.

/-- Two configurations have the same quotient class iff indistinguishable -/
theorem quotientMk_eq_iff {c₁ c₂ : C} :
    recognitionQuotientMk r c₁ = recognitionQuotientMk r c₂ ↔ c₁ ~[r] c₂ :=
  Quotient.eq (r := indistinguishableSetoid r)

/-- The quotient event map makes the diagram commute -/
theorem quotientEventMap_spec (c : C) :
    quotientEventMap r (recognitionQuotientMk r c) = r.R c := rfl

/-- The quotient event map is injective -/
theorem quotientEventMap_injective :
    Function.Injective (quotientEventMap r) := by
  intro q₁ q₂ h
  obtain ⟨c₁, hc₁⟩ := Quotient.exists_rep q₁
  obtain ⟨c₂, hc₂⟩ := Quotient.exists_rep q₂
  simp only [← hc₁, ← hc₂] at h ⊢
  -- h : quotientEventMap r ⟦c₁⟧ = quotientEventMap r ⟦c₂⟧
  -- which means r.R c₁ = r.R c₂
  apply Quotient.sound
  exact h

/-- The quotient is isomorphic to the image of R -/
noncomputable def quotient_equiv_image :
    RecognitionQuotient r ≃ Set.range r.R :=
  Equiv.ofBijective
    (fun q => ⟨quotientEventMap r q,
      Quotient.inductionOn q (fun c => ⟨c, rfl⟩)⟩)
    ⟨fun q₁ q₂ h => by
      simp only [Subtype.mk.injEq] at h
      exact quotientEventMap_injective r h,
     fun ⟨e, c, hc⟩ => ⟨recognitionQuotientMk r c, by simp [quotientEventMap_spec, hc]⟩⟩

/-- Summary: The recognition quotient captures exactly the observable structure -/
theorem recognition_quotient_summary :
    Function.Surjective (recognitionQuotientMk r) ∧
    Function.Injective (quotientEventMap r) := by
  constructor
  · intro q
    obtain ⟨c, rfl⟩ := Quotient.exists_rep q
    exact ⟨c, rfl⟩
  · exact quotientEventMap_injective r

What this page does not claim

The quotient construction is a definitional tool, not a physical law, and does not by itself derive any constants. The module does not specify what the recognizer R is; it works for any recognizer, and the physical content comes from choosing R. The quotient is not claimed to be a manifold or to carry any smooth structure; only the set of classes and the induced event map are constructed.

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/RecogGeom/Quotient.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: