Weighted Vertex Products and Closed Walks

Abstract

On a connected graph over a commutative group with surjective squaring, symmetric edge weights factor into vertex products exactly when every even closed walk balances. For a bipartite graph over any commutative group, every specified spanning tree gives equivalent simple-cycle and fundamental-cycle tests.

Let V be an arbitrary vertex type, A a commutative group, G a simple graph, and w:Sym2(V)->A symmetric edge weights. For a walk p, alpha(w,p) is List.alternatingProd of its edge-weight list. Every occurrence is retained, including repeated edges and immediate backtracks. The empty walk has value one. Sol(w,G) means that there is b:V->A with b(u)b(v)=w({u,v}) on every edge.

Theorem 1.1 (Even Closed Walks Are the Complete Obstruction).

$$\forall V\in \mathrm{Type},\forall A\in \mathrm{Type},(\mathrm{CommGroup}\left(A\right))\Rightarrow (\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall w\in \mathrm{Function}\left(Sym2\left(V\right),A\right),(\mathrm{SurjectiveSquare}\left(A\right))\Rightarrow ((\mathrm{Connected}\left(G\right))\Rightarrow ((\mathrm{Sol}\left(w,G\right))\iff (\forall u\in V,\forall p\in \mathrm{Walk}\left(G,u,u\right),(\mathrm{Even}\left(\mathrm{length}\left(p\right)\right))\Rightarrow (\mathrm{alpha}\left(w,p\right)=1)))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/WeightedVertexProducts.vertex_products_iff_even_closed_walks (✓ std3). ∎

Source. Repository-derived.

Commentary.

The square map a->aa is assumed surjective and G is connected. Along a walk from u to v, a vertex factorization gives alpha(p)=b(u)b(v)^(-(-1)^length(p)). At a root, either every closed walk is even, and its value can be set to one, or an odd closed walk fixes the square of the root value. Concatenating two odd loops shows that this constraint is independent of the chosen loop. Comparing two root-to-vertex walks through their closed concatenation proves path compatibility. Transporting the root value then constructs all vertex factors.

Theorem 1.2 (Simple Cycles and Every Spanning Tree).

$$\forall V\in \mathrm{Type},\forall A\in \mathrm{Type},(\mathrm{CommGroup}\left(A\right))\Rightarrow (\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall w\in \mathrm{Function}\left(Sym2\left(V\right),A\right),(\mathrm{Colorable}\left(G,2\right))\Rightarrow (\forall T\in \mathrm{SimpleGraph}\left(V\right),(\mathrm{SubgraphOnSameVertices}\left(T,G\right))\Rightarrow ((\mathrm{IsTree}\left(T\right))\Rightarrow (((\mathrm{Sol}\left(w,G\right))\iff (\mathrm{AllSimpleCyclesBalance}\left(w,G\right)))\wedge ((\mathrm{Sol}\left(w,G\right))\iff (\mathrm{AllFundamentalCyclesBalance}\left(w,G,T\right)))))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/WeightedVertexProducts.bipartite_cycle_tree_criteria (✓ std3). ∎

Source. Repository-derived.

Commentary.

No square-root hypothesis is needed here. The graph is bipartite and T is any specified spanning tree on the same vertices. Tree paths construct vertex factors. A non-tree edge together with the tree path returning to its initial vertex is a fundamental simple cycle. Bipartiteness makes that returning path odd. Balancing its cycle is exactly the missing edge equation. Thus checking all simple cycles, or only the fundamental cycles of any T, is equivalent to Sol(w,G). Connectedness is carried by T.IsTree; no finiteness hypothesis is imposed.

For finite characteristic-two fields, the square-root premise follows from the bijective Frobenius map. In the stabilizer model, n is any odd integer at least three and q is at least two. The replica character is t:Fin(q-1)->ZMod(n); its readout on a party c is t(c) for cFin(q) is allowed, and x(u) is that readout at col(u). The field is the intermediate field generated by a primitive nth root zeta inside the algebraic closure of F2. Primitive-root power injection identifies the nonempty character fibers with the lambda fibers. The zero character gives the empty support graph. Stabilizer edge weights are lambda(u)+lambda(v) on the support where this sum is nonzero. Applying the graph criterion to these units requires the exact character-fiber support correspondence. For the fiber mask A(u,v)=0 when the character readouts agree and A(u,v)=Gamma(u,v) otherwise, a solution gives M=B(A mapped into F)B with B=diag(beta). Diagonal invertibility and rank_map_algebraMap at its original QuantumMaxFlowBound owner give rank_F(M)=rank_F2(A). This deduction includes empty principal restrictions. Component rank additivity and any converse to rank equality require separate results.

References

• Truth anchor: D5/S3/Combinatorics/Graph/Walks/WeightedVertexProducts.bipartite_cycle_tree_criteria
• Truth anchor: D5/S3/Combinatorics/Graph/Walks/WeightedVertexProducts.vertex_products_iff_even_closed_walks