Finite set-form Menger certificates
Abstract
Finite vertex separators attain disjoint path certificates, with sharp weak duality for arbitrary walks.
Definition 1.1 (Separation by full walk support).
Formalization. D5/S3/Combinatorics/Graph/Walks/MengerCertificates.Separates (✓ std3).
Citation. Juan Pablo Traverso Gianini (2026). BrooksSubcubic, finite chordal elimination and set-form Menger: Lean sources. URL: https://github.com/Vilin97/lean-pool/tree/91c154506e3d08a1a25e4966c22c99212bf9df54/LeanPool/BrooksSubcubic.
Commentary.
Separates(G,A,B,X) means that every G-walk starting in A and ending in B has a vertex in X in its support. Support includes both endpoints. There is no restriction that X avoid A or B.
Theorem 1.2 (An attained certificate and universal walk weak duality).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/MengerCertificates.exists_separator_paths_and_weak_duality (✓ std3). ∎
Citation. Juan Pablo Traverso Gianini (2026). BrooksSubcubic, finite chordal elimination and set-form Menger: Lean sources. URL: https://github.com/Vilin97/lean-pool/tree/91c154506e3d08a1a25e4966c22c99212bf9df54/LeanPool/BrooksSubcubic.
Commentary.
For every vertex type V in any universe with Finite(V), every simple undirected graph G on V, and arbitrary finite vertex sets A and B, there is a finite separator X and an indexed family of exactly card(X) paths with initial vertices in A, final vertices in B, and pairwise disjoint full vertex supports. The same G, A and B satisfy the universal second clause: every finite separator Y bounds the size m of every pairwise vertex-disjoint family of A-to-B walks. The latter walks need not be paths.
In the displayed formula, Fin(n) is the index type with n elements, a and b are functions from this index type to V, and WalkFamily(G,a,b) is the dependent product of G.Walk(a(i),b(i)) over that index type. The product contains actual walks, including nil walks. IsPath is required only for the attained certificate. Disjointness quantifies over every vertex of each support, including endpoints.
Empty V, empty terminal sets, overlapping A and B, endpoint separators and zero-length paths remain in scope. In particular, the edge-free induction base uses nil paths at A intersect B. There is no connectedness, terminal-disjointness, distinct-terminal, nonadjacency or positive-length assumption. Directed, infinite-vertex, edge-disjoint and special two-terminal variants are outside this statement.
The proof is received from Juan Pablo Traverso Gianini’s jtraverso/menger-hamiltonian at immutable commit 35c5f684f9bfbd244bd0999ce725623ab571adb6. The source attributes its edge-induction proof to the second proof of Diestel, Graph Theory, Theorem 3.3.1 (Boehme, Goering, Harant). The private induction preserves the stronger terminal-clean Fam invariant because the splice consumes it; only the public output forgets those extra cleanliness clauses. Weak duality chooses a separator vertex on each walk and proves that disjointness makes this choice injective. This is known mathematics with source proof attribution.
The source copyright and full Apache license are retained in the Lean source and docs/reports/licenses/menger-hamiltonian-LICENSE.txt. Retire this port when this repository’s own pinned Mathlib supplies an equivalent entire finite set-form certificate and arbitrary-walk duality, after lawful migration of all consumers to direct applications.