IndisputableMonolith.RRF.Core.Recognition

   1import IndisputableMonolith.Recognition
   2
   3/-!
   4# RRF Core: Recognition (Re-export)
   5
   6This module re-exports the existing Recognition definitions under the RRF namespace,
   7providing a bridge between the existing `IndisputableMonolith.Recognition` module
   8and the new RRF framework.
   9
  10Key concepts from Recognition.lean:
  11- `Recognize`: The fundamental pairing of recognizer and recognized
  12- `MP` (Metaphysical Primitive): Nothing cannot recognize itself
  13- `RecognitionStructure`: A type with a recognition relation
  14- `Chain`: A sequence of recognition steps
  15- `Ledger`: Double-entry bookkeeping for recognition
  16- `AtomicTick`: Discrete time structure
  17-/
  18
  19
  20namespace IndisputableMonolith
  21namespace RRF.Core
  22
  23-- Re-export core Recognition types under RRF namespace
  24
  25/-- Re-export: The fundamental recognition pairing. -/
  26abbrev Recognize := Recognition.Recognize
  27
  28/-- Re-export: The metaphysical primitive (MP). -/
  29abbrev MP := Recognition.MP
  30
  31/-- Re-export: MP holds. -/
  32theorem mp_holds : MP := Recognition.mp_holds
  33
  34/-- Re-export: Nothing cannot recognize itself. -/
  35abbrev NothingCannotRecognizeItself := Recognition.NothingCannotRecognizeItself
  36
  37theorem nothing_cannot_recognize_itself : NothingCannotRecognizeItself :=
  38  Recognition.nothing_cannot_recognize_itself
  39
  40/-- Re-export: Recognition structure. -/
  41abbrev RecognitionStructure := Recognition.RecognitionStructure
  42
  43/-- Re-export: Chain of recognition steps. -/
  44abbrev Chain := Recognition.Chain
  45
  46/-- Re-export: Ledger for double-entry. -/
  47abbrev RecogLedger := Recognition.Ledger
  48
  49/-- Re-export: Phi (net balance) function. -/
  50def phi {M : RecognitionStructure} (L : Recognition.Ledger M) : M.U → ℤ :=
  51  Recognition.phi L
  52
  53/-- Re-export: Chain flux. -/
  54def chainFlux {M : RecognitionStructure} (L : Recognition.Ledger M) (ch : Recognition.Chain M) : ℤ :=
  55  Recognition.chainFlux L ch
  56
  57/-- Re-export: Atomic tick class. -/
  58abbrev AtomicTick := Recognition.AtomicTick
  59
  60/-- Re-export: Atomicity theorem (T2). -/
  61theorem T2_atomicity {M : RecognitionStructure} [Recognition.AtomicTick M] :
  62    ∀ t u v, Recognition.AtomicTick.postedAt (M:=M) t u → Recognition.AtomicTick.postedAt (M:=M) t v → u = v :=
  63  Recognition.T2_atomicity
  64
  65/-- The bridge theorem: chainFlux is zero for balanced ledgers. -/
  66theorem chainFlux_zero_of_balanced {M : RecognitionStructure} (L : Recognition.Ledger M)
  67    (ch : Recognition.Chain M) (hbal : ∀ u, L.debit u = L.credit u) :
  68    Recognition.chainFlux L ch = 0 :=
  69  Recognition.chainFlux_zero_of_balanced L ch hbal
  70
  71end RRF.Core
  72end IndisputableMonolith
  73