module module

`IndisputableMonolith.Recognition`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Core.Recognition module_import
IndisputableMonolith.Foundation.RecognitionForcing module_import
IndisputableMonolith.LedgerPostingAdjacency module_import
IndisputableMonolith.LedgerUniqueness module_import
IndisputableMonolith.Potential module_import
IndisputableMonolith.Recognition.Cycle3 module_import
IndisputableMonolith.Recognition.ModelingExamples module_import
IndisputableMonolith.RRF.Core.Recognition module_import

declarations in this module (24)

abbrev Nothing L9
structure Recognize L12
def MP L17
theorem mp_holds L19
abbrev NothingCannotRecognizeItself L25
theorem nothing_cannot_recognize_itself L28
structure RecognitionStructure L31
structure Chain L35
def head L42
def last L45
structure Ledger L50
def phi L57
def chainFlux L59
class Conserves L62
lemma chainFlux_zero_of_loop L65
lemma phi_zero_of_balanced L68
lemma chainFlux_zero_of_balanced L72
class AtomicTick L77
theorem T2_atomicity L81
structure U L95
def recog L99
def M L101
def L L103
def twoStep L105