IndisputableMonolith.Holography.RecordCostAsymmetry

declarations in this module (24)

• def recordCost L116
• def microstateCost L121
• theorem log2_eq_zero_of_le_one L128
• theorem record_zero_general L136
• theorem record_zero_of_constant L143
• theorem recordCost_closed L156
• theorem recordCost_domino L161
• theorem fiber_posts_one_record L173
• theorem records_performed L180
• theorem recordCost_eq_multiplicity_one L189
• theorem recordCost_eq_multiplicity_two L197
• theorem selector_forced L211
• theorem bekenstein_selector_from_asymmetry L226
• theorem one_le_log2_of_two_le L233
• theorem microstate_cost_nonzero_on_constant L251
• def target_record_cost_asymmetry L273
• theorem target_record_cost_asymmetry_holds L287
• theorem recordCostAsymmetryCert L298
• def HorizonEntropyIsRecordCost L336
• def HorizonEntropyIsMicrostateCost L343
• theorem bekenstein_coefficient_of_record_cost L348
• theorem kappa_four_thirds_of_microstate_cost L359
• theorem record_zero_separates_readings L375
• theorem bekenstein_tag_b_cert L387