Foundation Pair Kernel Production Quotient Identification S23 Hidden Implementat

The hidden implementation

A physical theory that predicts five possible response classes faces an obvious objection: what if a real system carries extra internal states that no test can see? The Recognition Science framework answers this with a deliberately extreme example. It builds a hidden implementation, a physical system whose raw carrier has more states than the five allowed responses, and then proves a theorem about what an observer can actually distinguish.

The theorem, hiddenImplementation_observableQuotient_card_eq_five, states that for this hidden implementation, the quotient of states by all committed probes has exactly five elements. In plain language: even though the system secretly has more internal states than the theory permits, any observer using the allowed tests can only ever see five distinct classes. The extra states are invisible; they collapse into the five recognized responses. This is a theorem in the framework's machine-checked library, meaning the proof is verified by a computer and carries no unproven assumptions.

The result is a sharpening of a more general fact the framework proves: for any physical response system, the map from observable states to recognition classes is injective. That is, no two distinct observable classes can be forced into the same recognition response. The hidden implementation shows the converse is also possible: a system can have more raw states than recognition classes, and the surplus states simply vanish from the observable quotient. The five-class result is a concrete witness to that possibility.

What the theorem does not claim is just as important. It does not say that every physical system has exactly five observable states. It applies to this specific constructed carrier. It does not say that the raw carrier itself is identical to the recognition quotient; in fact, the framework proves the opposite for this example, that the raw carrier is not equivalent to the five recognition classes. And it does not establish that any real production system exists that exhausts the five recognition classes. That remains a hypothesis, not a theorem.

/-- The hidden six-point implementation still has exactly five physical
observational classes. -/
theorem hiddenImplementation_observableQuotient_card_eq_five
    (event : RealizedPostingEvent3 3) :
    Fintype.card
        (ProductionObservableStateQuotient3
          (hiddenImplementationResponseSystem3 3)
          event) = 5 := by
  calc
    Fintype.card
        (ProductionObservableStateQuotient3
          (hiddenImplementationResponseSystem3 3)
          event) =
        Fintype.card RecognitionResponseQuotient3 :=
      Fintype.card_congr
        (productionObservableStateEquiv3
          (hiddenImplementationResponseSystem3 3)
          hiddenImplementation_observableStatesExhaustive
          event)
    _ = 5 :=
      recognitionResponseQuotient_card_eq_five

/-- 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 hiddenImplementation_rawCarrier_not_identified :
    ¬ RawPhysicalCarrierIsRecognitionClasses3
      (hiddenImplementationResponseSystem3 3) := by
  intro hraw
  obtain ⟨pair, hpair⟩ :=
    realizedPrimitivePostingPair3_exists
  let event : RealizedPostingEvent3 3 :=
    ⟨pair, hpair⟩
  have hinjective := (hraw event).1
  have hclasses :
      canonicalPhysicalClass3
          (hiddenImplementationResponseSystem3 3)
          event ExtraResponseState3.ghost =
        canonicalPhysicalClass3
          (hiddenImplementationResponseSystem3 3)
          event
          (ExtraResponseState3.base
            spatialZeroResponse3) := by
    rfl
  exact ExtraResponseState3.noConfusion
    (hinjective hclasses)

What this page does not claim

The theorem does not claim that every physical system has exactly five observable states. The theorem does not claim that any actual production system exists that exhausts the five recognition classes. The theorem does not claim that the raw carrier is identical to the recognition quotient.

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: