Encyclopedia Foundation Foundation Pair Kernel Response Quotient Carrier S22 Hidden Extra Carrier Not Re

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Response Quotient Carrier S22 Hidden Extra Carrier Not Re

A machine-checked theorem proves that adding a hidden state to a physical system changes its identity, even when no existing probe can detect the addition.

Verify this page

The extra carrier

In the Recognition Science framework, a physical system is described by the responses it can give to a fixed set of probes. Two responses are equivalent when every probe agrees on them, and the quotient of all responses by that equivalence is the system's canonical carrier of information. The framework's library proves that this quotient is complete: it realizes every forced response and separates every distinct response.

The declaration hiddenExtraCarrier_not_responseQuotientIdentified establishes a sharp boundary around that construction. It proves, as a theorem, that a carrier built by adding a hidden state to the system is not identical to the canonical response quotient. The hidden state is one that no probe in the original family can detect, a ghost state that reads as zero on every coordinate probe. Yet the theorem shows that the enlarged carrier, with that ghost state included, is a different object from the quotient. The proof runs through a failure of injectivity: the map from the extra carrier to the response quotient is not injective, because the ghost state and the zero response collapse to the same quotient class.

The theorem does not claim that the hidden state is physically real. It does not assert that the enlarged carrier is the correct description of any actual system. It establishes only a structural fact about the framework's own construction: adding a state that no probe detects still changes the carrier's identity, because the carrier is defined by its responses to probes, and the hidden state is a distinct response that the original probes cannot see. The framework's library also proves the complementary positive case: a state detected by a new probe enlarges the quotient, and the enlarged quotient then has six elements rather than five.

What the theorem does not claim is that any physical production carrier, supplied independently of the framework, is identical to the response quotient. That final identification is stated explicitly as a separate property, and the library proves it is equivalent to a completeness condition on the production carrier. The library does not prove that any particular production carrier satisfies that condition. That remains a physical hypothesis, not a theorem.

THEOREM hiddenExtraCarrier_not_responseQuotientIdentified · IndisputableMonolith/Foundation/PairKernelResponseQuotientCarrierS22.lean
hiddenExtraCarrier_not_responseQuotientIdentified · IndisputableMonolith/Foundation/PairKernelResponseQuotientCarrierS22.lean:904 
theorem hiddenExtraCarrier_not_responseQuotientIdentified :
    ¬ ProductionCarrierIsResponseQuotient3
      (extraPhysicalChannelCarrier3 3) := by
  intro hidentified
  obtain ⟨pair, hpair⟩ :=
    realizedPrimitivePostingPair3_exists
  let event : RealizedPostingEvent3 3 :=
    ⟨pair, hpair⟩
  have hcomplete :=
    (productionCarrierIsResponseQuotient_iff_complete
      (extraPhysicalChannelCarrier3 3)).1
      hidentified
  exact
    extraCarrierToResponseQuotient_not_injective
      event
      (externalCarrierToResponseQuotient3_injective_of_classifier
        (hcomplete event).1)
THEOREM hiddenExtraCarrier_not_responseQuotientIdentified · IndisputableMonolith/Foundation/PairKernelResponseQuotientCarrierS22.lean
hiddenExtraCarrier_not_responseQuotientIdentified · IndisputableMonolith/Foundation/PairKernelResponseQuotientCarrierS22.lean:904 
theorem hiddenExtraCarrier_not_responseQuotientIdentified :
    ¬ ProductionCarrierIsResponseQuotient3
      (extraPhysicalChannelCarrier3 3) := by
  intro hidentified
  obtain ⟨pair, hpair⟩ :=
    realizedPrimitivePostingPair3_exists
  let event : RealizedPostingEvent3 3 :=
    ⟨pair, hpair⟩
  have hcomplete :=
    (productionCarrierIsResponseQuotient_iff_complete
      (extraPhysicalChannelCarrier3 3)).1
      hidentified
  exact
    extraCarrierToResponseQuotient_not_injective
      event
      (externalCarrierToResponseQuotient3_injective_of_classifier
        (hcomplete event).1)
