Foundation Recognition Signature Gauge First Bit Scalar Cost Not Complete

The one-bit boundary

A state space is a collection of possible conditions a system can be in. A recognition event, a discrete act of distinguishing one condition from another, assigns a value to each state. The question is how much information one such value carries. The answer, proved in the machine-checked library of formal theorems, is that a single scalar value can be a poor summary: two genuinely different states may receive the same number.

The proof uses the simplest possible example. Consider states that are pairs of bits, four possibilities: (false, false), (false, true), (true, false), (true, true). Let the scalar cost be the first bit alone, reading false as 0 and true as 1. The states (false, false) and (false, true) are different, yet both yield cost 0. The theorem first_bit_scalar_cost_not_complete records exactly this: there exist two distinct states with equal scalar cost.

The contrast is sharp. The full recognition signature, the pattern of values assigned by a family of observables, does separate these states. The family that reads both bits distinguishes all four possibilities, and its projection is injective. A single coordinate is not complete; the pair is. This is the one-bit boundary: one Boolean coordinate cannot encode an arbitrary state space, while a separating family of coordinates can.

In Recognition Science, this boundary is load-bearing. Physical identification is equality of the full recognition signature, not equality of any single scalar. A scalar cost is a complete gauge invariant only under a separate completeness hypothesis, never by default. The theorem does not claim that scalar costs are useless; it claims they are incomplete without the full signature. The consequence is that any theory built on a single cost value must justify that the value carries the whole state, and the default is that it does not.

/-- Scalar cost equality alone is not a complete physical quotient unless a
separate completeness theorem is supplied. -/
theorem first_bit_scalar_cost_not_complete :
    ∃ x y : PairBoolState, x ≠ y ∧ firstBitScalarCost x = firstBitScalarCost y := by
  refine ⟨(false, false), (false, true), ?_, ?_⟩
  · decide
  · 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

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

The theorem does not claim that scalar costs are never useful, only that they are not complete by default. The theorem does not claim that one Boolean coordinate is always insufficient; it shows a specific counterexample. The theorem does not claim that the full recognition signature always exists or is always finite.

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: