Eq. (26) — for a forest F ⊆ E some basis state has energy ≥ Σ_{e∈F} w_e

Proved

QMaxCutBeyond.TwoQubit.eq_26

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

forestmax-cutp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-max-cut

Let $G=(V,E,w)$ have nonnegative weights and let $F\subseteq E$ be a forest. There is a computational basis state $|s\rangle$ , $s\in\{0,1\}^n$ , with

\langle s|H_G|s\rangle\;\ge\;f,\qquad f=\sum_{e\in F}w_e .

This is the first (classical) candidate state of eq. (27).

Formalization Note Only existence is stated; "we may efficiently compute" is not formalized.

Preamble

import Mathlib
import Definitions.Def_QMaxCutBeyond_TwoQubit_Setting

Formal statement

namespace QMaxCutBeyond.TwoQubit

/-- Eq. (26), p. 11 (existence part): if `F ⊆ E` is a forest, some computational basis state
`|s⟩` has `⟨s|H_G|s⟩ ≥ f = Σ_{e∈F} w_e`. -/
theorem eq_26 {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    (w : Sym2 (Fin n) → ℝ) (hw : ∀ e, 0 ≤ w e)
    (F : Finset (Sym2 (Fin n))) (hFG : F ⊆ G.edgeFinset)
    (hF : (SimpleGraph.fromEdgeSet (F : Set (Sym2 (Fin n)))).IsAcyclic) :
    ∃ s : Config n, ∑ e ∈ F, w e ≤ energy (hamiltonian G w) (basisState s) := by sorry

end QMaxCutBeyond.TwoQubit

Source

Anshu, Gosset & Morenz, Beyond product state approximations for a quantum analogue of Max Cut, arXiv:2003.14394v1, p. 11, eq. (26), proof of Theorem 3

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph