Information Thermodynamics Reciprocity Skew

The skew measure

In information thermodynamics, a system's state can be described by the ratios between its parts. The reciprocity skew, a measure of imbalance, is the sum of the absolute values of the natural logarithms of these ratios. A ratio of 1, meaning perfect balance, contributes zero; a ratio of 2 and a ratio of 1/2 both contribute the same positive amount, about 0.693. This symmetry is what makes the measure a skew: it treats reciprocal relationships as equally imbalanced, regardless of direction.

The Recognition Science framework defines this skew as a foundational quantity in its information-theoretic ledger, a discrete record of recognition events. The framework's library, a machine-checked collection of formal theorems, defines the skew as the sum over all active bonds of |log(bond_multiplier)|. This definition is not a theorem; it is a modeling choice, a way of assigning a number to a state. The framework also defines ledger entropy as exactly this skew, making the two terms interchangeable by definition.

The framework then proves a thermodynamic consequence. Its Landauer bound theorem states that the total recognition cost, the sum of J-costs across the ledger, is at least half the sum of the squares of the logarithms of the bond multipliers. Since the skew is the sum of absolute logarithms, and the square of a number is always at least its absolute value for numbers greater than 1, this bound implies that the cost grows at least quadratically with the skew. A state twice as imbalanced in its ratios costs at least four times as much to maintain, a sharpening of the linear intuition one might have from the skew alone.

This quadratic lower bound is the framework's version of the Landauer principle, the physical limit on the energy cost of erasing information. In this account, the cost is not a free parameter but a forced consequence of the recognition cost function. The framework also defines a thermal cost per tick as T times the natural log of 2, and proves that a recognition operator, a rule for evolving the ledger, never increases total cost. These results give the skew a thermodynamic role: it is not just a descriptive statistic but a quantity whose square bounds the unavoidable dissipation.

The skew itself, however, is only a definition. It does not, by itself, establish any physical law. The theorems that use it, such as the dissipation bound, are proved for the framework's specific cost function and ledger structure. The framework does not claim that this skew is the entropy of any real physical system, nor that the Landauer bound it derives applies outside its own model. Those are empirical questions, not formal ones.

/-- Entropy proxy: sum of absolute log-imbalances over active bonds. -/
noncomputable def reciprocity_skew (s : LedgerState) : ℝ :=
  s.active_bonds.sum (fun b => |Real.log (s.bond_multipliers b)|)

/-- **DEFINITION: Ledger Entropy**
    Entropy defined as the absolute log-imbalance of the ledger. -/
noncomputable def ledger_entropy (s : LedgerState) : ℝ :=
  reciprocity_skew s

/-- **Entropy Dissipation Theorem**
    The total recognition cost of a state is bounded below by the quadratic
    sum of the information mismatches. -/
theorem total_dissipation_bound (s : LedgerState) :
    RecognitionCost s ≥ (1/2 : ℝ) * (s.active_bonds.sum (fun b => (Real.log (s.bond_multipliers b))^2)) := by
  unfold RecognitionCost
  rw [Finset.mul_sum]
  apply Finset.sum_le_sum
  intro b hb
  have h := landauer_bound_holds s b hb
  dsimp at h
  linarith

/-- **8-Tick Dissipation Limit**
    The total dissipation over one 8-tick cycle corresponds to the Landauer limit
    for pattern closure. -/
theorem eight_tick_dissipation_limit (R : RecognitionOperator) (s : LedgerState) :
    let s_next := R.evolve s
    -- Over one complete cycle, the integrated cost balances the erasure
    admissible s → admissible s_next → RecognitionCost s_next ≤ RecognitionCost s := by
  intro s_next hadm_s _
  exact R.minimizes_J s hadm_s

What this page does not claim

The reciprocity skew is not claimed to be the entropy of any real physical system outside the framework's model. The Landauer bound is not claimed to apply to physical computers or biological systems without an empirical mapping. The definition of the skew does not by itself establish any thermodynamic law; only the theorems that use it do.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/Thermodynamics.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: