Foundation Pair Kernel Scale Covariant Observables S20 Response Distinguishabili

Distinguishable channels

A physical system that records events must answer each one. The question is what its answers can reveal. In the Recognition Science framework, a system's responses are called recognition events: discrete postings in a ledger that track what happened. The declaration responseDistinguishability_implies_parentInjective states a precise consequence: if a system's responses to every possible event are all distinct, then the mapping from parent configurations to responses is injective. In plain language, distinguishable responses mean no two different underlying configurations produce the same answer.

The theorem is proved in the framework's machine-checked library of formal theorems, in the module PairKernelScaleCovariantObservablesS20. It builds on the definition of channel distinguishability, which requires that for every event, the system's response function is injective. The result then shows this injectivity carries upward: the parent configuration, the full set of spatial and temporal tags attached to an event, is also recoverable from the response. This is a structural fact about how information flows from configurations to responses.

The theorem does not claim that any particular physical system actually has distinguishable responses. That is a separate hypothesis, named PostingCarrierResponseObservability3, which combines distinguishability with the realization of every theorem-backed parent response. The library is explicit about this boundary: the parent-response catalog is a theorem, but its physical realization and channel distinguishability remain an exact hypothesis boundary. No absolute SI unit, hydrogen datum, or exact-J field unit is selected by this result.

The practical meaning is that if a system passes the distinguishability test, its responses carry complete information about the parent configurations. This supports the framework's operational account of physical carrier completeness: completeness follows from distinguishable channel responses together with realization of every parent response. The theorem is one link in that chain, not the whole chain.

theorem parentTagResponse3_injective
    {N : ℕ} [NeZero N]
    {event : RealizedPostingEvent3 N} :
    Function.Injective
      (@parentTagResponse3 N _ event) := by
  intro left right h
  cases left with
  | inl leftAxis =>
      cases right with
      | inl rightAxis =>
          simp [parentTagResponse3] at h
          exact congrArg Sum.inl h
      | inr rightKind =>
          simp [parentTagResponse3] at h
  | inr leftKind =>
      cases right with
      | inl rightAxis =>
          simp [parentTagResponse3] at h
      | inr rightKind =>
          simp [parentTagResponse3] at h
          exact congrArg Sum.inr h

theorem parentTagResponse3_injective
    {N : ℕ} [NeZero N]
    {event : RealizedPostingEvent3 N} :
    Function.Injective
      (@parentTagResponse3 N _ event) := by
  intro left right h
  cases left with
  | inl leftAxis =>
      cases right with
      | inl rightAxis =>
          simp [parentTagResponse3] at h
          exact congrArg Sum.inl h
      | inr rightKind =>
          simp [parentTagResponse3] at h
  | inr leftKind =>
      cases right with
      | inl rightAxis =>
          simp [parentTagResponse3] at h
      | inr rightKind =>
          simp [parentTagResponse3] at h
          exact congrArg Sum.inr h

What this page does not claim

The theorem does not claim any particular physical system has distinguishable responses. The theorem does not select any absolute SI unit, hydrogen datum, or exact-J field unit.

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