module module moderate

`IndisputableMonolith.Thermodynamics.BoltzmannDistribution`

The BoltzmannDistribution module supplies core definitions for energy levels, systems, Boltzmann factors, partition functions and normalized probabilities in Recognition Science thermodynamics. Researchers deriving thermal statistics from the J-cost or RS constants would cite these objects. The module consists of type definitions plus short lemmas on positivity and normalization.

claimEnergyLevel := \{E : \mathbb{R}, g : \mathbb{N}\}, System a finite collection of EnergyLevel, boltzmannFactor(E,\beta) = e^{-\beta E}, partitionFunction = \sum g_i \cdot boltzmannFactor(E_i,\beta), probability_i = boltzmannFactor(E_i,\beta) / partitionFunction.

background

The module sits in the thermodynamics domain and imports Constants (where \tau_0 = 1 tick) together with Cost. It opens with EnergyLevel, documented as an energy level with degeneracy. It then defines System, boltzmannFactor, partitionFunction, probability and auxiliary lemmas such as boltzmannFactor_pos, partition_positive and prob_normalized.

These objects rest on the upstream cost structure to assign statistical weights. The setting prepares the canonical ensemble using RS-native units without introducing temperature scaling or dynamics.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the objects that later thermodynamics results rely on when linking the recognition cost to equilibrium distributions. It fills the initial layer of the thermodynamics section before any derivation of the full Boltzmann law or connection to the eight-tick octave.

scope and limits

Does not derive the distribution from the J-cost equation.
Does not fix the temperature scale in RS units.
Does not treat quantum statistics or degeneracy beyond the basic definition.
Does not prove normalization for continuous spectra.

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