Foundation Recognition Signature Gauge

The signature gauge

A gauge is a way of deciding when two things are the same for all practical purposes. In physics and mathematics, a gauge choice identifies configurations that differ only in some redundancy, like choosing a coordinate system or a phase. The foundation recognition signature gauge is the framework's answer to a precise question: when do two states of a system count as physically identical? The answer, proved in the framework's machine-checked library of formal theorems, is that two states are identical exactly when every admitted observable returns the same value on both. That full collection of readings is the recognition signature, and equality of signatures is the gauge.

The central result is a quotient theorem: the map that sends each state to its signature is exact, meaning two states land on the same signature point if and only if they are indistinguishable by the observables. Every admitted observable descends cleanly to the quotient, and if the family of observables is rich enough to separate states, the signature map is injective: distinct states get distinct signatures. This is the formal backbone that lets the framework treat physical identification as equality of full signatures rather than equality of some cheaper summary.

The framework also draws a sharp boundary against a tempting shortcut. A scalar cost, a single number assigned to each state, is not by default a complete gauge. The framework proves that a one-bit Boolean coordinate, a single yes/no observation, cannot separate the four states of a two-bit system: the states (false, false) and (false, true) share the same first bit and hence the same one-bit signature. The same failure applies to a scalar cost that reads only that first bit. Only under a separate completeness hypothesis does scalar-cost equality coincide with signature equality. Two Boolean coordinates, by contrast, do separate all four states, and the framework proves the two-bit signature map is injective.

In Recognition Science, this framework is the correction to a naive reading of its own primitive: a single recognition event is an atomic floor, but it is not a complete encoding of a state space. The complete observable object is the family of recognizers and its full signature. The framework records this as a formal boundary: one Boolean shadow is incomplete, two are separating, and the full signature quotient is exact. The practical consequence is that any claim that a single cost or a single bit captures physical identity carries a burden of proof, and the framework now has a named theorem for exactly when that burden is met.

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

/-- Every admitted recognition coordinate descends to the signature quotient, so
the quotient loses no observable information from that family. -/
theorem signature_observable_descends (F : Set (X → C)) (f : X → C) (hf : f ∈ F) :
    ∃ g : PhysicalQuotient F → C, ∀ x, g (proj F x) = f x :=
  observable_descends F f hf

/-- If the full recognition signature separates states, the quotient projection
is injective.  This is the precise "complete recognizer family" condition. -/
theorem signature_projection_injective_of_separating (F : Set (X → C))
    (hsep : ∀ x y, SameRecognitionSignature F x y → x = y) :
    Function.Injective (proj F) :=
  proj_injective_of_separating F hsep

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

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

What this page does not claim

This framework does not derive the cost function J or any of the forcing chain theorems. It does not claim that a single scalar cost is ever complete without a separate hypothesis. It does not specify which observables any particular physical system admits.

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: