module module

`IndisputableMonolith.Physics.NullRecognitionMode`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (21)

structure CarrierEvent L27
structure PropagatingMode L33
def perTickCost L37
def totalModeCost L41
def GaugeEquivalent L46
def canonicalNRM L50
abbrev zeroMode L54
theorem canonicalNRM_ratio L56
theorem zeroMode_ratio L59
theorem canonicalNRM_perTickCost L63
theorem nrm_totalCost_zero L69
theorem zeroMode_totalCost L76
theorem nullRecognitionMode_nonempty L80
theorem zeroCostMode_nonempty L85
theorem perTickCost_nonneg L92
theorem perTickCost_zero_of_total_zero L98
theorem ratio_eq_one_of_total_zero L109
theorem zeroCostMode_unique_up_to_gauge L117
structure NullRecognitionModeCert L125
def nullRecognitionModeCert L131
theorem nullRecognitionModeCert_inhabited L136