Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Every Ten-Vertex Set Has Boundary at Least Eight

Abstract

Bounded gaps, the fourteen-column long-gap case, and deletion through an empty buffer give a uniform isoperimetric bound.

Theorem 1.1 (The boundary bound for bounded support gaps).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeTenBoundary.bounded_gap_boundary (✓ 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.

For a ten-vertex set with five through eight occupied columns and gaps at most seven, the score bound and the exact exceptional-support intervals give external boundary at least eight.

Theorem 1.2 (Remove one column inside an empty buffer).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeTenBoundary.buffered_deletion (✓ 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.

If no selected column lies within three cyclic steps of t, deletion of t preserves the selected-set cardinality and external-boundary cardinality. The map sending each column through succAbove t recovers the entire selected set, its external boundary, and its occupied columns.

Theorem 1.3 (The uniform ten-vertex boundary inequality).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeTenBoundary.p3_ten_boundary (✓ 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.

Every ten-vertex set in P(n,3), for n at least fourteen, has at least eight external neighbors. Occupied spoke mates handle at least nine columns; bounded gaps, the fourteen-column long-gap bound, and strong induction using buffered deletion handle the remaining supports.

References