IndisputableMonolith.Information

   1import IndisputableMonolith.Information.CompressionPrior
   2import IndisputableMonolith.Information.EMLFromRecognition
   3import IndisputableMonolith.Information.FEPBridgeFromJCost
   4import IndisputableMonolith.Information.JCostNecessity
   5import IndisputableMonolith.Information.Thermodynamics
   6
   7/-!
   8# Information Bridge Aggregator
   9
  10This module aggregates the information-theoretic and thermodynamic
  11foundation of Recognition Science.
  12
  13## Modules
  14- `CompressionPrior`: Minimum Description Length (MDL) grounded in J-cost.
  15- `EMLFromRecognition`: Oriented exp-log compiler gate from ledger coordinates.
  16- `FEPBridgeFromJCost`: Local FEP/KL contact with reciprocal J-cost.
  17- `JCostNecessity`: Proof of J-cost uniqueness from recognition axioms.
  18- `Thermodynamics`: Landauer limit and 8-tick dissipation.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Information
  23
  24/-- **HYPOTHESIS**: J-Cost Uniqueness.
  25    The J-cost is the unique symmetric minimal information cost.
  26
  27    STATUS: SCAFFOLD — Proof established in `Information.JCostNecessity`.
  28    TODO: Fully unify the uniqueness theorem with the aggregator. -/
  29def H_UniquenessVerified : Prop :=
  30  ∀ (F : ℝ → ℝ), InformationCost F → (∀ x > 0, F x = Cost.Jcost x)
  31
  32-- Legacy axiom eliminated. See CostUniqueness.T5_uniqueness_complete.
  33
  34/-- **HYPOTHESIS**: Thermodynamic Bound.
  35    Recognition cost satisfies the Landauer bound for information erasure.
  36
  37    STATUS: SCAFFOLD — Bound derived in `Information.Thermodynamics`.
  38    TODO: Complete the Taylor expansion proof in `Thermodynamics.lean`. -/
  39def H_ThermodynamicsVerified : Prop :=
  40  ∀ (s : Thermodynamics.LedgerState), ∀ b ∈ s.active_bonds,
  41    let m := s.bond_multipliers b
  42    let u := Real.log m
  43    Cost.Jcost m ≥ u^2 / 2
  44
  45-- Legacy axiom eliminated. See Foundation.ConstantDerivations.
  46
  47end Information
  48end IndisputableMonolith
  49