module module

`IndisputableMonolith.Information.InformationIsLedger`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Information.ShannonEntropy module_import

declarations in this module (31)

structure RecognitionEvent L46
def infoCost L53
theorem info_cost_nonneg L57
theorem info_cost_zero_iff_unit L62
theorem info_cost_pos_of_ne_one L77
theorem info_cost_symmetric L86
def balancedEvent L94
theorem balanced_has_minimum_cost L98
theorem balanced_is_unique_minimum L106
theorem nothingness_infinite_cost L117
theorem zero_ratio_not_valid L137
theorem shannon_entropy_equals_expected_jcost L147
theorem entropy_nonneg L152
theorem deterministic_has_zero_entropy L158
theorem uniform_has_max_entropy L165
structure LedgerState L172
def totalInfoCost L177
lemma foldl_add_nonneg L181
theorem total_info_cost_nonneg L191
theorem empty_state_zero_cost L197
theorem ledger_identity L203
def k_B_ln2 L212
theorem landauer_constant_pos L216
theorem landauer_energy_pos L224
def erasure_jcost L230
theorem erasure_jcost_pos L233
theorem erasure_jcost_eq L241
theorem phi_irrational_information L250
theorem phi_self_similar L256
theorem phi_has_positive_info_cost L261
def ic001_certificate L270