Counted edges and overlap conjugacy

Abstract

A nonnegative matrix records numbered parallel edges. Lexicographic fiber ranks split and reassemble each product edge.

Theorem 1.1 (Recover both numbered half-edges).

$$\forall n\in Nat,m\in Nat,U\in \mathrm{CountMat}\left(n,m\right),V\in \mathrm{CountMat}\left(m,n\right),a\in \mathrm{Edge}\left(U\right),b\in \mathrm{Edge}\left(V\right),h\in \mathrm{target}\left(a\right)=\mathrm{source}\left(b\right),\mathrm{split}\left(U,V,\mathrm{join}\left(U,V,a,b,h\right)\right)=\mathrm{pair}\left(a,b\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/CountedMatrixOverlap.split_join (✓ std3). ∎

Source. Repository-derived.

Commentary.

The product edge number is the lexicographic rank of its middle vertex and both factor-edge numbers. The proved finite-fiber count supplies the increasing rank equivalence. Splitting after joining therefore recovers the full pair, including parallel-edge identity.

Theorem 1.2 (Recover the original matrix edge).

$$\forall n\in Nat,m\in Nat,U\in \mathrm{CountMat}\left(n,m\right),V\in \mathrm{CountMat}\left(m,n\right),a\in \mathrm{Edge}\left(\mathrm{product}\left(U,V\right)\right),\mathrm{join}\left(U,V,\mathrm{first}\left(\mathrm{split}\left(U,V,a\right)\right),\mathrm{second}\left(\mathrm{split}\left(U,V,a\right)\right)\right)=a$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/CountedMatrixOverlap.join_split (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two split half-edges have matching middle endpoints; their equality proof is implicit in the displayed join. The inverse ordered finite-fiber equivalence recovers the original numbered edge. The outside endpoints are unchanged in both constructions.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/CountedMatrixOverlap.join_split
• Truth anchor: D5/S3/ConceptDynamics/Coding/CountedMatrixOverlap.split_join
• Dependency: D5/S3/ConceptDynamics/Coding/BipartiteOverlapConjugacy