Bounded Gap Roots

Abstract

The mask recurrence accepts the stated rooted bounded-gap families.

Theorem 1.1 (5 gaps with root 1 to 7).

$$\forall q\in \mathrm{Nat},\left(1\le q\wedge q\le 7\right)\Rightarrow \mathrm{maskCheck}\left(5,4,q,[q]\right)=\mathrm{true}$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeGapData56A.roots5 (✓ 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 5 positive gaps, maskCheck accepts the root prefix [q] with 4 remaining entries and maximum gap q, for q from 1 through 7.

Theorem 1.2 (6 gaps with root 1 to 5).

$$\forall q\in \mathrm{Nat},\left(1\le q\wedge q\le 5\right)\Rightarrow \mathrm{maskCheck}\left(6,5,q,[q]\right)=\mathrm{true}$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeGapData56A.roots6 (✓ 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 6 positive gaps, maskCheck accepts the root prefix [q] with 5 remaining entries and maximum gap q, for q from 1 through 5.

References

• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeGapData56A.roots5
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeGapData56A.roots6
• Dependency: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeGapCompute