Foundation Recognition Signature Gauge One Boolean Coordinate Not Complete

The one-bit boundary

A Boolean coordinate is a single true-or-false observation, like a switch that records only one bit of information. The theorem one_boolean_coordinate_not_complete proves that such a lone bit is not a complete description of a state space with more than two possible states. Concretely, consider a system with two switches, so four possible states: both off, first on, second on, both on. If you only look at the first switch, the states (off, off) and (off, on) look identical, even though they are genuinely different. The proof exhibits exactly this pair and shows they share the same recognition signature under the family that only reads the first bit.

This result lives inside the framework's account of how physical objects are identified. In Recognition Science, the recognition signature of a state is the complete list of answers given by every observable in a chosen family. The framework's library proves that two states are physically the same exactly when their full signatures agree, and that any observable can be evaluated on the resulting quotient of states. A single Boolean coordinate fails this test: it cannot separate states that differ only in the second bit. The theorem is the boundary marker for how much observational data is needed before a description becomes complete.

The companion theorem shows what completeness does require. The family that reads both switches, first and second, is separating: if two states have the same answers for both bits, they are the same state. Its projection onto the quotient is injective, meaning no information is lost. The contrast is sharp: one bit collapses distinct states together, two bits do not. The framework's library records this as the Boolean shadow completeness boundary, a formal certificate that the one-bit case is the minimal failure and the two-bit case is the minimal success.

What the theorem does not claim is equally important. It does not say that a single Boolean coordinate is useless, only that it is incomplete for distinguishing all states. It does not claim that scalar cost, a single number assigned to a state, is always a complete invariant; that holds only under an extra completeness hypothesis. And it does not assert that any particular physical system is described by two Boolean coordinates. The theorem is a structural fact about information, not a claim about which observables nature actually provides.

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

/-- The physical quotient induced by a family of recognizers is exactly equality
of the full recognition signature. -/
theorem signature_forced_quotient_iff (F : Set (X → C)) (x y : X) :
    proj F x = proj F y ↔ SameRecognitionSignature F x y :=
  forced_iff F x y

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

What this page does not claim

A single Boolean coordinate is useless, only that it is incomplete for distinguishing all states. Scalar cost is always a complete invariant without an extra completeness hypothesis. Any particular physical system is described by two Boolean coordinates.

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: