Extend weighted LGV to directed multigraphs

[faabian]

Summary

• add a directed multigraph representation with a genuine type of arcs, retaining parallel arcs
• reduce multigraph paths to the standard incidence subdivision, where each arc becomes a distinct intermediate vertex
• repackage the existing weighted LGV proof to establish the full path-finite acyclic digraph statement from the TeX source

The subdivision preserves path weights by assigning the original weight to the first half-edge and weight one to the second. It also preserves vertex-disjointness: sharing an intermediate arc vertex forces sharing that arc's endpoints.

Validation

• targeted build of AlgebraicCombinatorics.Determinants.LGVMultiDigraph
• full project build (8,079 jobs)
• #print axioms LGV.MultiDigraph.lgv_weighted_multidigraph: only propext, Classical.choice, and Quot.sound; no sorryAx
• git diff --check