  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.