module module moderate

`IndisputableMonolith.Thermodynamics.BoltzmannDistribution`

This module defines the Boltzmann distribution in Recognition Science by introducing energy levels with degeneracy, systems, Boltzmann factors, partition functions, and normalized probabilities. It would be cited by researchers deriving thermodynamic probabilities from the J-cost and RS constants. The module consists of definitions and basic lemmas for non-negativity and normalization.

claimEnergyLevel is a structure with energy $E$ and degeneracy $g$. The Boltzmann factor is $e^{-E}$, the partition function is $Z = sum g_i e^{-E_i}$, and the probability for each level is the normalized Boltzmann factor.

background

The module builds directly on IndisputableMonolith.Constants, which supplies the RS-native time quantum with doc-comment stating the fundamental RS time quantum (RS-native) where τ₀ = 1 tick. It also imports IndisputableMonolith.Cost to ground quantities in the J-cost framework of Recognition Science. Key objects introduced are EnergyLevel (an energy level with degeneracy), System, boltzmannFactor, partitionFunction, and probability, together with lemmas such as boltzmannFactor_pos and prob_normalized.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the foundational definitions for the Boltzmann distribution in the thermodynamics domain. It feeds parent theorems on thermodynamic equilibrium and entropy derivations within the Recognition framework, connecting the cost function to probabilistic system descriptions. No used_by edges are recorded yet.

scope and limits

Does not derive the distribution from the J-functional equation.
Does not assign specific energy values or temperatures.
Does not address quantum or relativistic corrections.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (29)

structure EnergyLevel L54
structure System L63
def boltzmannFactor L72
def partitionFunction L76
lemma boltzmannFactor_pos L80
lemma list_sum_nonneg_of_pos L88
theorem partition_positive L98
def probability L121
theorem prob_nonneg L126
lemma finset_sum_eq_list_sum_aux L136
lemma finset_sum_eq_list_sum L147
theorem prob_normalized L153
def levelCost L172
theorem partition_ge_ground L179
def temperature L186
theorem temperature_thermodynamic L190
def averageEnergy L199
def entropy L203
def freeEnergy L207
theorem free_energy_identity L211
theorem entropy_nonneg_of_Z_ge_one L226
def recognitionCost L239
theorem recognition_cost_well_defined L246
def twoLevelSystem L253
def groundStateProb L262
theorem high_temp_value L266
theorem high_temp_limit L276
theorem low_temp_limit L292
structure BoltzmannFalsifier L326