Foundation Recognition Signature Gauge Pair Bit Family Projection Injective

The two-bit separation

A Boolean distinction is a yes-or-no answer to a single question. A state of the world can be probed by many such questions, and the full set of answers is called its recognition signature. The Recognition Science framework models physical identification as equality of these signatures: two states are the same physical state exactly when every admitted observable answers identically on both. The machine-checked library of formal theorems proves this quotient structure in full generality, including that every admitted observable descends to the quotient and that a separating family of observables yields an injective projection.

The theorem in question, pairBitFamily_projection_injective, applies that general machinery to the simplest nontrivial case: a state space with exactly two Boolean coordinates, so four possible states. The family of observables it considers is the pair of coordinate projections, the two questions that read the first bit and the second bit. The theorem proves that this two-member family is separating: if two states agree on both coordinates, they are the same state. Consequently, the projection from the original four states onto the quotient of recognition signatures is injective: no two distinct states collapse into the same signature. In plain terms, two yes-or-no questions suffice to tell all four states apart.

The theorem's companion results make the boundary precise. One Boolean coordinate alone is not complete: the state (false, false) and the state (false, true) share the same first-bit answer, so a single coordinate cannot separate them. Likewise, scalar cost equality, a single real number attached to each state, is only a complete gauge invariant under a separate completeness hypothesis, not by default. The one-bit scalar cost that reads the first coordinate fails to distinguish the same pair. The two-coordinate family closes that gap, and the injective projection is the formal certificate that no information is lost when passing to the quotient.

What the theorem does not claim is just as important. It does not say that any arbitrary family of observables separates states; it says this particular two-coordinate family does. It does not assert that one Boolean coordinate is ever complete; the companion theorem one_boolean_coordinate_not_complete proves the opposite. And it does not claim that scalar cost equality is always a complete invariant; that holds only under the separate completeness hypothesis. The framework's library records the boundary explicitly: a single Boolean distinction is an atomic recognition floor, but it is not a complete encoding of an arbitrary state space. The full signature, not any single coordinate, is the complete observable object when it exists.

The consequence for the framework is that completeness is a property of families, not of individual observables. A reader who wants to know whether a set of measurements pins down the physical state must ask whether the family separates, not whether each member is individually informative. The two-bit example is the smallest case where the difference shows, and the theorem makes the difference exact.

/-- The two coordinate Boolean recognizers separate all states of `Bool × Bool`. -/
theorem pairBitFamily_separating :
    ∀ x y : PairBoolState, SameRecognitionSignature pairBitFamily x y → x = y := by
  intro x y hsig
  cases x with
  | mk x₁ x₂ =>
    cases y with
    | mk y₁ y₂ =>
      have h₁ : x₁ = y₁ := by
        exact hsig firstBit (Or.inl rfl)
      have h₂ : x₂ = y₂ := by
        exact hsig secondBit (Or.inr rfl)
      cases h₁
      cases h₂
      rfl

/-- Therefore the physical quotient by the two-coordinate family is injective:
two Boolean recognizers recover the whole two-bit toy state. -/
theorem pairBitFamily_projection_injective :
    Function.Injective (proj pairBitFamily) :=
  signature_projection_injective_of_separating pairBitFamily pairBitFamily_separating

/-- One Boolean coordinate fails to separate the two states with the same first
bit and different second bit. -/
theorem one_boolean_coordinate_not_complete :
    ∃ x y : PairBoolState,
      x ≠ y ∧ SameRecognitionSignature firstBitFamily x y := by
  refine ⟨(false, false), (false, true), ?_, ?_⟩
  · decide
  · intro f hf
    have hf' : f = firstBit := hf
    rw [hf']
    rfl

/-- Under the explicit completeness hypothesis, the scalar-cost kernel matches
the full recognition-signature equivalence.  Without this hypothesis, scalar
cost equality is only a cost observable. -/
theorem scalar_cost_kernel_eq_signature_of_complete
    (F : Set (X → C)) (cost : X → ℝ) (hcomplete : ScalarCostCompleteFor F cost)
    (x y : X) :
    cost x = cost y ↔ SameRecognitionSignature F x y :=
  hcomplete x y

What this page does not claim

This theorem does not claim that any arbitrary family of observables separates states. This theorem does not claim that one Boolean coordinate is ever complete. This theorem does not claim that scalar cost equality is always a complete invariant without a separate completeness hypothesis.

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