module module

`IndisputableMonolith.LedgerFloor`

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 module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LedgerFloorT0Bridge module_import
IndisputableMonolith.Foundation.RecognitionLedgerFloor module_import

declarations in this module (11)

abbrev DefectLedger L43
abbrev ledgerCost L46
abbrev ledgerCost_add L49
abbrev two_independent_same_defects L53
abbrev observable_floor_iff_pos_weight L58
abbrev boolean_floor_is_truncation L62
abbrev LedgerFloorT0Bridge L69
abbrev ledger_floor_t0_bridge L73
abbrev ledgerToFloor_surjective L77
abbrev rank1_cost_is_boolean_truncation L82
abbrev ledger_t0_identification_certificate L87