IndisputableMonolith.Cosmology.RungCoarsen

declarations in this module (26)

• structure Event L59
• def sameBlock L65
• def internalOf L71
• def crossOf L75
• def relabel L80
• def coarseLedger L85
• def refineCell L90
• def roundtrip L94
• theorem cross_add_internal L100
• theorem roundtrip_eq L108
• theorem conserved L117
• def count L122
• def spectrum L125
• def cost L128
• theorem count_preserved L130
• theorem spectrum_preserved L133
• theorem cost_preserved L136
• theorem cost_add L141
• theorem cost_coarse_eq_cross L147
• theorem cost_partition L155
• def netFlow L165
• theorem sigma_preserved L170
• theorem idle_carries_nothing L179
• structure CoarseningExact L196
• theorem coarseningExact L205
• theorem t1_coarsening_exact L221