Total edge-label extension
Abstract
A bijection from the actual edge set to a finite initial segment supplies positive successor labels on actual edges and zero elsewhere.
Definition 1.1 (Total edge-label extension).
Lean statement: D5/S3/Combinatorics/EdgeLabeling/CubicARGraphLabeling.edgeLabel
Formalization. D5/S3/Combinatorics/EdgeLabeling/CubicARGraphLabeling.edgeLabel (✓ std3).
Source. Repository-derived.
Commentary.
A bijection from the actual edge set to a finite initial segment supplies positive successor labels on actual edges and zero elsewhere.
Theorem 1.2 (From an edge equivalence to additive rigidity).
Lean statement: D5/S3/Combinatorics/EdgeLabeling/CubicARGraphLabeling.arGraph_of_edge_equiv
Proof. Machine-checked in Lean as D5/S3/Combinatorics/EdgeLabeling/CubicARGraphLabeling.arGraph_of_edge_equiv (✓ std3). ∎
Source. Repository-derived.
Commentary.
For a cubic graph, an edge equivalence with no additive collision at any vertex supplies an exact AR-labeling.