Integer and modular
flow reconfiguration

01 The finding

Fix an orientation of a finite loopless multigraph G. Integer flows satisfy conservation and 0 < |f(e)| < k; modular flows satisfy conservation with nonzero values in ℤ/kℤ. A legal step changes a flow along one simple cycle. Parallel edges are allowed.

Theorem. For k ∈ {4, 5}, reduction modulo k induces a bijection between the connected components of the integer and modular reconfiguration graphs.

This addresses the small-modulus cases of Problem 2.6 in Esperet et al., whose current version explicitly identifies k = 4 as unresolved. The general equivalence is also Conjecture A in Cranston et al. The arbitrary-modulus conjecture remains outside this result. Neither flow existence nor connectivity for every graph is asserted.

The midpoint construction

For a modular cycle move q → q + 2c, lift the auxiliary flow q + c to a bounded integer circulation h, allowing zeros. Then h − c and h + c are valid adjacent integer flows. Their nonzero residues exclude the only possible forbidden values: −k, 0 and k.

Different lifts of one modular flow can be joined by conformal cycle moves. Unit moves lift directly. Every nonzero scalar modulo 4 or 5 is represented by ±1 or ±2, which completes the path-lifting argument.

02 Verification and its limits

Formal proof

Lean 4.34.0-rc2 compilation and kernel replay passed. No sorry placeholders or custom axioms. Standard logical dependencies: propext, Classical.choice and Quot.sound.

Constructive checks

3,060 lifted modular moves; 4,092 ordered endpoint pairs in common fibers; 12,276 returned path steps checked independently, across 24 small graph/modulus cases.

Exploratory search

300 sampled graph/modulus cases, with matching component counts. Finite computation supports implementation checks; it does not prove the universal statement.

The Lean theorem assumes the standard conformal-cycle property of a finite circulation system. The graph-specific justification and the spanning-forest lifting argument are supplied in the full written proof, but are not instantiated from graph incidence definitions in Lean. This is an abstract formalization with a written graph application.

03 Research record

Produced by Codex in a research session initiated by Jack. Initial candidates in spectral graph theory were set aside after finding existing proofs. The work then focused on the explicit flow-reconfiguration problem, developed the midpoint argument, formalized the abstract theorem and checked an exact-integer implementation against independent enumeration.

Reported research effort: 35m 11s. This elapsed duration was supplied by Jack for the original research session. It excludes preparation of this report and website and is not an independently measured compute-cost estimate.

Targeted literature searches on 4 September 2026 found no prior proof. That search does not certify priority. This publication is a transparent research record, not an assertion of external endorsement.