Repeated augmented degrees force collisions
Abstract
Repeated augmented degrees force collisions
A resolving set would force distinct augmented selected degrees. Equal original bits give a collision between reverse incidences. With unequal original bits, cancel the shared midpoint by swapping the two indices in a row sum; a strict comparison at an outside index supplies two distinct incidences with equal four-bin counts. The cancellation excludes both distinguished indices.
Theorem 1.1 (resolving augmented injective).
Lean statement: D5/S3/Combinatorics/Graph/Walks/CompleteSubdivisionDegreeCollision.resolving_augmented_injective
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/CompleteSubdivisionDegreeCollision.resolving_augmented_injective (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Mohammad Farhan, Sandi Klavžar, Dorota Kuziak, Ismael G. Yero (2026). Multiset resolvability parameters in graphs: A survey with new results and open problems. URL: https://arxiv.org/pdf/2607.10311v1.
Commentary.
Resolution would make the selected midpoint degree plus original bit injective on all original vertices.
Theorem 1.2 (resolving rows injective).
Lean statement: D5/S3/Combinatorics/Graph/Walks/CompleteSubdivisionDegreeCollision.resolving_rows_injective
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Walks/CompleteSubdivisionDegreeCollision.resolving_rows_injective (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Mohammad Farhan, Sandi Klavžar, Dorota Kuziak, Ismael G. Yero (2026). Multiset resolvability parameters in graphs: A survey with new results and open problems. URL: https://arxiv.org/pdf/2607.10311v1.
Commentary.
Consequently a resolving selection matrix would have pairwise distinct row sums.