Requests, Collisions, and Cyclic Gap Scores

Abstract

The external boundary is counted by requests and collisions, whose total is dominated by ten cyclic layer scores.

Definition 1.1 (Forward requests).

$$\forall n\in \mathrm{Nat},\forall X\in \mathrm{Finset}\left(\mathrm{Bool}\times \mathrm{Fin}\left(n\right)\right),0<n\Rightarrow \mathrm{positiveRequests}\left(n,X\right)=\left\{\mathrm{positiveShift}\left(n,v\right)\mid v\in X\right\}$$

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

Each selected vertex requests its forward neighbor in the same layer.

Definition 1.2 (Backward requests).

$$\forall n\in \mathrm{Nat},\forall X\in \mathrm{Finset}\left(\mathrm{Bool}\times \mathrm{Fin}\left(n\right)\right),0<n\Rightarrow \mathrm{negativeRequests}\left(n,X\right)=\left\{\mathrm{negativeShift}\left(n,v\right)\mid v\in X\right\}$$

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

Each selected vertex requests its backward neighbor in the same layer.

Definition 1.3 (Requests landing in occupied columns).

$$\forall n\in \mathrm{Nat},\forall X\in \mathrm{Finset}\left(\mathrm{Bool}\times \mathrm{Fin}\left(n\right)\right),0<n\Rightarrow I\left(n,X\right)=\mathrm{card}\left(\mathrm{inter}\left(\mathrm{positiveRequests}\left(n,X\right),\mathrm{occupiedVertices}\left(X\right)\right)\right)+\mathrm{card}\left(\mathrm{inter}\left(\mathrm{negativeRequests}\left(n,X\right),\mathrm{occupiedVertices}\left(X\right)\right)\right)$$

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

Count requests into occupied columns separately in the two directions, retaining multiplicity when both directions reach the same vertex.

Definition 1.4 (Two requests at an empty column).

$$\forall n\in \mathrm{Nat},\forall X\in \mathrm{Finset}\left(\mathrm{Bool}\times \mathrm{Fin}\left(n\right)\right),0<n\Rightarrow K\left(n,X\right)=\mathrm{card}\left(\mathrm{inter}\left((\mathrm{positiveRequests}\left(n,X\right)\setminus \mathrm{occupiedVertices}\left(X\right)),(\mathrm{negativeRequests}\left(n,X\right)\setminus \mathrm{occupiedVertices}\left(X\right))\right)\right)$$

