module module high

`IndisputableMonolith.Thermodynamics.RecognitionThermodynamics`

RecognitionThermodynamics introduces the Recognition Temperature T_R that interpolates between deterministic J-minimization at T_R=0 and maximum disorder at T_R→∞. It supplies the core objects Gibbs weight exp(-J/T_R), partition function, and recognition entropy for the thermodynamics layer. The module is definitional, providing positivity and normalization lemmas that downstream modules apply to derive Boltzmann statistics and the second law.

claimThe Recognition Temperature $T_R$ parameterizes noise level with $T_R=0$ yielding only $J=0$ states and $T_R→∞$ yielding maximum disorder. The Gibbs weight is $w(x)=e^{-J(x)/T_R}$, the partition function is $Z=∑w(x)$, and recognition entropy is the Shannon entropy of the resulting Gibbs measure.

background

Recognition Science begins from the T=0 foundation in which all states minimize the universal cost J(x)=½(x+1/x)-1. The module imports the J-cost ledger from Cost and the self-similar forcing of φ from PhiForcing. It defines RecognitionSystem as the underlying state space and introduces gibbs_weight, partition_function, and recognition_entropy to extend the deterministic ledger into a statistical setting.

proof idea

This is a definition module with no complex proofs. It consists of direct definitions for gibbs_weight, partition_function, and recognition_entropy, followed by elementary lemmas establishing positivity, normalization to one, and non-negativity of the entropy measure.

why it matters in Recognition Science

This module supplies the foundational objects for the thermodynamics layer. It is imported by JCostBoltzmann to connect J-cost to biological Boltzmann statistics, by JCostEntropyAncestor to derive entropy from constrained J-minimization, by MaxEntFromCost to prove the maximum-entropy principle, by MemoryLedger for retention dynamics, and by SecondLaw to obtain the second law from first principles.

scope and limits

Does not derive the second law of thermodynamics.
Does not prove the maximum entropy principle.
Does not specify the explicit form of the J-cost function.
Does not address convergence of the partition function for infinite state spaces.

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