Absolute value is a tropical (max-plus) sum

Proved

DeciTN.abs_eq_tropical_max

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

combinatorial-optimizationisingtropical

For every real number $a$ , the larger of $a$ and $-a$ equals the absolute value $|a|$ . In the max-plus (tropical) semiring this is the statement that the tropical sum of a literal and its additive inverse recovers the tropical norm. It is the one-site identity behind exact degree-one elimination of an Ising spin: maximizing $s(h+J s_u)$ over $s\in\{\pm 1\}$ yields $|h+J s_u|$ .

\max(a,-a)=|a|.

This lemma is the first certified building block of DeciTN's exact residual reductions.

Preamble

import Mathlib.Data.Real.Basic

Formal statement

namespace DeciTN
theorem abs_eq_tropical_max (a : Real) : max a (-a) = |a| := by sorry
end DeciTN

Source

Liu, Wang, Zhang, Tropical Tensor Network for Ground States of Spin Glasses, Phys. Rev. Lett. 126, 090506 (2021), https://arxiv.org/abs/2008.06888; the max-plus arithmetic

x\oplus y=\max(x,y)

View graph