THEOREM extraCarrierToResponseQuotient_not_injective · IndisputableMonolith/Foundation/PairKernelResponseQuotientCarrierS22.lean
extraCarrierToResponseQuotient_not_injective · IndisputableMonolith/Foundation/PairKernelResponseQuotientCarrierS22.lean:778 
/-- Explicit collision: the extra carrier map sends two distinct external
points to the same successor response class. -/
theorem extraCarrierToResponseQuotient_not_injective
    (event : RealizedPostingEvent3 3) :
    ¬ Function.Injective
      (externalCarrierToResponseQuotient3
        (extraPhysicalChannelCarrier3 3)
        event) := by
  intro hinjective
  have hclasses :
      externalCarrierToResponseQuotient3
          (extraPhysicalChannelCarrier3 3) event
          (Sum.inr (0 : Fin 3)) =
        externalCarrierToResponseQuotient3
          (extraPhysicalChannelCarrier3 3) event
          (Sum.inr (2 : Fin 3)) := by
    rfl
  have hpoints := hinjective hclasses
  have hfin : (0 : Fin 3) = 2 :=
    Sum.inr.inj hpoints
  have hnat : (0 : ℕ) = 2 :=
    congrArg Fin.val hfin
  omega
THEOREM productionCarrierIsResponseQuotient_iff_complete · IndisputableMonolith/Foundation/PairKernelResponseQuotientCarrierS22.lean
productionCarrierIsResponseQuotient_iff_complete · IndisputableMonolith/Foundation/PairKernelResponseQuotientCarrierS22.lean:830 
/-- The final production identification is exactly carrier completeness. This
records the remaining physical boundary rather than renaming it. -/
theorem productionCarrierIsResponseQuotient_iff_complete
    {N : ℕ} [NeZero N]
    (physical : PostingPhysicalChannelCarrier3 N) :
    ProductionCarrierIsResponseQuotient3 physical ↔
      PostingCarrierCoherenceComplete3 physical := by
  constructor
  · intro hidentified event
    obtain ⟨identification, hcommutes⟩ :=
      hidentified event
    have hquotient :=
      classifyResponseQuotient3_bijective event
    constructor
    · intro left right hclassify
      apply identification.injective
      apply hquotient.1
      rw [hcommutes left, hcommutes right,
        hclassify]
    · intro parent
      obtain ⟨responseClass, hresponseClass⟩ :=
        hquotient.2 parent
      refine
        ⟨identification.symm responseClass, ?_⟩
      have hcommute :=
        hcommutes
          (identification.symm responseClass)
      rw [identification.apply_symm_apply]
        at hcommute
      exact hcommute.symm.trans hresponseClass
  · intro hcomplete event
    let physicalEquiv :
        physical.Carrier event ≃
          PostingConfigurationDegreeCarrier3
            (realizedPostingEventConfiguration3 event) :=
      Equiv.ofBijective
        (physical.classify event)
        (hcomplete event)
    let quotientEquiv :
        RecognitionResponseQuotient3 ≃
          PostingConfigurationDegreeCarrier3
            (realizedPostingEventConfiguration3 event) :=
      Equiv.ofBijective
        (classifyResponseQuotient3 event)
        (classifyResponseQuotient3_bijective event)
    let identification :=
      physicalEquiv.trans quotientEquiv.symm
    refine ⟨identification, ?_⟩
    intro channel
    change
      quotientEquiv
          (quotientEquiv.symm
            (physical.classify event channel)) =
        physical.classify event channel
    exact quotientEquiv.apply_symm_apply _

What this page does not claim

The hidden state is physically real or observable. Any independently supplied production carrier is identical to the response quotient. The extra carrier is the correct description of any actual physical system.

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/PairKernelResponseQuotientCarrierS22.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