`Recognize`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Core.Recognition
domain: RRF
line: 26 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Core.Recognition on GitHub at line 26.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

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