Foundation Pair Kernel Production Quotient Identification S23 Committed Response

The exhaustion split

The declaration committed_response_ancestry_admits_observableExhaustion_split is a theorem in the framework's machine-checked library of formal theorems. In plain language it proves that there exist two physical response systems, each of which reads the full set of forced recognition responses, but which differ in a specific way: one system's observable states exhaust all the recognition classes, while the other system's observable states do not. Both systems share the same committed response ancestry, meaning every response they can produce is one of the forced classes. The split is not about whether responses are correct, but about whether the states a system can observe cover the entire range of recognition classes.

The theorem is a constructive existence result. It names two concrete systems, left and right, and proves the four properties that define the split: both read the forced responses, the left system's observable states are exhaustive over the recognition classes, and the right system's are not. The right system is built from a hidden implementation that carries extra states beyond the recognition classes; its observable quotient still has five classes, matching the recognition quotient, but the raw carrier itself is not identified with the recognition classes. The left system is the observable production system built from an exhaustive state space.

The split matters because it separates two notions that might otherwise be conflated. Reading the forced responses is one property; having observable states that cover all recognition classes is another. The theorem proves these are independent, in the sense that neither implies the other across all systems. It also shows that hidden implementation duplicates are allowed and collapse under observation, while a newly admitted observable enlarges the probe algebra, as a separate theorem proves: adding one extra observable raises the quotient cardinal from five to six.

What the theorem does not claim is just as important. It does not prove that any actual production system exhausts the recognition classes. The docstring states plainly that no committed declaration names a production system, so the strongest theorem-backed result is a canonical observational embedding plus the exact realization residual for any candidate system. Selecting an actual production system and proving it exhausts the recognition classes remains a hypothesis, not a theorem. The split establishes the logical space of possibilities, not which possibility the physical world occupies.

/-- Committed response ancestry does not force physical observable
exhaustion. This is the active ancestry obstruction, transported from S21's
full/incomplete split. -/
theorem committed_response_ancestry_admits_observableExhaustion_split :
    ∃ left right : PostingPhysicalResponseSystem3.{0} 3,
      PhysicalChannelsReadRecognitionForcedResponses3 left ∧
        PhysicalChannelsReadRecognitionForcedResponses3 right ∧
        PhysicalObservableStatesAreRecognitionClasses3 left ∧
        ¬ PhysicalObservableStatesAreRecognitionClasses3 right := by
  obtain
    ⟨left, right, hleftReads, hrightReads,
      hleftRealizes, hrightNotRealizes⟩ :=
    committed_response_ancestry_admits_realization_split
  refine
    ⟨left, right, hleftReads, hrightReads,
      (physicalObservableStates_iff_forcedResponsesRealized
        left).2 hleftRealizes, ?_⟩
  intro hright
  exact hrightNotRealizes
    ((physicalObservableStates_iff_forcedResponsesRealized
      right).1 hright)

/-- Observable extras are different: admitting S22's detector enlarges the
committed quotient to six classes. -/
theorem observableExtra_enlarges_probeAlgebra :
    Fintype.card
        (PhysicalQuotient
          observableExtraProbeFamily3) = 6 :=
  observableExtraQuotient_card_eq_six

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

What this page does not claim

No actual production system is proven to exhaust the recognition classes. The right system's failure to exhaust does not mean it reads the wrong responses. The split does not establish that any physical system realizes 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: