`entropy`

definition

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.PartitionFunction
domain: Thermodynamics
line: 85 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Thermodynamics.PartitionFunction on GitHub at line 85.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  82  partitionFunction sys T hT
  83
  84/-- Entropy S = k_B(ln Z + β⟨E⟩). -/
  85noncomputable def entropy (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=
  86  k_B * (log (partitionFunction sys T hT) + beta T hT * averageEnergy sys T hT)
  87
  88/-- Heat capacity C_V = ∂⟨E⟩/∂T. -/
  89noncomputable def heatCapacity (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) : ℝ :=
  90  -- This would require calculus; placeholder
  91  k_B * (beta T hT)^2 *
  92    ((∑ i : Fin sys.numLevels,
  93      (sys.energy i)^2 * (sys.degeneracy i : ℝ) * exp (-beta T hT * sys.energy i)) /
  94    partitionFunction sys T hT - (averageEnergy sys T hT)^2)
  95
  96/-! ## RS Derivation: Ledger Sum -/
  97
  98/-- In Recognition Science, the partition function is a **sum over ledger states**.
  99
 100    Each microscopic configuration corresponds to a ledger entry.
 101    The Boltzmann weight exp(-βE) comes from the J-cost:
 102
 103    P(state) ∝ exp(-J_cost(state) / k_B T)
 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"

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.