Recog Geom Composition

Combining recognizers

In Recognition Science, a recognizer is a rule that assigns a label to each configuration in a space, and two configurations are indistinguishable to that recognizer when it gives them the same label. The central idea of recog geom composition is that recognizers can be combined. Given two recognizers R₁ and R₂, their composite R₁₂ assigns to each configuration the pair of labels (R₁(c), R₂(c)). This is a definition, a choice of how to build a new recognizer from old ones, not a derived fact.

The power of the construction appears in what the composite can see. If either R₁ or R₂ can tell two configurations apart, then the composite can too, because their labels differ in at least one component. The theorem proving this is `composite_distinguishes`. A direct consequence is that the composite's indistinguishability relation is exactly the intersection of the two component relations: two configurations are indistinguishable to R₁₂ precisely when they are indistinguishable to both R₁ and R₂. The theorem `composite_indistinguishable_iff` states this as an if-and-only-if. This means the composite never blurs distinctions that either component made; it can only separate configurations further.

This refinement is the heart of the module. The theorem `refinement_theorem` shows that the composite's recognition quotient, the set of all distinct labels it can produce, maps surjectively onto the quotient of each component. Every class in the finer quotient projects down to a class in the coarser one, and every class in the coarser quotient is hit by some class in the finer one. In plain terms, the composite produces a more detailed picture of the configuration space, one that refines the views of both original recognizers. The module also proves that composition is commutative, `composite_comm_events`, so the order in which recognizers are combined does not matter.

In Recognition Science, this is how richer geometry emerges from simpler measurements. The framework's library, a machine-checked collection of formal theorems, establishes these results as theorems, not as empirical observations. The practical consequence is that any collection of recognizers can be merged into a single recognizer with strictly more resolving power, and this merging is associative and order-independent, allowing complex observations to be built reliably from simple ones.

/-- The composite of two recognizers produces events in the product space.
    This is RG6: composition of recognizers. -/
def CompositeRecognizer (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
    Recognizer C (E₁ × E₂) where
  R := fun c => (r₁.R c, r₂.R c)
  nontrivial := by
    -- Use nontriviality of r₁ to construct distinct events
    obtain ⟨c₁, c₂, hne⟩ := r₁.nontrivial
    use c₁, c₂
    intro heq
    apply hne
    exact (Prod.mk.injEq _ _ _ _).mp heq |>.1

/-- The composite distinguishes configs that either component distinguishes -/
theorem composite_distinguishes (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
    {c₁ c₂ : C} (h : Distinguishable r₁ c₁ c₂ ∨ Distinguishable r₂ c₁ c₂) :
    Distinguishable (r₁ ⊗ r₂) c₁ c₂ := by
  unfold Distinguishable at *
  intro heq
  rw [composite_R_eq] at heq
  have ⟨h1, h2⟩ := (Prod.mk.injEq _ _ _ _).mp heq
  cases h with
  | inl h₁ => exact h₁ h1
  | inr h₂ => exact h₂ h2

/-- Indistinguishability under composite iff indistinguishable under both -/
theorem composite_indistinguishable_iff (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
    (c₁ c₂ : C) :
    Indistinguishable (r₁ ⊗ r₂) c₁ c₂ ↔
    Indistinguishable r₁ c₁ c₂ ∧ Indistinguishable r₂ c₁ c₂ := by
  simp only [Indistinguishable, composite_R_eq, Prod.mk.injEq]

/-- **Refinement Theorem**: The composite quotient refines both component quotients.

    This is the fundamental theorem of recognition composition. It says that
    combining recognizers gives us a "finer" view of configuration space.
    The composite quotient C_{R₁₂} maps onto both C_{R₁} and C_{R₂}.

    Mathematically: there exist surjective maps
      π₁ : C_{R₁₂} → C_{R₁}
      π₂ : C_{R₁₂} → C_{R₂}

    This means the composite recognizer "sees" at least as much structure as
    either component recognizer. -/
theorem refinement_theorem (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
    Function.Surjective (quotientMapLeft r₁ r₂) ∧
    Function.Surjective (quotientMapRight r₁ r₂) :=
  ⟨quotientMapLeft_surjective r₁ r₂, quotientMapRight_surjective r₁ r₂⟩

/-- Composition is commutative up to isomorphism on events -/
theorem composite_comm_events (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
    (r₁ ⊗ r₂).R c = Prod.swap ((r₂ ⊗ r₁).R c) := by
  simp [composite_R_eq]

What this page does not claim

The composite recognizer's labels are not claimed to be physically meaningful on their own. Composition is not claimed to be associative, only commutative. The refinement theorem does not claim the composite quotient is strictly larger, only that it refines the component quotients.

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