Encyclopedia Foundation Foundation Pair Kernel Production Quotient Identification S23 Canonical Physical

ARTICLE 4 claims 3 theorems 1 hypothesis

Foundation Pair Kernel Production Quotient Identification S23 Canonical Physical

When two physical states look identical to every probe, the framework's canonical map sends them to the same recognition class.

Verify this page

The canonical class map

The declaration establishes a consistency property for how physical states are sorted into recognition classes. In the framework, a recognition event is a discrete record of a system responding to a probe. The declaration states that if two raw physical states are observationally equivalent, meaning every committed probe returns the same result for both, then the canonical map assigns them to the same recognition class. This is a result proved in the machine-checked library.

The practical meaning is that the classification is well-defined: it does not depend on hidden internal details that no probe can distinguish. The result guarantees that the map from raw physical states to recognition classes respects the observational quotient, the set of states identified by all probes. This injective embedding means no hidden observable content can exist beyond the committed response classes. The map is also unique: any map that agrees with the classification on every channel must be the canonical one.

The declaration does not claim that the map is surjective, that every recognition class is actually realized by some physical state. That surjectivity is a separate, still-missing property called the response-realization arrow. The result also does not claim that any particular production system exists or that any system exhausts the recognition classes. Selecting an actual production system and proving it realizes all classes remains a hypothesis.

What the result does establish is a firm lower bound on physical content: whatever a system's raw states are, the observable ones cannot contain more distinctions than the recognition classes themselves. This is the exact sense in which the framework's response classes are the ceiling for physical observation, while leaving open whether that ceiling is reached.

THEOREM canonicalPhysicalClass_respects_probeEquivalence · IndisputableMonolith/Foundation/PairKernelProductionQuotientIdentificationS23.lean
canonicalPhysicalClass_respects_probeEquivalence · IndisputableMonolith/Foundation/PairKernelProductionQuotientIdentificationS23.lean:97 
/-- Unobservable raw implementation differences always map to the same
Recognition response class. -/
theorem canonicalPhysicalClass_respects_probeEquivalence
    {N : ℕ} [NeZero N]
    (system : PostingPhysicalResponseSystem3 N)
    (event : RealizedPostingEvent3 N)
    {left right : system.physical.Carrier event}
    (hindistinguishable :
      ObsEquiv (physicalChannelProbeFamily3 system event)
        left right) :
    canonicalPhysicalClass3 system event left =
      canonicalPhysicalClass3 system event right := by
  apply identified_of_obsEquiv
  intro observation hobservation
  obtain ⟨probe, rfl⟩ := hobservation
  exact
    hindistinguishable
      (fun channel =>
        responseCoordinateObservation3 probe
          (system.respond event channel))
      ⟨probe, rfl⟩
THEOREM productionObservableClassMap_injective · IndisputableMonolith/Foundation/PairKernelProductionQuotientIdentificationS23.lean
productionObservableClassMap_injective · IndisputableMonolith/Foundation/PairKernelProductionQuotientIdentificationS23.lean:144 
/-- The external observational quotient embeds canonically into the committed
Recognition response quotient for every response system. No raw hidden state
can add a physical observable degree without enlarging the probe family. -/
theorem productionObservableClassMap_injective
    {N : ℕ} [NeZero N]
    (system : PostingPhysicalResponseSystem3 N)
    (event : RealizedPostingEvent3 N) :
    Function.Injective
      (productionObservableClassMap3 system event) := by
  intro leftClass rightClass hclasses
  refine
    Quotient.inductionOn₂ leftClass rightClass
      (fun left right hrepresentatives => ?_)
      hclasses
  apply identified_of_obsEquiv
  have hresponses :
      system.respond event left =
        system.respond event right := by
    apply responseCoordinateQuotient_projection_injective
    exact hrepresentatives
  intro observation hobservation
  obtain ⟨probe, rfl⟩ := hobservation
  change
    responseCoordinateObservation3 probe
        (system.respond event left) =
      responseCoordinateObservation3 probe
        (system.respond event right)
  rw [hresponses]
THEOREM productionObservableClassMap_unique · IndisputableMonolith/Foundation/PairKernelProductionQuotientIdentificationS23.lean
productionObservableClassMap_unique · IndisputableMonolith/Foundation/PairKernelProductionQuotientIdentificationS23.lean:173 
/-- The descended map is the unique map with the canonical projection
triangle. -/
theorem productionObservableClassMap_unique
    {N : ℕ} [NeZero N]
    (system : PostingPhysicalResponseSystem3 N)
    (event : RealizedPostingEvent3 N)
    (map :
      ProductionObservableStateQuotient3 system event →
        RecognitionResponseQuotient3)
    (hmap :
      ∀ channel,
        map
            (proj (physicalChannelProbeFamily3 system event)
              channel) =
          canonicalPhysicalClass3 system event channel) :
    map = productionObservableClassMap3 system event := by
  funext stateClass
  refine
    Quotient.inductionOn stateClass
      (fun channel => ?_)
  exact hmap channel
HYPOTHESIS PhysicalObservableStatesAreRecognitionClasses3 · IndisputableMonolith/Foundation/PairKernelProductionQuotientIdentificationS23.lean
PhysicalObservableStatesAreRecognitionClasses3 · IndisputableMonolith/Foundation/PairKernelProductionQuotientIdentificationS23.lean:197 
/-- Target-blind physical-state extensionality and realization after hidden
implementation details have been quotiented out. This is the exact S23
production residual for a named external response system. -/
def PhysicalObservableStatesAreRecognitionClasses3
    {N : ℕ} [NeZero N]
    (system : PostingPhysicalResponseSystem3 N) : Prop :=
  ∀ event,
    Function.Surjective
      (productionObservableClassMap3 system event)

What this page does not claim

The map from physical states to recognition classes is not claimed to be surjective. No specific production system is claimed to exist or to exhaust the recognition classes. The declaration does not claim that the framework's response classes are the only possible ones, only that they are the ceiling for observable distinctions.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND