IndisputableMonolith.Gravity.RecognitionLedger

declarations in this module (24)

• def rclGate L55
• theorem rclGate_symmetric L57
• theorem rclGate_zero_right L60
• theorem rclGate_zero_left L63
• theorem rclGate_nonneg L66
• structure RecognitionLedger L74
• def flatLedger L90
• def isFlat L98
• theorem flatLedger_isFlat L101
• def totalCost L108
• theorem totalCost_nonneg L113
• theorem totalCost_eq_zero_iff_flat L123
• theorem flatLedger_totalCost_zero L146
• def deficit L153
• theorem deficit_nonneg L158
• theorem totalCost_eq_sum_deficits L166
• structure SubstrateBipartition L175
• def boundaryCost L184
• theorem boundaryCost_nonneg L189
• theorem boundaryCost_symmetric L201
• structure RecognitionLedgerCert L213
• def recognitionLedgerCert L223
• theorem recognitionLedgerCert_inhabited L229
• theorem recognition_ledger_one_statement L238