module module high

`IndisputableMonolith.Thermodynamics.RecognitionThermodynamics`

This module introduces Recognition Temperature T_R to parameterize noise and exploration in Recognition Science, with T_R=0 recovering deterministic J-minimization and T_R to infinity recovering maximum disorder. It supplies the core definitions of Gibbs weights, partition functions, and recognition entropy that all downstream thermodynamic modules import. The module consists entirely of definitions and elementary positivity lemmas.

claimLet $T_R$ be the Recognition Temperature. For a Recognition System equipped with cost $J$, the Gibbs weight is $w(x) = e^{-J(x)/T_R}$, the partition function is $Z = sum_x w(x)$, and the recognition entropy is the Shannon entropy of the normalized Gibbs measure.

background

Recognition Science begins from the T=0 foundation in which physical states are defined by absolute minimization of the universal cost $J(x) = 1/2(x + 1/x) - 1$ (from the PhiForcing module). The present module extends that foundation by introducing a single scalar parameter $T_R$ that controls the relative weight of higher-cost states. Sibling definitions include RecognitionSystem (the underlying ledger), gibbs_weight, partition_function, and recognition_entropy, all expressed directly in terms of $J$ and $T_R$.

proof idea

This is a definition module, no proofs. The module simply declares the Recognition Temperature, the Gibbs weight formula, the partition function, and the induced probability measure, together with immediate non-negativity and normalization lemmas.

why it matters in Recognition Science

The module supplies the statistical-mechanics layer that feeds JCostBoltzmann, JCostEntropyAncestor, MaxEntFromCost, MemoryLedger, and SecondLaw. It thereby converts the deterministic J-cost structure (T5 J-uniqueness and T6 phi fixed point) into a finite-temperature theory whose $T_R to 0$ limit recovers the original Recognition Science ledger.

scope and limits

Does not derive the second law or any fluctuation theorem.
Does not fix the numerical value of $T_R$ in physical units.
Does not connect $T_R$ to the fine-structure constant or other RS constants.
Does not treat continuous or quantum extensions of the ledger.

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Thermodynamics module_import
IndisputableMonolith.Thermodynamics.JCostBoltzmann module_import
IndisputableMonolith.Thermodynamics.JCostEntropyAncestor module_import
IndisputableMonolith.Thermodynamics.MaxEntFromCost module_import
IndisputableMonolith.Thermodynamics.MemoryLedger module_import
IndisputableMonolith.Thermodynamics.SecondLaw module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (26)

structure RecognitionSystem L44
def gibbs_weight L65
theorem gibbs_weight_pos L69
theorem gibbs_weight_one L73
def partition_function L79
theorem partition_function_pos L84
def gibbs_measure L94
theorem gibbs_measure_nonneg L99
theorem gibbs_measure_sum_one L105
theorem gibbs_measure_pos L112
structure ProbabilityDistribution L120
def recognition_entropy L130
def expected_cost L135
def recognition_free_energy L140
def free_energy_from_Z L145
theorem free_energy_identity L151
def kl_divergence L197
theorem kl_divergence_nonneg L202
def T_phi L243
theorem T_phi_pos L246
def phi_temperature_system L251
structure CoherenceThreshold L260
def rs_coherence L273
theorem coherence_at_phi_temp L276
def eight_tick L283
def fundamental_frequency L287