IndisputableMonolith.Cost.UnitFromMinimality

declarations in this module (24)

• lemma jcost_rpow_inv L59
• lemma jcost_pow_inv L66
• lemma jcost_lt_odd_power_of_one_lt L75
• theorem jcost_lt_odd_power L89
• theorem unit_is_selected_by_minimality L101
• def IsLeastOddPowerCost L114
• theorem isLeast_iff_canonical L121
• lemma jcost_lt_pow_of_one_lt L157
• theorem jcost_lt_pow L170
• theorem unit_is_selected_by_minimality_over_powers L179
• def IsLeastPowerCost L186
• theorem isLeastPower_iff_canonical L191
• theorem exponent_zero_charges_nothing L213
• theorem exponent_zero_undercuts_everything L217
• theorem anchor_iff_canonical L234
• theorem anchor_is_minimality L252
• theorem anchorPower_iff_canonical L258
• theorem anchor_is_minimality_over_powers L271
• theorem cost_of_the_first_distinction L280
• lemma gauge_halving_is_cheaper_of_one_lt L286
• theorem no_least_gauge_member L299
• theorem gauge_tendsto_zero L311
• theorem zero_cost_is_admissible L329
• theorem discrete_gauge_has_a_floor_and_continuous_gauge_does_not L349