Multigraph Contraction on Rational Cycles

Abstract

Nonloop contraction of an edge-indexed directed multigraph preserves rational signed-incidence cycles by surviving-coordinate restriction.

Let G be EssentialWordRealization.DirectedMultigraph V E. E is finite, while V may be arbitrary. Distinct edge IDs remain distinct even when their endpoints agree. No connectedness, simplicity, cyclic vertex order, or condition on bridges is imposed.

Definition 1.1 (The actual rational boundary).

Lean statement: D5/S3/Combinatorics/Graph/Incidence/MultigraphContraction.boundary

Formalization. D5/S3/Combinatorics/Graph/Incidence/MultigraphContraction.boundary (✓ std3).

Source. Repository-derived.

Commentary.

incidence G v f is the rational cast of the existing integer signedIncidence G.source G.target v f. Its sign is head minus tail. boundary G is multiplication by this matrix on E-indexed rational coefficients; CycleSpace G is its kernel. Every loop has zero boundary, including loops retained after contraction.

Definition 1.2 (Delete one edge and identify its endpoints).

Lean statement: D5/S3/Combinatorics/Graph/Incidence/MultigraphContraction.contract

Formalization. D5/S3/Combinatorics/Graph/Incidence/MultigraphContraction.contract (✓ std3).

Source. Repository-derived.

Commentary.

For e with source(e) different from target(e), Surviving e is the subtype of original edge IDs f different from e. ContractedVertex G e is the subtype of vertices different from target(e). vertexMap sends target(e) to source(e) and fixes every other vertex. contract G e h has the same existing DirectedMultigraph structure with source and target obtained by composing the original endpoint maps with vertexMap. All isolated vertices other than the removed endpoint persist. Parallel edges retain their IDs, and an edge joining the identified vertices becomes a loop rather than disappearing.

Theorem 1.3 (Endpoint fibers and the cycle equivalence).

$$\forall V:\mathrm{Type},\forall E:\mathrm{Type},[\mathrm{DecidableEq}\left(V\right)][\mathrm{DecidableEq}\left(E\right)][\mathrm{Fintype}\left(E\right)],\forall G:\mathrm{DirectedMultigraph}\left(V,E\right),\forall e:E,\forall h:\mathrm{source}\left(G,e\right)\ne \mathrm{target}\left(G,e\right),\forall w:V,\forall v:\mathrm{ContractedVertex}\left(G,e\right),\mathrm{vertexMap}\left(G,e,h,w\right)=v⟺w=\mathrm{val}\left(v\right)\vee w=\mathrm{target}\left(G,e\right)\wedge \mathrm{val}\left(v\right)=\mathrm{source}\left(G,e\right)\wedge \exists Phi:\mathrm{LinearEquiv}\left(\mathbb{Q},\mathrm{CycleSpace}\left(G\right),\mathrm{CycleSpace}\left(\mathrm{contract}\left(G,e,h\right)\right)\right),\forall z:\mathrm{CycleSpace}\left(G\right),\forall f:\mathrm{Surviving}\left(e\right),\mathrm{coeff}\left(\mathrm{apply}\left(Phi,z\right),f\right)=\mathrm{coeff}\left(z,\mathrm{val}\left(f\right)\right)\wedge \forall z:\mathrm{CycleSpace}\left(\mathrm{contract}\left(G,e,h\right)\right),\mathrm{coeff}\left(\mathrm{inverse}\left(Phi,z\right),e\right)=-\mathrm{residual}\left(G,e,\mathrm{val}\left(z\right),\mathrm{target}\left(G,e\right)\right)\wedge \forall z:\mathrm{CycleSpace}\left(\mathrm{contract}\left(G,e,h\right)\right),\forall f:\mathrm{Surviving}\left(e\right),\mathrm{coeff}\left(\mathrm{inverse}\left(Phi,z\right),\mathrm{val}\left(f\right)\right)=\mathrm{coeff}\left(z,f\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Incidence/MultigraphContraction.nonloop_contraction_cycle_equiv (✓ std3). ∎

Source. Repository-derived.

Commentary.

In the formula, coeff(z,f) means the underlying cycle coefficient z.val f; inverse(Phi,z) means Phi.symm z. LinearEquiv(Q,A,B) denotes a Q-linear equivalence. The fiber identity identifies precisely the two selected endpoints and no other vertices. The forward equivalence literally restricts surviving coordinates. Its inverse preserves each surviving coefficient and reconstructs the deleted coefficient as the negative original target-row residual. residual G e x v is the sum, over surviving IDs f, of incidence G v f times x(f).

The contracted boundary at a vertex other than the merged source is its original surviving-edge boundary. At the merged source it is the sum of the original source and target residuals. On a full cycle the removed edge contributes minus its coefficient at the source and plus its coefficient at the target, so restriction has zero contracted boundary. Conversely the target balance fixes the removed coefficient, and the merged balance then proves the source balance. These identities prove both inverse laws. The argument includes bridges, loops, parallel edges, empty surviving edge types, and arbitrary additional isolated vertices.

This supplies the cycle-space transport step in the common-contraction argument of the caller-supplied completed marked-four-loop proof, Section Half-edge rule and the homology calculation, proof.tex SHA256 7723959228b1445082f506550b1473155eb8210a27f8025e7a56d1a669663d82. The primary mathematical source is Kuperberg, arXiv:2608.11334v1, oddvas.tex. Cyclic-order signs, actual AS/IHX/CL relation maps, cohomology, coefficient duality, socket gluing, and the marked odd two-color four-loop Jacobi quotient require further arguments.

References

• Truth anchor: D5/S3/Combinatorics/Graph/Incidence/MultigraphContraction.boundary
• Truth anchor: D5/S3/Combinatorics/Graph/Incidence/MultigraphContraction.contract
• Truth anchor: D5/S3/Combinatorics/Graph/Incidence/MultigraphContraction.nonloop_contraction_cycle_equiv
• Dependency: D5/S3/ConceptDynamics/Coding/EssentialWordRealization
• Dependency: D5/S3/Fourier/CharacterSelection/SignedIncidenceTotalUnimodularity