module module high

`IndisputableMonolith.Information.InformationIsLedger`

Recognition events are formalized as positive ratios in the ledger, each encoding a physical fact. InformationIsLedger supplies the basic objects and cost functions for information measures in Recognition Science. The module connects constants, J-cost structures, and Shannon entropy derivations to establish the ledger foundation.

claimA recognition event is a positive real number $x > 0$ representing a ratio in the ledger. The information cost of such an event is defined via the J-cost function and satisfies non-negativity, vanishing only at the unit ratio, and symmetry under inversion.

background

The module sits in the Information domain and imports the RS time quantum τ₀ = 1 tick, cost functions, and the Shannon entropy construction. RecognitionEvent is introduced as the basic ledger object. The upstream ShannonEntropy module targets derivation of Shannon entropy H = -Σ p_i log(p_i) directly from the J-cost structure of Recognition Science.

proof idea

This is a definition module, no proofs. It establishes RecognitionEvent and the associated information cost properties through direct definitions followed by elementary lemmas on non-negativity and symmetry.

why it matters in Recognition Science

The module supplies the ledger encoding required for the Shannon entropy derivation from J-cost (INFO-001). It anchors information measures to the J-uniqueness and cost axioms of the Recognition framework, preparing the ground for entropy calculations on physical ratios.

scope and limits

Does not derive numerical entropy values for specific physical systems.
Does not treat multi-event or continuous distributions beyond the basic ledger.
Does not incorporate observer or measurement dynamics.

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