Binary Simple Graph Cycle Spaces
Abstract
Simple cycles determine binary edge labels, all vertex lifts, and every fundamental cycle basis.
Definition 1.1 (Endpoint evaluation).
Lean statement: D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.endpointCharacters
Formalization. D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.endpointCharacters (✓ std3).
Source. Repository-derived.
Commentary.
Let G be a simple graph on a vertex type V. Its edge carrier E is the subtype of actual unordered edges in Sym2 V. The coefficient field F is ZMod 2. For each edge {u,v}, the endpoint character sends a vertex function x to x(u)+x(v). Addition is symmetric, so this functional is independent of the order of the two endpoints.
Definition 1.2 (The binary differential).
Lean statement: D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.edgeDifferential
Formalization. D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.edgeDifferential (✓ std3).
Source. Repository-derived.
Commentary.
The linear map delta from V-to-F functions to E-to-F functions evaluates all endpoint characters simultaneously. Thus delta(x)({u,v})=x(u)+x(v).
Definition 1.3 (The independently generated cycle space).
Lean statement: D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.simpleCycleSpace
Formalization. D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.simpleCycleSpace (✓ std3).
Source. Repository-derived.
Commentary.
With decidable vertex equality, S is the F-linear span of the functions that are one on the edge list of an actual simple closed G-walk and zero elsewhere. The generators range over every base vertex and every walk satisfying IsCycle. This definition does not use the kernel of an incidence map.
Definition 1.4 (A sum with traversal multiplicity).
Lean statement: D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.walkParity
Formalization. D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.walkParity (✓ std3).
Source. Repository-derived.
Commentary.
For any edge labeling y and any walk p, walkParity(y,p) is the sum of y over the full unordered-edge list of p. Each occurrence contributes once. The summand extends y by zero outside E; every entry of a G-walk lies in E. In particular, traversing one edge twice contributes zero in F.
Theorem 1.5 (Closed walks are generated by simple cycles).
Proof. Machine-checked in Lean as D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.closed_walk_mod_two_mem_simple_cycle_span (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every vertex type V with decidable equality, every simple graph G, every vertex v and every closed walk p from v to v, its vector nu(p) belongs to S. At an edge e, nu(p)(e) is the number of occurrences of e in p.edges, reduced modulo two. Neither finiteness of V nor connectedness is required. The statement places no global nonemptiness condition on V.
Induction on the walk shows that nu(p)-nu(p.bypass) belongs to S. When a repeated vertex is removed, the retained path prefix together with the first edge is either a simple cycle or a single edge traversed in both directions. The cycle contributes its indicator; the backtrack contributes zero. A closed bypass path is empty.
Theorem 1.6 (Lifts, fundamental bases, and independent fair labels).
Proof. Machine-checked in Lean as D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.finite_graph_cycle_space (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Frank Harary (1953). On the notion of balance of a signed graph. DOI: 10.1307/mmj/1028989917.
Commentary.
The binary cycle criterion has the classical signed-balance formulation: give an edge sign +1 for label zero and -1 for label one. Zero cycle parity means that every cycle has positive sign product; a vertex lift expresses each edge sign as the product of its endpoint signs. The literature acknowledgement concerns this classical core. The arbitrary-anchor bijections, constructions for every supplied forest, counts, probabilities, and this Lean proof are not attributed as a bundle to the cited paper. No full 2-adic classification is asserted.
Let V be any finite type with decidable equality and let G be any simple graph on V. Finite enumerations of E and the actual connected-component quotient are supplied. Set n=card(V), m=card(E), and c=card(components). R is the kernel of the linear-combination map of endpoint characters. Then S=R and c is at most n. For every y:E-to-F, delta(x)=y has a solution if and only if walkParity(y,p)=0 for every base vertex v and every simple closed walk p at v.
For every realizable y and every section o choosing a vertex o(K) in each actual component K, evaluation x maps to the function K maps to x(o(K)) is a bijection from the fiber over y to the functions from components to F. Equivalently, every independently specified anchor vector has exactly one lift. Every such fiber has 2^c elements, and the image of delta has 2^(n-c) elements.
A spanning forest exists. For every supplied graph T on V with T<=G, T acyclic and T.Reachable=G.Reachable, let D be the subtype of E consisting of edges outside T. There is a family C indexed by D of actual simple closed G-walks. For each d, there are endpoints a,b and a G-edge from a to b representing d such that C(d) is that edge followed by the unique T-path from b to a, mapped into G. Every T-path with those endpoints equals the selected path.
For all d,e in D, the indicator of C(d) at e is one exactly when e=d. There is a basis of S indexed by D whose vector at d, at every actual edge e of G, is one exactly when e occurs in C(d). Write t=card(T.edges) and b=card(D). Then t+c=n, n<=m+c, b=m-t=m+c-n in the natural numbers, and the integer cast of b is the integer expression m-n+c. The F-dimension of S is b. In particular, subtraction in m+c-n is performed only after the displayed bound.
Equip F with any measurable structure in which singletons are measurable; on this finite field every set is then measurable. Each uniform law on F assigns real mass 1/2 to each bit. The product of these laws indexed by the actual unordered edges equals the uniform law on all E-to-F functions. Under this joint product law, the real probability of the image of delta is 2^(-b), with the exponent interpreted in the integers, equivalently the reciprocal of 2^b. The integer identity for b also gives 2^(-(m-n+c)).
The construction chooses a spanning forest and paths from component roots. Vanishing on simple cycles extends to all closed walks by the decomposition above; comparing two root walks across an edge gives the endpoint equation. Along walks, equal differentials imply that the difference of two lifts is componentwise constant. Adjusting those constants gives any prescribed anchors and the fiber bijection. Coordinate pairing and double orthogonality identify S with R.
Component vertices and component edges are put in bijection with the corresponding disjoint unions, so the tree edge-count formula sums to t+c=n. Fundamental cycles give the unit chord coordinates. Subtracting the corresponding linear combination leaves a vector supported on the forest. Acyclicity makes the forest simple-cycle span zero; the differential criterion on that forest and orthogonality force the residual vector to vanish. Thus chord restriction is an isomorphism and the stated family is a basis. Finally, the uniform event formula divides the image count by 2^m.
All quantifiers include empty vertex types, disconnected graphs, isolated vertices, and forests. When V is empty, both function spaces have one element and c=b=0. When E is empty, c=n, the image has one element, and its fiber has 2^n elements. Each isolated component retains its own independent anchor.
References
- Truth anchor:
D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.closed_walk_mod_two_mem_simple_cycle_span - Truth anchor:
D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.edgeDifferential - Truth anchor:
D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.endpointCharacters - Truth anchor:
D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.finite_graph_cycle_space - Truth anchor:
D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.simpleCycleSpace - Truth anchor:
D5/S3/Fourier/CharacterSelection/SimpleGraphCycleSpace.walkParity - Dependency: D5/S3/Fourier/CharacterSelection/BinaryCharacterCodeDuality