jcostLandscape
plain-language theorem explainer
The jcostLandscape definition supplies the explicit functional form of the J-cost in terms of the order parameter m and temperature T. Researchers analyzing phase transitions within the Recognition Science framework would reference this expression when deriving bifurcation conditions. It is introduced as a direct algebraic definition modeled on the Landau expansion.
Claim. The J-cost landscape is the function $J(m,T)=(T-1)m^2 + m^4/4$, where $m$ is the order parameter and $T$ the temperature parameter.
background
In the Thermodynamics.PhaseTransitions module, phase transitions arise from bifurcations in the J-cost landscape as parameters vary. The J-cost is the cost function induced by recognition events, drawn from upstream results such as ObserverForcing.cost (the cost of a recognition event is its J-cost) and MultiplicativeRecognizerL4.cost (the cost function induced by a multiplicative recognizer). The module setting states that phase transitions occur when the J-cost landscape develops multiple local minima that merge or split.
proof idea
The definition is a direct algebraic expression providing the Landau-like form for the J-cost.
why it matters
This definition serves as the foundation for the subsequent theorems jcost_at_zero and jcost_positive_for_T_gt_1 in the same module, which establish that m=0 is the unique minimum for T>1. It connects to the Recognition Science mechanism where phase transitions are J-cost bifurcations, aligning with the T5 J-uniqueness landmark and the forcing chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.