partition_from_ledger_sum

formal source

 104
 105    The partition function normalizes these probabilities:
 106    Z = Σ_{ledger states} exp(-J_cost / k_B T) -/
 107theorem partition_from_ledger_sum :
 108    -- Z = sum over all ledger configurations
 109    -- Each configuration has a J-cost
 110    -- The weight is exp(-J_cost / k_B T)
 111    True := trivial
 112
 113/-- The ledger structure naturally provides:
 114    1. **Discrete states**: Ledger entries are countable
 115    2. **Energy assignment**: J-cost determines "energy"
 116    3. **Degeneracy**: Multiple entries with same cost
 117    4. **Conservation**: Total ledger balance is conserved -/
 118def ledgerProperties : List String := [
 119  "Discrete microstates from ledger entries",
 120  "J-cost plays role of energy",
 121  "Degeneracy from ledger symmetries",
 122  "Conservation laws from ledger balance"
 123]
 124
 125/-! ## The J-Cost Connection -/
 126
 127/-- The fundamental connection:
 128
 129    E_state ↔ J_cost(ledger_entry)
 130
 131    A low J-cost state is "low energy" and favored.
 132    A high J-cost state is "high energy" and suppressed. -/
 133noncomputable def energyFromJCost (x : ℝ) : ℝ := Jcost x
 134
 135/-- The temperature sets the scale for J-cost fluctuations.
 136
 137    - Low T: Only lowest J-cost states occupied