Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

QuantumMaxFlowMinCut

Abstract

QuantumMaxFlowMinCut supplies the width-three bridge max-flow proof.

Formulas retain the Lean parameter types and all hypotheses. HDiv.hDiv and HMod.hMod are displayed infix: on natural and integer carriers they mean the respective Lean integer division and remainder operations; on rational carriers division is field division. Coe.coe denotes the coercion determined by the displayed target type. Finite and dependent-pair constructors omit proof fields, which do not change their values. A dash in a match pattern is an anonymous wildcard. CoeFun.coe and CoeSort.coe retain coercions to functions and types. All dimensions use ℕ, all construction coefficients use ℚ, and max-flow uses ℂ.

Definition 1.1 (claim).

Formalization. D5/S3/Quantum/TensorNetworks/BridgeGraph/QuantumMaxFlowMinCut.claim (✓ std3).

Citation. Fulvio Gesmundo; Vladimir Lysikov; Vincent Steffan (2025). Quantum max-flow in the bridge graph. DOI: 10.1007/s00031-024-09863-2. URL: https://arxiv.org/abs/2212.09794v2.

Commentary.

Conjecture 1.4, page 6: “Let (a, b), (a′, b′) ∈ U_w ∪ V_w ∪ W_w. Then” followed by “QMaxFlow = QMinCut = min{a·b′, a′·b}” with the bridge-diagram arguments. Conjecture 3.14 repeats this on page 19. Conjecture 3.15, page 19: “Let (a, b), (a′, b′) ∈ U_3 ∪ V_3 ∪ W_3. Then” followed by “QMinCut = QMaxFlow = min{a′b, ab′}” at width three. The parameters are positive natural dimensions, and (a,b,c,d)=(a,b,a′,b′). The source region is exactly a ≤ b and aa+bb ≤ 3ab: its larger ratio endpoint is (3+√5)/2, as derived in the cited note. The claim asserts both equalities.

Theorem 1.2 (result).

Proof. Machine-checked in Lean as D5/S3/Quantum/TensorNetworks/BridgeGraph/QuantumMaxFlowMinCut.result (✓ std3). ∎

Resolves. Problems/gesmundo-lysikov-steffan-2022-bridge-graph-max-flow (proved) by D5/S3/Quantum/TensorNetworks/BridgeGraph/QuantumMaxFlowMinCut.result.

Source. Repository-derived.

Acknowledgement. Fulvio Gesmundo; Vladimir Lysikov; Vincent Steffan (2025). Quantum max-flow in the bridge graph. DOI: 10.1007/s00031-024-09863-2. URL: https://arxiv.org/abs/2212.09794v2.

Commentary.

The width-three quantum max-flow equals the quantum min-cut and the smaller outer cut for the positive ordered dimension pairs in the displayed cone. The proof combines a rational cyclic shift construction, short and long reservoir Schur complements, scalar extension to complex matrices, and castling deficit preservation followed by strong induction on b+d. Proposition 3.18 of the source derives Conjecture 1.4 at every w≥3 from this case; the implication to general width is supplied by the source.

References