module module

`IndisputableMonolith.LedgerUniqueness`

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

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Causality.Basic module_import
IndisputableMonolith.Potential module_import
IndisputableMonolith.Recognition module_import

declarations in this module (8)

structure Kinematics L7
inductive ReachN L9
def inBall L12
def Reaches L13
def IsAffine L23
lemma unique_on_reachN L26
lemma unique_on_inBall L38
lemma unique_up_to_const_on_component L47