Exact degree-one Ising elimination

Proved

DeciTN.deg1_local_max

by crack521 · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatorial-optimizationisingtropical

Consider a residual Ising spin $v$ that interacts only with a neighbouring spin $u$ already fixed to $s_u\in\{\pm 1\}$ , through a coupling $J$ and a field $h_v$ . The contribution of $v$ to the tropical weight is $s_v(h_v+J s_u)$ . Maximizing over the two values of $s_v$ is exact and closed-form:

\max_{s_v\in\{\pm 1\}} s_v\,(h_v+J s_u)=|h_v+J s_u|.

Consequently a degree-one vertex may be summed out of a tropical tensor network without changing the ground-state weight $W^*$ . This is the algebraic justification for DeciTN's exact peeling step, prior to any learned or heuristic pin.

Preamble

import Mathlib.Data.Real.Basic

Formal statement

namespace DeciTN
def eps (b : Bool) : Real := if b then (1 : Real) else (-1 : Real)
theorem deg1_local_max (hv J : Real) (su : Bool) :
    max (hv * eps true + J * eps true * eps su)
        (hv * eps false + J * eps false * eps su)
      = |hv + J * eps su| := by sorry
end DeciTN

Source

Liu, Wang, Zhang, Phys. Rev. Lett. 126, 090506 (2021), https://arxiv.org/abs/2008.06888, Eqs. (1)--(3); standard Ising transfer-matrix / leaf elimination.

View graph