Pith. sign in
module module high

IndisputableMonolith.Thermodynamics.JCostBoltzmann

show as:
view Lean formalization →

JCostBoltzmann certifies that the Gibbs weight at the ground state x=1 equals 1 and is maximal because J(1)=0. Researchers extending zero-temperature J-minimization to finite Recognition Temperature cite these weight properties. The results follow from direct substitution into the weight definition using the upstream J properties.

claimThe Gibbs weight $w$ satisfies $w(1)=1$, the maximum value, since $J(1)=0$.

background

The module belongs to the Thermodynamics domain and imports RecognitionThermodynamics. That parent module defines the statistical mechanics of Recognition Science by extending the T=0 cost minimization (J=0) to finite Recognition Temperature (TR) that parameterizes the strictness of J-minimization.

JCostBoltzmann introduces the J-cost Boltzmann weights and certifies their ground-state property as stated in the module doc comment.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds the JCostBoltzmannCert into the Recognition Thermodynamics framework. It supplies the concrete weight calculations required by the statistical mechanics definitions in the upstream RecognitionThermodynamics module.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)