RecognitionSystem
plain-language theorem explainer
The recognition system structure packages a positive real recognition temperature TR that sets the noise level for J-cost minimization at finite temperature. Researchers extending zero-temperature RS dynamics to statistical mechanics would cite it when constructing Gibbs measures or proving free-energy monotonicity. The definition is a direct structure declaration with a positivity field on TR and a derived reciprocal beta field.
Claim. A recognition system consists of a positive real number $T_R > 0$ together with the derived inverse temperature $beta = 1/T_R$.
background
Recognition Thermodynamics extends the zero-temperature J-cost minimization of Recognition Science to finite temperature. The J-function J(x) = (x + x^{-1})/2 - 1 supplies the cost, while recognition temperature TR controls the strictness of minimization: TR = 0 recovers deterministic behavior and TR to infinity yields maximum disorder. Beta is introduced as the thermodynamic inverse temperature 1/TR. The module draws on upstream structures for J-cost from PhiForcingDerived and Born-rule probabilities from QuantumLedger.
proof idea
The structure is declared directly with the positivity hypothesis TR_pos. The beta field is introduced by the one-line definition 1/TR. Positivity of beta is obtained by applying the division rule for positive reals to the constant 1 and the hypothesis TR_pos.
why it matters
This structure is the base object for all thermodynamic constructions in the module, feeding directly into fault-tolerance definitions, coarse-graining monotonicity of free energy, the recognition H-theorem, and the arrow of time defined by decreasing free energy. It supplies the finite-temperature extension of the T0-T8 forcing chain, where the eight-tick octave sets the fundamental time unit and the phi-ladder discretizes states. Downstream results quote the variational identity relating free energy to Kullback-Leibler divergence from the Gibbs measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.