module module

`IndisputableMonolith.Holography.SeamLedgerDischarge`

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.Holography.HorizonClockRate module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Holography.SeamTransferCore module_import

declarations in this module (23)

theorem two_le_add_inv L61
theorem add_inv_eq_two_iff L67
theorem conserving_trace_eq L86
theorem conserving_trace_ge_two L94
theorem conserving_trace_eq_two_iff L103
theorem conserving_trace_bound L115
structure TraceReading L142
def LedgerClosurePricing L172
theorem b2_unique_zero_of_ledgerClosure L191
def anomalyReading L220
theorem anomalyReading_apply L228
theorem conservingSeamPricing_of_anomalyLedger L234
theorem anomalyLedger_iff_conserving L247
theorem censusPricing_of_anomalyLedger L259
theorem cost_eq_J_of_anomalyLedger L269
theorem b2_unique_zero_of_anomalyLedger L278
theorem ledgerClosurePricing_turnRatioCost L290
theorem ledgerClosurePricing_readingCost L311
theorem faithfulness_is_load_bearing L332
theorem calibration_is_load_bearing L359
instance is L380
structure SeamLedgerDischargeCert L384
theorem seamLedgerDischargeCert L398