IndisputableMonolith.Gravity.SevenGaps.Gap2DynamicsKindRule

declarations in this module (39)

• def zeroLedger L92
• def postAt L99
• inductive PostReachable L110
• theorem phi_zeroLedger L117
• theorem phi_postAt_debit_self L119
• theorem phi_postAt_credit_self L128
• theorem phi_postAt_ne L137
• theorem ledger_ext L155
• def mass L165
• theorem eq_zeroLedger_of_mass_zero L169
• theorem exists_pos_of_ne_zero L182
• def predOf L202
• theorem postAt_predOf L210
• theorem predOf_nonneg L256
• theorem mass_predOf_lt L289
• theorem postReachable_zero_of_nonneg L362
• theorem imbalance_realized L397
• structure does L416
• abbrev Schedule L417
• def runSchedule L420
• def phiAfter L428
• theorem runSchedule_eq_of_agree_below L432
• theorem postReachable_run L445
• theorem exists_schedule_of_reachable L458
• theorem imbalance_realized_by_schedule L474
• def incidenceImbalance L488
• theorem dynamics_produces_incidence_countermodel L505
• def CountsOnlyImbalance L537
• def CountsOnlySchedule L549
• def cmEdge0 L554
• def cmEdge1 L557
• theorem cmEdge1_ne_cmEdge0 L559
• def countermodelSchedule L567
• theorem schedule_countermodel_not_countsOnly L575
• theorem about L606
• theorem ledger_forces_countsOnly_at_no_layer L607
• structure Index L621
• def index L628
• theorem index_audit L647