IndisputableMonolith.Foundation.RecognizerInducesLogic

   1import Mathlib
   2import IndisputableMonolith.Foundation.PrimitiveDistinction
   3import IndisputableMonolith.Foundation.MagnitudeOfMismatch
   4import IndisputableMonolith.Foundation.ObserverFromRecognition
   5
   6/-!
   7# Recognizers Induce a Law-of-Logic Realization
   8
   9This module unifies Recognition Geometry with the Law of Logic. The
  10companion paper `RS_Recognition_Geometry_Logic_Unification.tex` argues
  11that any recognizer `r : 𝒞 → ℰ` mapping configurations to events
  12automatically generates a Law-of-Logic realization on its event space
  13`ℰ`. We formalise the honest version of that claim:
  14
  15* A recognizer automatically supplies the **three definitional**
  16  Aristotelian conditions on its event space:
  17    (L1) Identity, (L2) Non-Contradiction, (L3a) Totality.
  18  These are forced by the equality-induced cost on `ℰ` together with
  19  the type signature of the recognizer.
  20
  21* A recognizer automatically supplies a **primitive observer** in the
  22  sense of `ObserverFromRecognition`. The recognizer is the primitive
  23  observer.
  24
  25* (L4) Composition Consistency is **not** automatic. It requires extra
  26  compositional structure on the recognizer family, made explicit as the
  27  hypothesis `RecognizerComposition`.
  28
  29Putting these together: a recognizer alone produces three of the four
  30classical conditions for free (definitional from the type signature plus
  31equality), the primitive observer for free (canonical two-outcome
  32recognizer), and reduces the remaining substantive content of the
  33Aristotelian framework to a single named compositional axiom. This is the
  34single forcing chain promised by the companion paper.
  35
  36This module connects:
  37
  38* `PrimitiveDistinction.lean` (definitional facts from equality)
  39* `MagnitudeOfMismatch.lean` (single-valuedness forces symmetry)
  40* `ObserverFromRecognition.lean` (non-trivial recognition forces
  41  primitive observer)
  42
  43into one Lean-checked unification.
  44-/
  45
  46namespace IndisputableMonolith
  47namespace Foundation
  48namespace RecognizerInducesLogic
  49
  50open Classical
  51open PrimitiveDistinction
  52open MagnitudeOfMismatch
  53open ObserverFromRecognition
  54
  55/-! ## The Recognizer
  56
  57We use the Recognition Geometry presentation: a recognizer is a
  58surjection from a configuration space onto an event space.
  59-/
  60
  61/-- A **recognizer** in the Recognition Geometry sense: a surjection
  62from a configuration space `𝒞` onto an event space `ℰ`. The fact that
  63it is many-to-one is essential; it is what generates the
  64indistinguishability quotient. -/
  65structure Recognizer (𝒞 ℰ : Type*) where
  66  observe : 𝒞 → ℰ
  67  surjective : Function.Surjective observe
  68
  69/-! ## The Indistinguishability Quotient -/
  70
  71/-- Two configurations are observationally indistinguishable under a
  72recognizer if the recognizer maps them to the same event. -/
  73def Recognizer.kernel {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ) (x y : 𝒞) : Prop :=
  74  r.observe x = r.observe y
  75
  76/-- The kernel of a recognizer is an equivalence relation. -/
  77theorem Recognizer.kernel_is_equivalence {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ) :
  78    Equivalence (r.kernel) :=
  79  ⟨fun _ => rfl, fun h => h.symm, fun h₁ h₂ => h₁.trans h₂⟩
  80
  81/-! ## The Recognizer-Induced Cost on the Event Space -/
  82
  83/-- The cost of distinguishing two events: zero when they are the same
  84event, a positive weight otherwise. This is exactly the equality-induced
  85cost of `PrimitiveDistinction` applied to the event space `ℰ`. -/
  86noncomputable def Recognizer.cost {𝒞 ℰ : Type*} (_r : Recognizer 𝒞 ℰ)
  87    (weight : ℝ) : ℰ → ℰ → ℝ :=
  88  equalityCost ℰ weight
  89
  90/-! ## The Three Definitional Aristotelian Conditions
  91
  92A recognizer induces (L1), (L2), and (L3a) on its event space
  93automatically, by `PrimitiveDistinction`. No further structural choice
  94is required.
  95-/
  96
  97/-- **(L1) Identity from the recognizer.** The cost of distinguishing an
  98event from itself is zero. -/
  99theorem Recognizer.identity {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ)
 100    (weight : ℝ) :
 101    ∀ e : ℰ, r.cost weight e e = 0 := by
 102  intro e
 103  exact identity_from_equality ℰ weight e
 104
 105/-- **(L2) Non-Contradiction from the recognizer.** The cost of
 106distinguishing `e₁` from `e₂` equals the cost of distinguishing `e₂`
 107from `e₁`. -/
 108theorem Recognizer.non_contradiction {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ)
 109    (weight : ℝ) :
 110    ∀ e₁ e₂ : ℰ, r.cost weight e₁ e₂ = r.cost weight e₂ e₁ := by
 111  intro e₁ e₂
 112  exact non_contradiction_from_equality ℰ weight e₁ e₂
 113
 114/-- **(L3a) Totality from the recognizer.** The cost is defined and
 115returns a value for every pair of events. -/
 116theorem Recognizer.totality {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ)
 117    (weight : ℝ) :
 118    ∀ e₁ e₂ : ℰ, ∃ c : ℝ, r.cost weight e₁ e₂ = c := by
 119  intro e₁ e₂
 120  exact totality_from_function_type ℰ weight e₁ e₂
 121
 122/-- **Single-valuedness from the recognizer.** The induced cost is a
 123single-valued function on unordered pairs of events; equivalently, by
 124`MagnitudeOfMismatch`, it is symmetric. -/
 125theorem Recognizer.singleValued {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ)
 126    (weight : ℝ) :
 127    SingleValuedOnUnorderedPair (r.cost weight) :=
 128  equalityCost_singleValued ℰ weight
 129
 130/-! ## The Primitive Observer is the Recognizer
 131
 132Once the event space has at least two distinct events, the recognizer
 133delivers the primitive observer of `ObserverFromRecognition`. This is the
 134unification: the recognizer of Recognition Geometry **is** the primitive
 135observer of the Law-of-Logic chain. They are the same object.
 136-/
 137
 138/-- The event space of a recognizer admits non-trivial recognition iff
 139it contains at least two distinct events. -/
 140def Recognizer.hasNontrivialRecognition {𝒞 ℰ : Type*}
 141    (_r : Recognizer 𝒞 ℰ) : Prop :=
 142  ∃ e₁ e₂ : ℰ, e₁ ≠ e₂
 143
 144/-- **Recognizer is observer.** Any recognizer with a non-trivially
 145populated event space induces a primitive observer (a finite-valued
 146interface) that separates two distinct events.
 147
 148This is the unification: the geometric primitive (recognizer producing
 149event space) and the logical primitive (interface producing primitive
 150observer) are the same act. -/
 151theorem Recognizer.induces_primitive_observer {𝒞 ℰ : Type*}
 152    (r : Recognizer 𝒞 ℰ) (h : r.hasNontrivialRecognition) :
 153    ∃ (O : PrimitiveObserver ℰ) (e₁ e₂ : ℰ),
 154      e₁ ≠ e₂ ∧ Separates O e₁ e₂ := by
 155  rcases h with ⟨e₁, e₂, hne⟩
 156  refine ⟨pointInterface e₁, e₁, e₂, hne, ?_⟩
 157  exact pointInterface_separates hne
 158
 159/-! ## (L4) Composition Consistency: The Substantive Hypothesis
 160
 161Composition consistency is not automatic from the type signature. It
 162requires the recognizer family to compose lawfully: composing two
 163recognition events should yield a cost determined by the costs of the
 164components. We make this an explicit hypothesis package; it is what the
 165companion paper acknowledges as the genuinely structural part of the
 166Aristotelian framework.
 167-/
 168
 169/-- **(L4) Composition consistency on the event space.** The cost of a
 170composed comparison is determined by the costs of its components.
 171
 172The exact algebraic form depends on the carrier; for the continuous
 173positive-ratio realization it is `F(xy) + F(x/y) = P(F(x), F(y))`. We
 174state the abstract version: there exists a combiner `Φ` on the cost
 175space realizing this functional dependence. -/
 176def Recognizer.RecognizerComposition {𝒞 ℰ : Type*}
 177    (r : Recognizer 𝒞 ℰ) (weight : ℝ)
 178    (compose : ℰ → ℰ → ℰ) (revcompose : ℰ → ℰ → ℰ) : Prop :=
 179  ∃ Φ : ℝ → ℝ → ℝ,
 180    ∀ e₁ e₂ : ℰ,
 181      r.cost weight (compose e₁ e₂) e₁ + r.cost weight (revcompose e₁ e₂) e₁ =
 182        Φ (r.cost weight e₁ e₁) (r.cost weight e₂ e₂)
 183
 184/-! ## The Unification Theorem
 185
 186The single forcing chain claim of the companion paper, in its honest
 187Lean form: a recognizer plus a compositional structure delivers all four
 188classical Aristotelian conditions on its event space.
 189-/
 190
 191/-- **The Unification Theorem.**
 192
 193A recognizer automatically supplies the three definitional Aristotelian
 194conditions (Identity, Non-Contradiction, Totality) on its event space,
 195plus the primitive observer (the recognizer itself), provided the event
 196space is non-trivially populated.
 197
 198The fourth condition (Composition Consistency) is not automatic; it
 199requires the explicit `RecognizerComposition` hypothesis on a chosen
 200composition law for the event space. When that hypothesis is supplied,
 201the recognizer's event space is a full Law-of-Logic carrier in the sense
 202of the rigidity paper. -/
 203theorem unification {𝒞 ℰ : Type*}
 204    (r : Recognizer 𝒞 ℰ) (weight : ℝ)
 205    (h : r.hasNontrivialRecognition) :
 206    -- Three definitional Aristotelian conditions:
 207    (∀ e : ℰ, r.cost weight e e = 0) ∧
 208    (∀ e₁ e₂ : ℰ, r.cost weight e₁ e₂ = r.cost weight e₂ e₁) ∧
 209    (∀ e₁ e₂ : ℰ, ∃ c : ℝ, r.cost weight e₁ e₂ = c) ∧
 210    -- Single-valuedness on unordered pairs (≡ Non-Contradiction):
 211    SingleValuedOnUnorderedPair (r.cost weight) ∧
 212    -- Primitive observer:
 213    (∃ (O : PrimitiveObserver ℰ) (e₁ e₂ : ℰ),
 214      e₁ ≠ e₂ ∧ Separates O e₁ e₂) := by
 215  refine ⟨?_, ?_, ?_, ?_, ?_⟩
 216  · exact Recognizer.identity r weight
 217  · exact Recognizer.non_contradiction r weight
 218  · exact Recognizer.totality r weight
 219  · exact Recognizer.singleValued r weight
 220  · exact Recognizer.induces_primitive_observer r h
 221
 222/-! ## Headline Certificate -/
 223
 224/-- **Recognizer-Induces-Logic Certificate.**
 225
 226The single forcing chain from Recognition Geometry to the Law of Logic
 227in its current form: the three definitional Aristotelian conditions are
 228automatic, the primitive observer is automatic, and the substantive
 229content reduces to a named compositional hypothesis. -/
 230structure RecognizerInducesLogicCert where
 231  identity_auto :
 232    ∀ {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ) (weight : ℝ),
 233      ∀ e : ℰ, r.cost weight e e = 0
 234  non_contradiction_auto :
 235    ∀ {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ) (weight : ℝ),
 236      ∀ e₁ e₂ : ℰ, r.cost weight e₁ e₂ = r.cost weight e₂ e₁
 237  totality_auto :
 238    ∀ {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ) (weight : ℝ),
 239      ∀ e₁ e₂ : ℰ, ∃ c : ℝ, r.cost weight e₁ e₂ = c
 240  primitive_observer_auto :
 241    ∀ {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ),
 242      r.hasNontrivialRecognition →
 243        ∃ (O : PrimitiveObserver ℰ) (e₁ e₂ : ℰ),
 244          e₁ ≠ e₂ ∧ Separates O e₁ e₂
 245
 246def recognizerInducesLogicCert : RecognizerInducesLogicCert where
 247  identity_auto := fun r w => Recognizer.identity r w
 248  non_contradiction_auto := fun r w => Recognizer.non_contradiction r w
 249  totality_auto := fun r w => Recognizer.totality r w
 250  primitive_observer_auto := fun r h => Recognizer.induces_primitive_observer r h
 251
 252theorem recognizerInducesLogicCert_inhabited :
 253    Nonempty RecognizerInducesLogicCert :=
 254  ⟨recognizerInducesLogicCert⟩
 255
 256end RecognizerInducesLogic
 257end Foundation
 258end IndisputableMonolith
 259