Exact list-edge labelings of bipartite multigraphs: uncrossing, nested minimizers, and a 2-factor criterion for equality

Let R = (X, Y; E) be a finite bipartite multigraph, and give every left vertex x a list of exactly deg(x) labels. A labeling of the edges is admissible if each vertex x ∈ X uses every label of its list exactly once and the labels at each right vertex are distinct. We show that replacing the supports A, B ⊆ X of two labels by A ∪ B and A ∩ B never increases the number of admissible labelings. Iterating this uncrossing yields a canonical nested minimizer that depends only on the left-degree sequence. In particular, if R is left-k-regular, then every exact k-list assignment admits at least cₖ(R) admissible labelings, where cₖ(R) is the number of proper k-edge-colorings of R. Applied to Kₙ,ₙ, this shows that every presentation of a purely parallel rank-n matroid as n disjoint bases has at least Lₙ ordered solutions to Rota’s basis problem, where Lₙ is the number of Latin squares of order n. Via a crown-graph correspondence, it also gives a new proof of Smetaniuk’s inequality Lₙ₊₁ ≥ (n + 1)!Lₙ. We then study equality. An exact formula for the loss caused by a single uncrossing, a laminar-forest description of the systems that remain, and a reduction to two terminal shapes show the following. For each k, the conjecture that every equality case on a connected k-regular graph has k − 1 labels common to all lists is equivalent to a three-part 2-factor property TFₖ: for every partition of X into three nonempty parts, some 2-factor has a cycle meeting all three. TF₂ is immediate. For k = 3, we reduce TF₃ to a prescribed-pair property of cubic bipartite braces and deduce it for planar graphs. The inequality, the nested minimizer, the surplus formula, and the Latin-square growth step are formalized in Lean 4.