IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCostDerivation

declarations in this module (98)

• abbrev AlphabetGauge L222
• theorem alphabetGauge_eq_sectorGroup L227
• theorem card_alphabetGauge L230
• theorem gibbsWeight_eq_inv_card_alphabetGauge L238
• def LetterCost L249
• def historyCost L255
• def postedWeight L260
• theorem postedWeight_pos L263
• def Equivariant L270
• theorem historyCost_invariant L276
• theorem postedWeight_invariant L282
• def KindRates L292
• def KindOnly L303
• theorem historyCost_of_kindRates L309
• theorem kindOnly_equivariant L330
• theorem postedWeight_sizeBlind L344
• theorem posting_cost_derives_premise_one L354
• theorem linearCost_atoms_force_zero L365
• theorem kindRates_atoms_force_zero L400
• theorem posting_cost_derives_gibbs L407
• theorem classMass_gibbsWeight_eq_mu L418
• theorem posting_cost_derives_mu L437
• def PostedBy L458
• theorem postedBy_postedWeight L462
• theorem postedBy_eq_postedWeight L468
• theorem measure_from_posting_premises L492
• def CostSizeBlind L511
• theorem postedWeight_sizeBlind_iff L518
• theorem kindOnly_costSizeBlind L539
• def squareCost L547
• theorem historyCost_squareCost L552
• theorem costSizeBlind_not_kindOnly L565
• def pairCost L598
• theorem historyCost_pairCost L603
• theorem costSizeBlind_and_atoms_do_not_give_gibbs L620
• def zeroCost L658
• theorem zeroCost_kindRates L660
• theorem zeroCost_kindOnly L663
• theorem postedWeight_zeroCost L666
• theorem zeroCost_normalizedAtTheAtoms L671
• theorem posting_premises_satisfiable L678
• def incidenceCost L690
• theorem incidenceCost_inl L696
• theorem incidenceCost_edge L699
• theorem incidenceCost_tet L703
• theorem historyCost_incidenceCost L709
• theorem postedWeight_incidenceCost L725
• theorem postedWeight_incidenceCost_eq L738
• theorem exp_neg_pos L743
• theorem exp_neg_ne_one L745
• theorem that L753
• theorem incidenceCost_equivariant L755
• theorem twoBridges_edges_proper L765
• theorem twoLoops_edges_loop L769
• theorem incidenceCost_not_kindOnly L775
• theorem incidencePosting_not_sizeBlind L787
• theorem incidencePosting_satisfiesTheOtherHypotheses L796
• theorem incidencePosting_classMass_ne_mu L802
• theorem incidence_silence_suffices_and_equivariance_does_not L841
• theorem equivariance_does_not_give_kindOnly L869
• theorem sizeBlind_not_always_posted L890
• theorem kindOnly_and_atoms_force_zeroCost L989
• theorem card_postingAlphabet L1001
• theorem card_alphabetGauge_pos L1005
• theorem postedBy_constrains_only_the_empty_complex L1022
• def KindTotalRates L1051
• def FixedKindTotals L1058
• theorem historyCost_of_kindTotalRates L1060
• theorem kindRates_kindTotalRates L1069
• theorem kindOnly_fixedKindTotals L1085
• theorem fixedKindTotals_costSizeBlind L1089
• theorem measure_from_fixedKindTotals L1098
• def centeredIncidenceCost L1124
• theorem centeredIncidenceCost_inl L1132
• theorem centeredIncidenceCost_edge L1135
• theorem centeredIncidenceCost_tet L1140
• theorem edgeSum_centeredIncidenceCost L1145
• theorem historyCost_centeredIncidenceCost L1160
• theorem postedWeight_centeredIncidenceCost L1169
• theorem centeredIncidenceCost_equivariant L1176

… and 18 more