module module

`IndisputableMonolith.Potential`

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 (1)

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

IndisputableMonolith.LedgerUniqueness module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Causality.Basic module_import
IndisputableMonolith.Recognition module_import

declarations in this module (12)

abbrev Pot L12
def DE L15
def Kin L18
lemma edge_diff_invariant L21
lemma diff_const_on_ReachN L30
lemma diff_const_on_component L42
theorem T4_unique_on_reachN L50
theorem T4_unique_on_component L60
theorem T4_unique_on_inBall L68
theorem T4_unique_up_to_const_on_component L77
lemma increment_on_ReachN L88
lemma diff_in_deltaSub L106