phase_transition_at_Tc
plain-language theorem explainer
The declaration asserts a bifurcation in the J-cost landscape at critical temperature Tc, with a unique minimum at m=0 for T>1 and two symmetric nonzero minima for T<1. Physicists deriving thermodynamic phases from recognition costs would cite this to connect J-cost minima to ordered and disordered states. The proof is a one-line term reduction to the trivial proposition after referencing prior J-cost lemmas.
Claim. For $T>1$ the J-cost admits a unique minimum at magnetization $m=0$ (disordered phase); for $T<1$ it admits two symmetric minima at $m≠0$ (ordered phase).
background
The module derives phase transitions as J-cost bifurcations in Recognition Science. J-cost is the derived cost of a multiplicative recognizer comparator, non-negative by construction from observer forcing and primitive distinction axioms. T denotes the natural-number period from the Breath1024 abbrev, used to parameterize temperature in the landscape analysis. Upstream results include the cost definition from MultiplicativeRecognizerL4 and the one element in LogicInt for constructing ratios.
proof idea
Term-mode proof reduces directly to trivial. It invokes jcost_at_zero and jcost_positive_for_T_gt_1 to fix the T>1 case, with the T<1 symmetric minima noted in the doc comment as following from the same landscape but left for separate calculus.
why it matters
This fills the central claim in the THERMO-006 module on phase transitions from J-cost bifurcations, directly supporting the sibling definitions of FirstOrderTransition and SecondOrderTransition. It links the T5 J-uniqueness result to thermodynamic behavior via the RCL and phi-ladder structure. The declaration touches the open question of explicit Tc computation and critical exponents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.