module module moderate

`IndisputableMonolith.Thermodynamics.PhaseTransitions`

This module defines the J-cost as a function of order parameter m and temperature T, together with the associated landscape, first-order and second-order transition mechanisms, and critical-point ratios. RS statistical mechanicians cite it when extending the T=0 J-minimization foundation to finite-temperature phase structure. The module consists of a collection of definitions and short lemmas that build directly on the imported Cost and PhiForcing primitives.

claimThe central object is the J-cost landscape $J(m,T)$ for order parameter $m$ and temperature $T$, with a phase transition located at critical temperature $T_c$, first-order transition mechanism, second-order transition mechanism, and critical ratios governing spontaneous symmetry breaking.

background

Recognition Science begins from the absolute minimization of the universal cost functional $J(x) = rac12(x + 1/x) - 1$ at $T=0$. The present module extends this cost to finite temperature by introducing an order parameter $m$ and studies the resulting phase structure. It imports the RS time quantum $ au_0 = 1$ tick from Constants, empirical calibration quarantine from ExternalAnchors, the J-cost definition from Cost, and the self-similar forcing of $\phi$ from PhiForcing.

proof idea

This is a definition module, no proofs. It introduces the J-cost landscape, positivity statements for $T>1$, the location of the transition at $T_c$, the two transition mechanisms, the critical-point object, and example order-parameter constructions, all as direct definitions or one-line wrappers around the imported J and $\phi$ primitives.

why it matters in Recognition Science

The module supplies the finite-temperature phase-transition layer required by the parent Thermodynamics module, which develops the full statistical mechanics of Recognition Science from the T=0 J-minimization foundation. It thereby completes the bridge from the phi-forced discrete ledger to observable thermodynamic behavior.

scope and limits

Does not derive an explicit closed-form expression for $J(m,T)$ from the RCL.
Does not identify $m$ with any particular physical order parameter such as magnetization.
Does not compute numerical values of $T_c$ or critical ratios from external data.
Does not address dynamical evolution across the transition.

used by (1)

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

IndisputableMonolith.Thermodynamics module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.ExternalAnchors module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.PhiForcing module_import

declarations in this module (20)

def jcostLandscape L47
theorem jcost_at_zero L51
theorem jcost_positive_for_T_gt_1 L57
theorem phase_transition_at_Tc L69
structure FirstOrderTransition L83
theorem first_order_mechanism L93
structure SecondOrderTransition L105
theorem second_order_mechanism L114
structure CriticalPoint L126
theorem critical_ratios L135
def orderParameterExamples L147
theorem spontaneous_symmetry_breaking L165
def ssbMechanism L171
structure MetastableState L182
def nucleationRate L192
structure QuantumPhaseTransition L203
def qptExamples L212
structure TopologicalTransition L226
def summary L241
structure PhaseTransitionFalsifier L255