jcost_positive_for_T_gt_1
plain-language theorem explainer
The theorem shows that for reduced temperature T exceeding 1 and nonzero order parameter m, the J-cost landscape J(m,T) is strictly positive. This pins m=0 as the unique global minimum, corresponding to the disordered phase. Physicists modeling phase transitions through Recognition Science J-cost bifurcations would cite the result to fix the high-temperature regime. The proof is a short tactic sequence that unfolds the landscape, applies square positivity and linear arithmetic to reach a contradiction-free inequality.
Claim. For real numbers $m$ and $T$ satisfying $T>1$ and $m≠0$, the J-cost landscape obeys $J(m,T)>0$.
background
The J-cost landscape is the effective potential whose local minima locate the equilibrium order parameter. In this module phase transitions are realized as bifurcations of that landscape: above the critical temperature the sole minimum sits at m=0 (disordered phase), while below it two symmetric minima appear at nonzero m (ordered phase). The module documentation states that these bifurcations constitute the Recognition Science mechanism for first- and second-order transitions.
proof idea
The proof unfolds jcostLandscape to the explicit quartic (T-1)m² + m⁴/4. It invokes sq_pos_of_ne_zero on the hypothesis m≠0 to obtain m²>0, applies linarith to confirm T-1>0, multiplies the two positive quantities, records that m⁴/4 is nonnegative by the positivity tactic, and concludes the sum exceeds zero by linarith.
why it matters
The declaration supplies the high-temperature half of the J-cost bifurcation argument inside THERMO-006. It pairs with the sibling jcost_at_zero to establish that m=0 is the unique minimum precisely when T>1, thereby locating the critical point at T=1. The result implements the disordered-phase statement quoted in the module doc-comment and anchors the information-theoretic treatment of phase transitions as J-cost bifurcations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.