Formalization. D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.K (✓ 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 collision is a vertex in an unoccupied column requested from both directions.

Theorem 1.5 (Boundary, requests, and collisions).

$$\forall n\in \mathrm{Nat},\forall X\in \mathrm{Finset}\left(\mathrm{Bool}\times \mathrm{Fin}\left(n\right)\right),14\le n\Rightarrow \mathrm{card}\left(\mathrm{externalBoundary}\left(n,X\right)\right)+I\left(n,X\right)+K\left(n,X\right)=2\cdot \mathrm{card}\left(\mathrm{columns}\left(X\right)\right)+\mathrm{card}\left(X\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.boundary_request_identity (✓ 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 every selected set at circumference at least fourteen, the boundary size plus the occupied requests and empty collisions equals twice the number of occupied columns plus the set size.

Definition 1.6 (Increasing enumeration of the support).

$$\forall n\in \mathrm{Nat},\forall C\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\mathrm{sortedColumn}\left(C\right)=\mathrm{orderEmbOfFin}\left(C\right)$$

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

The support is enumerated in increasing order by Fin of its cardinality.

Definition 1.7 (The terminal circumference).

$$\forall n\in \mathrm{Nat},\forall C\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\forall j\in \mathrm{Nat},\mathrm{extendedColumn}\left(C,j\right)=\mathrm{if}\left(j<\mathrm{card}\left(C\right),\mathrm{val}\left(\mathrm{sortedColumn}\left(C\right)[j]\right),n\right)$$

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

At an index below the support size, take the corresponding sorted column value; at every later index, take n.

Definition 1.8 (Positive cyclic differences).

$$\forall n\in \mathrm{Nat},\forall C\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\forall i\in \mathrm{Fin}\left(\mathrm{card}\left(C\right)\right),\mathrm{gapWord}\left(C,i\right)=\mathrm{extendedColumn}\left(C,\mathrm{val}\left(i\right)+1\right)-\mathrm{extendedColumn}\left(C,\mathrm{val}\left(i\right)\right)+\mathrm{if}\left(\mathrm{val}\left(i\right)+1=\mathrm{card}\left(C\right),\mathrm{extendedColumn}\left(C,0\right),0\right)$$

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

Consecutive sorted columns give the ordinary gaps; the final entry includes the wrap from the last occupied column to the first.

Definition 1.9 (One outer-gap contribution).

$$\forall h\in \mathrm{Nat},\mathrm{phi}\left(h\right)=\mathrm{if}\left(h=1,2,\mathrm{if}\left(h=2,1,0\right)\right)$$

Formalization. D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.phi (✓ 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 gap of one contributes two, a gap of two contributes one, and every other gap contributes zero.

Definition 1.10 (Cyclic displacement of an index).

$$\forall c\in \mathrm{Nat},\forall i\in \mathrm{Fin}\left(c\right),\forall j\in \mathrm{Nat},\mathrm{val}\left(\mathrm{cyclicIndex}\left(i,j\right)\right)=\left(\mathrm{val}\left(i\right)+j\right)\mathrm{mod}c$$

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

Add j to the index and reduce modulo the word length.

Definition 1.11 (Forward cyclic prefix sum).

$$\forall c\in \mathrm{Nat},\forall h\in \mathrm{Fin}\left(c\right)\to \mathrm{Nat},\forall i\in \mathrm{Fin}\left(c\right),\forall k\in \mathrm{Nat},\mathrm{positivePrefix}\left(h,i,k\right)=\sum _{j\in \mathrm{range}\left(k\right)}h\left(\mathrm{cyclicIndex}\left(i,j\right)\right)$$

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

Sum k gaps starting with the gap at i and proceeding forward.

Definition 1.12 (Backward cyclic prefix sum).

$$\forall c\in \mathrm{Nat},\forall h\in \mathrm{Fin}\left(c\right)\to \mathrm{Nat},\forall i\in \mathrm{Fin}\left(c\right),\forall k\in \mathrm{Nat},\mathrm{negativePrefix}\left(h,i,k\right)=\sum _{j\in \mathrm{range}\left(k\right)}h\left(\mathrm{cyclicIndex}\left(i,c-\left(j+1\right)\right)\right)$$

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

The reverse scan uses the displacement c - (j + 1). This subtraction is in the natural numbers and is truncated at zero.

Definition 1.13 (Score of a directional prefix scan).

$$\forall c\in \mathrm{Nat},\forall h\in \mathrm{Fin}\left(c\right)\to \mathrm{Nat},\forall i\in \mathrm{Fin}\left(c\right),\forall sums\in \left(\mathrm{Fin}\left(c\right)\to \mathrm{Nat}\right)\to \left(\mathrm{Fin}\left(c\right)\to \left(\mathrm{Nat}\to \mathrm{Nat}\right)\right),\mathrm{prefixScore}\left(h,i,sums\right)=\mathrm{if}\left(\exists k\in \mathrm{Nat},1\le k\wedge \left(k\le c\wedge \mathrm{sums}\left(h,i,k\right)=3\right),2,\mathrm{if}\left(\exists k\in \mathrm{Nat},1\le k\wedge \left(k\le c\wedge \mathrm{sums}\left(h,i,k\right)=6\right),1,0\right)\right)$$

Formalization. D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.prefixScore (✓ 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 prefix of one through c gaps summing to three scores two. If none exists, a prefix summing to six scores one; otherwise the score is zero.

Definition 1.14 (The outer layer slot).

$$\forall c\in \mathrm{Nat},\forall h\in \mathrm{Fin}\left(c\right)\to \mathrm{Nat},\forall i\in \mathrm{Fin}\left(c\right),A\left(h,i\right)=\mathrm{phi}\left(h\left(\mathrm{cyclicIndex}\left(i,c-1\right)\right)\right)+\mathrm{phi}\left(h\left(i\right)\right)$$

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

The outer slot adds the contributions from the gaps immediately before and after its column.

Definition 1.15 (The inner layer slot).

$$\forall c\in \mathrm{Nat},\forall h\in \mathrm{Fin}\left(c\right)\to \mathrm{Nat},\forall i\in \mathrm{Fin}\left(c\right),B\left(h,i\right)=\mathrm{prefixScore}\left(h,i,\mathrm{positivePrefix}\right)+\mathrm{prefixScore}\left(h,i,\mathrm{negativePrefix}\right)$$

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

The inner slot adds the two directional prefix scores.

Definition 1.16 (The supremum of ten selected slots).

$$\forall c\in \mathrm{Nat},\forall h\in \mathrm{Fin}\left(c\right)\to \mathrm{Nat},T\left(h\right)=\sup \left(\mathrm{powersetCard}\left(\mathrm{univ}\left(\mathrm{Bool}\times \mathrm{Fin}\left(c\right)\right),10\right),(\lambda Y:\mathrm{Finset}\left(\mathrm{Bool}\times \mathrm{Fin}\left(c\right)\right),\sum _{v\in Y}\mathrm{if}\left(\mathrm{fst}\left(v\right)=\mathrm{true},B\left(h,\mathrm{snd}\left(v\right)\right),A\left(h,\mathrm{snd}\left(v\right)\right)\right))\right)$$

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

Take the supremum of the sums over all sets of ten layer-column slots. When fewer than ten slots exist, the family is empty and the natural-number supremum is zero.

Definition 1.17 (Unwrapped support coordinates).

$$\forall n\in \mathrm{Nat},\forall C\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\forall i\in \mathrm{Fin}\left(\mathrm{card}\left(C\right)\right),\forall k\in \mathrm{Nat},\mathrm{liftedColumn}\left(C,i,k\right)=\mathrm{if}\left(\mathrm{val}\left(i\right)+k<\mathrm{card}\left(C\right),\mathrm{extendedColumn}\left(C,\mathrm{val}\left(i\right)+k\right),n+\mathrm{extendedColumn}\left(C,\mathrm{val}\left(i\right)+k-\mathrm{card}\left(C\right)\right)\right)$$

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

The coordinate continues beyond one wrap by adding n after the index reaches the support size.

Theorem 1.18 (A prefix is an unwrapped displacement).

$$\forall n\in \mathrm{Nat},\forall C\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\forall i\in \mathrm{Fin}\left(\mathrm{card}\left(C\right)\right),\forall k\in \mathrm{Nat},k\le \mathrm{card}\left(C\right)\Rightarrow \mathrm{positivePrefix}\left(\mathrm{gapWord}\left(C\right),i,k\right)=\mathrm{liftedColumn}\left(C,i,k\right)-\mathrm{liftedColumn}\left(C,i,0\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.positivePrefix_lifted (✓ 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 prefix of at most one full cycle equals the difference of the corresponding lifted support coordinates.

Theorem 1.19 (An occupied endpoint determines a prefix).

$$\forall n\in \mathrm{Nat},\forall C\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\forall i\in \mathrm{Fin}\left(\mathrm{card}\left(C\right)\right),\forall d\in \mathrm{Nat},\left(0<n\wedge \left(0<d\wedge \left(d<n\wedge \mathrm{sortedColumn}\left(C,i\right)+\mathrm{ofNat}\left(n,d\right)\in C\right)\right)\right)\Rightarrow \left(\exists k\in \mathrm{Nat},1\le k\wedge \left(k\le \mathrm{card}\left(C\right)\wedge \mathrm{positivePrefix}\left(\mathrm{gapWord}\left(C\right),i,k\right)=d\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.positive_request_prefix (✓ 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 a positive displacement less than n reaches another occupied column, that displacement is the sum of a nonempty cyclic gap prefix.

Theorem 1.20 (A short prefix determines its endpoint).

$$\forall n\in \mathrm{Nat},\forall C\in \mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right),\forall i\in \mathrm{Fin}\left(\mathrm{card}\left(C\right)\right),\forall k\in \mathrm{Nat},\forall d\in \mathrm{Nat},\left(0<n\wedge \left(1\le k\wedge \left(k\le \mathrm{card}\left(C\right)\wedge \left(d<n\wedge \mathrm{positivePrefix}\left(\mathrm{gapWord}\left(C\right),i,k\right)=d\right)\right)\right)\right)\Rightarrow \mathrm{sortedColumn}\left(C,\mathrm{cyclicIndex}\left(i,k\right)\right)=\mathrm{sortedColumn}\left(C,i\right)+\mathrm{ofNat}\left(n,d\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.positivePrefix_endpoint (✓ 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 nonempty prefix of at most one cycle, with total below n, ends at the column obtained by adding that total modulo n.

Theorem 1.21 (Ten slots dominate requests and collisions).

$$\forall n\in \mathrm{Nat},\forall X\in \mathrm{Finset}\left(\mathrm{Bool}\times \mathrm{Fin}\left(n\right)\right),\left(14\le n\wedge \mathrm{card}\left(X\right)=10\right)\Rightarrow 2\cdot \left(I\left(n,X\right)+K\left(n,X\right)\right)\le T\left(\mathrm{gapWord}\left(\mathrm{columns}\left(X\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.slot_domination (✓ 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 at circumference at least fourteen, twice the sum of occupied requests and empty collisions is at most the ten-slot score of its gap word.

References

• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.A
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.B
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.I
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.K
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.T
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.boundary_request_identity
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.cyclicIndex
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.extendedColumn
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.gapWord
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.liftedColumn
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.negativePrefix
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.negativeRequests
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.phi
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.positivePrefix
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.positivePrefix_endpoint
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.positivePrefix_lifted
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.positiveRequests
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.positive_request_prefix
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.prefixScore
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.slot_domination
• Truth anchor: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeRequests.sortedColumn
• Dependency: D5/S3/Combinatorics/GeneralizedPetersen/ZeroForcingThreeBoundary