module module high

`IndisputableMonolith.Thermodynamics.RecognitionThermodynamics`

RecognitionThermodynamics introduces the Recognition Temperature T_R that interpolates between deterministic J-cost minimization at T_R=0 and maximum disorder at infinity. Researchers building statistical mechanics from Recognition Science foundations cite this module for its Gibbs weights, partition functions, and recognition entropy. The module consists of definitions and basic positivity and normalization properties.

claimThe Recognition Temperature $T_R$ parameterizes noise level, with $T_R=0$ restricting to $J=0$ states and $T_R o\infty$ yielding maximum disorder. Main objects are the Gibbs weight $\exp(-J(x)/T_R)$, the partition function $\sum\exp(-J(x)/T_R)$, and the recognition entropy derived from the resulting Gibbs measure.

background

Recognition Science starts from the J-cost functional $J(x)=\frac12(x+1/x)-1$ whose absolute minimum defines the T=0 ground state. The upstream PhiForcing module establishes that self-similarity on a discrete ledger forces the golden ratio $\phi$ as the unique fixed point. This module extends the T=0 foundation to finite temperature by introducing $T_R$ as the single parameter controlling exploration versus exploitation.

The module imports the Cost and PhiForcing foundations and defines RecognitionSystem, gibbs_weight, partition_function, gibbs_measure, and recognition_entropy together with their elementary properties (positivity, normalization to one). These objects supply the statistical mechanics layer used by all downstream thermodynamics modules.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the core definitions that feed JCostBoltzmann (biology-facing Boltzmann bridge), JCostEntropyAncestor (entropy derivation), MaxEntFromCost (maximum-entropy theorem), MemoryLedger (learning dynamics), and SecondLaw (second-law derivation). It therefore closes the step from the T=0 J-minimization foundation to finite-temperature thermodynamics inside Recognition Science.

scope and limits

Does not derive any thermodynamic law or inequality.
Does not assign numerical values of T_R to physical systems.
Does not connect J-cost to specific Hamiltonians or Lagrangians.
Does not address quantum or relativistic extensions.

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