Rotation Preserves Adjacency

Abstract

Column rotations preserve all edges of P(13,3).

Theorem 1.1 (Adjacency under column rotation).

$$\forall r\in \mathrm{Fin}\left(13\right),\forall v\in V13,\forall w\in V13,\mathrm{Adj}\left(\mathrm{gp}\left(13,3\right),rotate13\left(r,v\right),rotate13\left(r,w\right)\right)\iff \mathrm{Adj}\left(\mathrm{gp}\left(13,3\right),v,w\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeFiniteRotation.rotate13_adj (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Arnav Krishnan (2026). A correction to the Zero Forcing Number of the Generalized Petersen Graphs P(n,3). DOI: 10.48550/arXiv.2607.19412. URL: https://arxiv.org/abs/2607.19412v1.

Commentary.

Subtracting the same column index preserves outer edges, inner step-three edges, and spokes.

References

• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeFiniteRotation.rotate13_adj
• Dependency: D5/S3/Combinatorics/GeneralizedPetersen/ParityRefutation
• Dependency: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeFiniteCore