IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison

   1/-
   2  PrimitiveRecognitionCalculus/ValidComparison.lean
   3
   4  Native object -> display object -> observable protocol.
   5
   6  This module turns the paper doctrine into a reusable formal object. A display
   7  map is not enough to justify comparison. A valid comparison also needs an
   8  observable protocol and a bridge showing the displayed value agrees with the
   9  observable datum.
  10
  11  No project-local axioms. No sorry.
  12-/
  13
  14import Mathlib
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace PrimitiveRecognitionCalculus
  19namespace ValidComparison
  20
  21/-- A bridge from a native object `N` to a display object `D` and an observable
  22object `O`. The commuting law says the display, when observed, agrees with the
  23native observable protocol. -/
  24structure Bridge (N D O : Type*) where
  25  display : N → D
  26  observeNative : N → O
  27  observeDisplay : D → O
  28  commutes : ∀ n : N, observeDisplay (display n) = observeNative n
  29
  30/-- A display comparison is valid when both displayed values come from native
  31objects through the same bridge and the displayed observations agree. -/
  32def IsValidComparison {N D O : Type*} (B : Bridge N D O) (x y : N) : Prop :=
  33  B.observeDisplay (B.display x) = B.observeDisplay (B.display y)
  34
  35theorem validComparison_iff_native {N D O : Type*} (B : Bridge N D O) (x y : N) :
  36    IsValidComparison B x y ↔ B.observeNative x = B.observeNative y := by
  37  unfold IsValidComparison
  38  rw [B.commutes x, B.commutes y]
  39
  40/-- Bridge composition: if a native-to-display bridge and a display-to-display
  41bridge both commute with the observable protocol, the composite bridge is valid. -/
  42def compose {N D E O : Type*} (B₁ : Bridge N D O) (B₂ : Bridge D E O) : Bridge N E O where
  43  display := B₂.display ∘ B₁.display
  44  observeNative := B₂.observeNative ∘ B₁.display
  45  observeDisplay := B₂.observeDisplay
  46  commutes := by
  47    intro n
  48    exact B₂.commutes (B₁.display n)
  49
  50theorem validComparison_compose {N D E O : Type*}
  51    (B₁ : Bridge N D O) (B₂ : Bridge D E O) (x y : N) :
  52    IsValidComparison (compose B₁ B₂) x y ↔ B₂.observeNative (B₁.display x) = B₂.observeNative (B₁.display y) :=
  53  validComparison_iff_native (compose B₁ B₂) x y
  54
  55/-- **Valid comparison doctrine.** A comparison in a display carrier is legitimate
  56exactly when it descends to equality of the native observable protocol, and this
  57legitimacy is stable under composition of display bridges. -/
  58theorem valid_comparison_doctrine {N D E O : Type*}
  59    (B₁ : Bridge N D O) (B₂ : Bridge D E O) :
  60    (∀ x y : N, IsValidComparison B₁ x y ↔ B₁.observeNative x = B₁.observeNative y)
  61      ∧ (∀ x y : N, IsValidComparison (compose B₁ B₂) x y
  62          ↔ B₂.observeNative (B₁.display x) = B₂.observeNative (B₁.display y)) :=
  63  ⟨validComparison_iff_native B₁, validComparison_compose B₁ B₂⟩
  64
  65end ValidComparison
  66end PrimitiveRecognitionCalculus
  67end Foundation
  68end IndisputableMonolith
  69