IndisputableMonolith.Foundation.RecognitionSignatureGauge

   1import Mathlib
   2import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientSelection
   3
   4/-!
   5# Recognition signatures, gauge quotients, and the one-bit T0 boundary
   6
   7This module records the Lean-level correction prompted by the T-1/T0 Boolean
   8shadow audit (June 2026).
   9
  10A single Boolean distinction is an atomic recognition floor.  It is not a
  11complete encoding of an arbitrary state space.  The complete observable object,
  12when it exists, is a family of recognizers/observables and its full signature.
  13
  14We connect that statement to the existing quotient theorem in
  15`PrimitiveRecognitionCalculus.QuotientSelection`:
  16
  17* physical identification is equality of the full recognition signature;
  18* every admitted observable descends to the quotient;
  19* a separating family gives an injective projection;
  20* scalar-cost equality is only a complete gauge invariant under a separate
  21  completeness hypothesis, not by default;
  22* one Boolean coordinate is not complete in general (`Bool × Bool`), while the
  23  two coordinate recognizers do separate.
  24
  25Status: 0 sorry, 0 project axiom.
  26-/
  27
  28namespace IndisputableMonolith
  29namespace Foundation
  30namespace RecognitionSignatureGauge
  31
  32open PrimitiveRecognitionCalculus.QuotientSelection
  33
  34variable {X C : Type*}
  35
  36/-! ## Full recognition signatures -/
  37
  38/-- Equality of the full recognition signature induced by a family of
  39observables.  This is just observational equivalence under all admitted
  40observables, named in the T0 language. -/
  41def SameRecognitionSignature (F : Set (X → C)) (x y : X) : Prop :=
  42  ObsEquiv F x y
  43
  44/-- The physical quotient induced by a family of recognizers is exactly equality
  45of the full recognition signature. -/
  46theorem signature_forced_quotient_iff (F : Set (X → C)) (x y : X) :
  47    proj F x = proj F y ↔ SameRecognitionSignature F x y :=
  48  forced_iff F x y
  49
  50/-- Every admitted recognition coordinate descends to the signature quotient, so
  51the quotient loses no observable information from that family. -/
  52theorem signature_observable_descends (F : Set (X → C)) (f : X → C) (hf : f ∈ F) :
  53    ∃ g : PhysicalQuotient F → C, ∀ x, g (proj F x) = f x :=
  54  observable_descends F f hf
  55
  56/-- If the full recognition signature separates states, the quotient projection
  57is injective.  This is the precise "complete recognizer family" condition. -/
  58theorem signature_projection_injective_of_separating (F : Set (X → C))
  59    (hsep : ∀ x y, SameRecognitionSignature F x y → x = y) :
  60    Function.Injective (proj F) :=
  61  proj_injective_of_separating F hsep
  62
  63/-- Certificate for the correct gauge story: gauge equivalence is equality of
  64the full admitted recognition signature, not equality under a single Boolean
  65coordinate. -/
  66structure RecognitionSignatureGaugeCertificate (F : Set (X → C)) : Prop where
  67  quotient_exact :
  68    ∀ x y : X, proj F x = proj F y ↔ SameRecognitionSignature F x y
  69  observables_descend :
  70    ∀ f ∈ F, ∃ g : PhysicalQuotient F → C, ∀ x, g (proj F x) = f x
  71  separating_family_injective :
  72    (∀ x y, SameRecognitionSignature F x y → x = y) → Function.Injective (proj F)
  73
  74/-- The full-signature gauge certificate is exactly the existing quotient
  75selection theorem, re-expressed for T0-family language. -/
  76theorem recognitionSignatureGaugeCertificate_holds (F : Set (X → C)) :
  77    RecognitionSignatureGaugeCertificate F where
  78  quotient_exact := signature_forced_quotient_iff F
  79  observables_descend := signature_observable_descends F
  80  separating_family_injective := signature_projection_injective_of_separating F
  81
  82/-! ## Scalar cost is not automatically a complete invariant -/
  83
  84/-- A scalar cost is complete for a recognition family only if equality of the
  85scalar is equivalent to equality of the full recognition signature.  This is a
  86separate hypothesis, not a consequence of having a scalar cost. -/
  87def ScalarCostCompleteFor (F : Set (X → C)) (cost : X → ℝ) : Prop :=
  88  ∀ x y : X, cost x = cost y ↔ SameRecognitionSignature F x y
  89
  90/-- Under the explicit completeness hypothesis, the scalar-cost kernel matches
  91the full recognition-signature equivalence.  Without this hypothesis, scalar
  92cost equality is only a cost observable. -/
  93theorem scalar_cost_kernel_eq_signature_of_complete
  94    (F : Set (X → C)) (cost : X → ℝ) (hcomplete : ScalarCostCompleteFor F cost)
  95    (x y : X) :
  96    cost x = cost y ↔ SameRecognitionSignature F x y :=
  97  hcomplete x y
  98
  99/-! ## One Boolean coordinate is not complete in general -/
 100
 101/-- A toy two-bit state space for the "one Boolean cannot encode everything"
 102counterexample. -/
 103abbrev PairBoolState := Bool × Bool
 104
 105/-- First coordinate recognizer. -/
 106def firstBit : PairBoolState → Bool := fun x => x.1
 107
 108/-- Second coordinate recognizer. -/
 109def secondBit : PairBoolState → Bool := fun x => x.2
 110
 111/-- The one-coordinate Boolean family. -/
 112def firstBitFamily : Set (PairBoolState → Bool) := {f | f = firstBit}
 113
 114/-- The two-coordinate Boolean family. -/
 115def pairBitFamily : Set (PairBoolState → Bool) :=
 116  {f | f = firstBit ∨ f = secondBit}
 117
 118/-- One Boolean coordinate fails to separate the two states with the same first
 119bit and different second bit. -/
 120theorem one_boolean_coordinate_not_complete :
 121    ∃ x y : PairBoolState,
 122      x ≠ y ∧ SameRecognitionSignature firstBitFamily x y := by
 123  refine ⟨(false, false), (false, true), ?_, ?_⟩
 124  · decide
 125  · intro f hf
 126    have hf' : f = firstBit := hf
 127    rw [hf']
 128    rfl
 129
 130/-- The first-bit scalar cost has the same incompleteness: it agrees on two
 131distinct states. -/
 132def firstBitScalarCost : PairBoolState → ℝ :=
 133  fun x => if x.1 then 1 else 0
 134
 135/-- Scalar cost equality alone is not a complete physical quotient unless a
 136separate completeness theorem is supplied. -/
 137theorem first_bit_scalar_cost_not_complete :
 138    ∃ x y : PairBoolState, x ≠ y ∧ firstBitScalarCost x = firstBitScalarCost y := by
 139  refine ⟨(false, false), (false, true), ?_, ?_⟩
 140  · decide
 141  · rfl
 142
 143/-- The two coordinate Boolean recognizers separate all states of `Bool × Bool`. -/
 144theorem pairBitFamily_separating :
 145    ∀ x y : PairBoolState, SameRecognitionSignature pairBitFamily x y → x = y := by
 146  intro x y hsig
 147  cases x with
 148  | mk x₁ x₂ =>
 149    cases y with
 150    | mk y₁ y₂ =>
 151      have h₁ : x₁ = y₁ := by
 152        exact hsig firstBit (Or.inl rfl)
 153      have h₂ : x₂ = y₂ := by
 154        exact hsig secondBit (Or.inr rfl)
 155      cases h₁
 156      cases h₂
 157      rfl
 158
 159/-- Therefore the physical quotient by the two-coordinate family is injective:
 160two Boolean recognizers recover the whole two-bit toy state. -/
 161theorem pairBitFamily_projection_injective :
 162    Function.Injective (proj pairBitFamily) :=
 163  signature_projection_injective_of_separating pairBitFamily pairBitFamily_separating
 164
 165/-- Compact audit certificate for the T0 Boolean-shadow correction. -/
 166structure BooleanShadowCompletenessBoundary : Prop where
 167  /-- One Boolean coordinate is not complete in general. -/
 168  one_bit_not_complete :
 169    ∃ x y : PairBoolState,
 170      x ≠ y ∧ SameRecognitionSignature firstBitFamily x y
 171  /-- Scalar cost equality is not complete in general. -/
 172  scalar_cost_not_complete :
 173    ∃ x y : PairBoolState, x ≠ y ∧ firstBitScalarCost x = firstBitScalarCost y
 174  /-- A separating family gives an injective quotient projection. -/
 175  two_bit_signature_injective :
 176    Function.Injective (proj pairBitFamily)
 177  /-- Full-signature gauge equivalence is the theorem-grade quotient statement. -/
 178  full_signature_quotient_exact :
 179    ∀ {X C : Type*} (F : Set (X → C)) (x y : X),
 180      proj F x = proj F y ↔ SameRecognitionSignature F x y
 181
 182/-- The corrected T0 boundary is machine-checkable: one bit is atomic, not
 183complete; a full signature quotient is theorem-grade; scalar cost completeness
 184requires an extra completeness hypothesis. -/
 185theorem booleanShadowCompletenessBoundary_holds :
 186    BooleanShadowCompletenessBoundary where
 187  one_bit_not_complete := one_boolean_coordinate_not_complete
 188  scalar_cost_not_complete := first_bit_scalar_cost_not_complete
 189  two_bit_signature_injective := pairBitFamily_projection_injective
 190  full_signature_quotient_exact := fun F x y => signature_forced_quotient_iff F x y
 191
 192end RecognitionSignatureGauge
 193end Foundation
 194end IndisputableMonolith
 195