IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGenerated · Recognition explainer

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGeneratedHostileProbe module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2GluingDerivation module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondRank module_import

declarations in this module (72)

def LedgerGenerated L79
def LedgerGeneratedAt L90
theorem LedgerGenerated_implies_at L98
def jCostVertexCharge L109
theorem jCost_ledgerGenerated L115
theorem jCost_ledgerGenerated_cap1 L127
theorem jCost_ledgerGenerated_cap2 L131
theorem jCost_ledgerGenerated_cap3 L135
def jCost_ledgerGenerated_decision_cap1 L140
def jCost_ledgerGenerated_decision_cap2 L141
def jCost_ledgerGenerated_decision_cap3 L142
theorem jCost_ledgerGenerated_decision_cap1_eq L144
theorem jCost_ledgerGenerated_decision_cap2_eq L146
theorem jCost_ledgerGenerated_decision_cap3_eq L148
def censusVertexCost L158
theorem censusVertexCost_not_ledgerGenerated L166
theorem historyCost_jCost_one L184
def loop1Complex L190
theorem imbalanceSq_point L200
theorem imbalanceSq_edge L201
theorem imbalanceSq_path L202
theorem imbalanceSq_loop1 L203
theorem imbalanceSq_empty_cap1 L204
theorem imbalanceSq_edge_native L209
theorem imbalanceSq_path_native L210
theorem imbalanceSq_loop1_native L211
theorem imbalanceSq_loopPoint_native L212
theorem imbalanceSq_fork_native L214
theorem historyCost_jCost_one_edge L216
theorem historyCost_jCost_one_point L221
theorem historyCost_jCost_one_path L225
theorem historyCost_jCost_one_loopPoint L230
theorem historyCost_jCost_one_fork L234
theorem historyCost_loop1 L239
theorem historyCost_empty_cap1 L244
theorem historyCost_table_cap1 L251
def historyCost_identically_zero_decision_cap1 L257
theorem historyCost_identically_zero_decision_cap1_eq L258
theorem historyCost_not_identically_zero_cap2 L263
def historyCost_identically_zero_decision_cap2 L268
theorem historyCost_identically_zero_decision_cap2_eq L269
theorem historyCost_not_identically_zero_cap3 L273
def historyCost_identically_zero_decision_cap3 L282
theorem historyCost_identically_zero_decision_cap3_eq L283
def historyCostRational L294
theorem historyCostRational_edge L296
theorem historyCostRational_fork L298
theorem historyCostRational_zero L300
def historyCostSeedTable L304
theorem historyCostSeedTable_length L313
theorem historyCostSeedTable_edge_row L315
theorem historyCostSeedTable_edge_row_native L318
structure CapHistoryTally L323
def measuredHistoryCaps L329
theorem measured_cap1_zero L337
theorem measured_cap2_nonzero L341
theorem measured_cap3_nonzero L345
def C27TriggerAt L355
theorem edgeComplex_fits_cap2 L360
theorem edgeComplex_fits_cap3 L364
theorem C27_trigger_armed_cap2 L369
theorem C27_trigger_armed_cap3 L375
def C27_hard_stop_armed L381
theorem C27_hard_stop_armed_eq L382
theorem C27_not_armed_by_cap1_seeds L385
structure LedgerGeneratedVerdict L396
theorem ledgerGeneratedVerdict L413
structure LedgerGeneratedIndex L425
def ledgerGeneratedIndex L433
theorem index_c27_armed L441
theorem index_flag_unmoved L442
theorem index_jCost_true L443