IndisputableMonolith.Cosmology.RecognitionEquilibrium

declarations in this module (25)

• def pairResolve L51
• lemma pairResolve_at_i L54
• lemma pairResolve_at_j L58
• lemma pairResolve_other L62
• def levelSum L68
• lemma sum_split_pair L72
• theorem pairResolve_levelSum L90
• def varAround L105
• theorem varAround_pairResolve L109
• def meanLevel L125
• def variance L128
• theorem meanLevel_pairResolve L130
• theorem variance_pairResolve L137
• theorem variance_nonincreasing L143
• theorem jcost_nonneg L151
• theorem jcost_eq_zero_iff L157
• theorem phi_rpow_eq_one_iff L167
• theorem cost_phi_eq_zero_iff L179
• def totalCost L185
• theorem totalCost_nonneg L189
• theorem totalCost_eq_zero_iff L196
• structure Equilibrium L210
• theorem recognitionEquilibrium L220
• theorem conjugateBirth_chargeSum L243
• theorem manyBirths_chargeSum L252