IndisputableMonolith.Gravity.SevenGaps.Gap2LetterCostDichotomy

declarations in this module (72)

• def censusV L126
• def censusE L130
• def censusT L133
• def evalMoments L136
• theorem censusV_eq_moments L139
• theorem censusE_eq_moments L146
• theorem censusT_eq_moments L153
• theorem censusV_pos L160
• structure CensusDilateFamily L174
• def flatCap L182
• def flatComplex L185
• def flatFamily L196
• def SurfaceTotal L214
• def SurfaceAreaTotal L218
• theorem historyCost_on_family L223
• theorem surface_and_kindTotals_force_zero L238
• theorem surface_at_positive_dilates_forces_zero L259
• theorem surfaceArea_and_kindTotals_force_zero L279
• theorem surface_and_fixedKindTotals_force_zero_historyCost L298
• theorem the_measure_is_exactly_the_gauge_divisor L310
• theorem atom_normalizations_are_derived L335
• theorem census4_columns_independent L350
• theorem surface_moment_forces_zero_rates L363
• def kindRateCost L387
• theorem kindRateCost_kindRates L393
• theorem kindRateCost_kindOnly L397
• theorem kindRateCost_equivariant L400
• theorem kindRateCost_fixedKindTotals L403
• theorem historyCost_kindRateCost_on_family L407
• theorem historyCost_kindRateCost_dust_one L413
• theorem bulk_cancellation_is_load_bearing L422
• theorem purity_of_the_surface_term_is_load_bearing L441
• theorem the_two_relaxations_cannot_be_combined L460
• def sideOf L483
• theorem sideOf_censusV L485
• theorem sideOf_one L493
• theorem sideOf_sixteen L499
• def surfaceCost L509
• theorem surfaceCost_inl L514
• theorem surfaceCost_edge L517
• theorem surfaceCost_tet L520
• theorem vertexBlockSum_surfaceCost L523
• theorem historyCost_surfaceCost L532
• theorem surfaceCost_equivariant L542
• theorem surfaceCost_surfaceTotal L551
• theorem surfaceCost_not_fixedKindTotals L563
• theorem fixed_kind_totals_is_load_bearing L578
• def indexTiltCost L598
• theorem indexTiltCost_inl L603
• theorem indexTiltCost_edge L607
• theorem indexTiltCost_tet L610
• theorem vertexSum_indexTilt L613
• theorem indexTiltCost_kindTotalRates L631
• theorem indexTiltCost_fixedKindTotals L641
• theorem historyCost_indexTiltCost L644
• theorem indexTiltCost_surfaceTotal L649
• def v0Dust2 L656
• def v1Dust2 L659
• def swapDust2 L663
• theorem swapDust2_v0 L670
• theorem indexTiltCost_at_v0 L674
• theorem indexTiltCost_at_v1 L680
• theorem indexTiltCost_not_equivariant L687
• theorem equivariance_is_not_load_bearing L700
• theorem the_letter_level_fibre_is_not_a_point L724
• structure LetterCostDichotomyVerdict L742
• theorem letterCostDichotomyVerdict L786
• structure DichotomyIndex L825
• def dichotomyIndex L843
• theorem index_no_triple L852
• theorem index_flag_unmoved L854
• theorem index_equivariance_unused L856