module module high

`IndisputableMonolith.Thermodynamics.JCostThermoBridge`

This module maps J-cost of configuration ratios directly to energy, allowing thermodynamic quantities such as Boltzmann factors and partition functions to be written in RS-native terms. Researchers deriving discrete thermodynamics from the 8-tick clock or the Law of Existence would cite these results when expressing standard statistical mechanics inside the Recognition framework. The module proceeds by a chain of definitions followed by short algebraic lemmas establishing non-negativity, monotonicity, and positivity of the derived quantities.

claimEnergy of a configuration ratio $r$ is defined by $E(r) = c_J J(r)$ for a positive constant $c_J$ fixed by the RS time quantum. The inverse temperature is recovered as the derivative of the log-partition function with respect to the J-cost scale, and the Boltzmann weight for each state is proportional to $e^{-J(r_i)}$.

background

The module sits inside the Thermodynamics domain and imports the J-cost function from the Cost module, the discrete 8-tick clock from EightTick, and the existence criterion defect(x)=0 from LawOfExistence. Constants supplies the RS-native time quantum τ₀=1 tick. SpinStatistics supplies the 8-tick phase structure that later yields Fermi-Dirac and Bose-Einstein statistics. The central object is the proportionality between energy and J-cost of the configuration ratio, which converts the Recognition Composition Law into thermodynamic potentials without extra postulates.

proof idea

This is a definition module whose core is the single definition energyFromJCost. Subsequent lemmas are one-line wrappers: energy_nonneg applies the known non-negativity of J, energy_min_at_unity uses the fixed-point property of J at unity, and the Boltzmann and partition lemmas follow by direct substitution of the energy definition into the exponential and summation. No deep tactic chains or external theorems beyond the imported Cost and Constants facts are required.

why it matters in Recognition Science

The module supplies the missing link that lets the J-cost function generate thermodynamic observables, thereby connecting the Cost module and the EightTick structure to concrete statistical mechanics. It fills the step that converts the abstract Recognition Composition Law into the partition function and state probabilities used in downstream thermodynamics. No parent theorems are listed in the used-by graph, indicating it functions as an interface layer rather than a terminal result.

scope and limits

Does not derive the continuum thermodynamic limit or fluctuation theorems.
Does not incorporate interactions beyond the single-configuration J-cost.
Does not address renormalization or running of the proportionality constant.
Does not treat time-dependent or non-equilibrium processes.

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.EightTick module_import
IndisputableMonolith.Foundation.LawOfExistence module_import
IndisputableMonolith.QFT.SpinStatistics module_import

declarations in this module (21)

def energyFromJCost L56
theorem energy_nonneg L60
theorem energy_min_at_unity L66
def inverseTemperature L74
def jcostBoltzmann L78
def standardBoltzmann L82
theorem jcost_boltzmann_pos L86
theorem jcost_boltzmann_max_at_unity L90
theorem jcost_boltzmann_monotone L96
def partitionFunction L110
theorem partition_pos L115
def stateProbability L126
theorem fermi_from_odd_phase L134
theorem bose_from_even_phase L144
def fermiDirac L157
theorem fermi_bounded L161
def boseEinstein L180
theorem bose_pos L184
def freeEnergy L200
theorem free_energy_decomposition L205
theorem jcost_thermo_fundamentals L222