jcost_at_zero
plain-language theorem explainer
The declaration shows that the J-cost landscape vanishes at zero order parameter for arbitrary temperature. Phase transition analyses in Recognition Science cite this as the reference point for the high-temperature disordered phase. The proof reduces to unfolding the landscape definition and applying ring simplification to confirm the identity.
Claim. For every real number $T$, the J-cost landscape evaluated at magnetization zero satisfies $L(0,T)=0$.
background
In Recognition Science, phase transitions arise from bifurcations in the J-cost landscape, where minima merge or split as parameters vary. The J-cost of a recognition event equals the J-cost of its state, per ObserverForcing.cost, and is induced by the comparator of a multiplicative recognizer via MultiplicativeRecognizerL4.cost. The module targets derivation of first-order, second-order, and critical-point transitions from these bifurcations, with T drawn from Breath1024 as fundamental periods and phase from EightTick as the 8-tick angles kπ/4.
proof idea
The proof is a term-mode reduction: it unfolds the definition of the J-cost landscape and invokes the ring tactic to discharge the resulting algebraic equality.
why it matters
This anchors the disordered phase in the J-cost bifurcation picture and feeds the downstream result jcost_positive_for_T_gt_1, which shows positivity for nonzero magnetization when T exceeds 1. It supports the module's derivation of phase transitions as information-theoretic bifurcations, consistent with the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.