External Boundary in P(n,3)

Abstract

The external boundary consists of unselected vertices adjacent to the selected set.

Definition 1.1 (External vertex boundary).

$$\forall n\in \mathrm{Nat},\forall X\in \mathrm{Finset}\left(\mathrm{Bool}\times \mathrm{Fin}\left(n\right)\right),\mathrm{externalBoundary}\left(n,X\right)=\{v\in \mathrm{Bool}\times \mathrm{Fin}\left(n\right)|\left(\neg v\in X\right)\wedge \left(\exists u\in \mathrm{Bool}\times \mathrm{Fin}\left(n\right),u\in X\wedge \mathrm{Adj}\left(\mathrm{gp}\left(n,3\right),u,v\right)\right)\}$$

Formalization. D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeBoundary.externalBoundary (✓ 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.

A vertex is in the external boundary when it lies outside X and has a neighbor in X.

References

• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeBoundary.externalBoundary
• Dependency: D5/S3/Combinatorics/GeneralizedPetersen/ParityRefutation
• Dependency: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeShiftCore