module module

`IndisputableMonolith.Foundation.RecognitionLedgerFloor`

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

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

IndisputableMonolith.Foundation.LedgerFloorT0Bridge module_import
IndisputableMonolith.Foundation.LedgerToFactorization module_import
IndisputableMonolith.Holography.RecognitionMultiplicity module_import
IndisputableMonolith.LedgerFloor module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.CostFromDistinction module_import

declarations in this module (21)

abbrev DefectLedger L58
def ledgerCost L62
theorem ledgerCost_zero L65
theorem ledgerCost_add L71
theorem ledgerCost_single L79
theorem ledgerCost_nonneg L84
def ObservablySame L96
def observableSetoid L100
theorem ledgerCost_constant_on_classes L106
theorem observable_floor_iff_pos_weight L113
theorem ledgerCost_eq_zero_iff L142
theorem two_independent_same_defects L165
theorem boolean_floor_is_truncation L174
def booleanTruncation L180
theorem booleanTruncation_zero L183
theorem booleanTruncation_pos L187
theorem booleanTruncation_add_eq_or L193
theorem unit_cost_is_generator_count L208
instance ledgerConfigSpace L221
def ledgerCostFunction L248
theorem ledger_recognition_work_constraint L261