Finite cycle seeds

Abstract

Explicit simple cycles provide small seeds for uniform nested padding.

Definition 1.1 (The six seed lists).

Lean statement: D5/S3/Combinatorics/Dice/EaslickCycleSeeds.sourceSeed

Formalization. D5/S3/Combinatorics/Dice/EaslickCycleSeeds.sourceSeed (✓ std3).

Source. Repository-derived.

Acknowledgement. Terry Easlick (2026). Computer-assisted results for n-sided non-transitive dice taking face values in [n]. URL: https://arxiv.org/abs/2610.40321v1.

Commentary.

The function sourceSeed assigns the explicit sorted-die cycles at six, seven, eight, nine, ten and eleven faces; it is empty at all other natural arguments. The corresponding lengths are 6,14,29,10,110,14. The lists omit the repeated closure row. The seven- through ten-face lists are the source lists in Appendices G through J, and the eleven-face list is obtained from the seven-face list by shifting each seed label by two and adding two low and two high faces in alternating nested intervals.

Definition 1.2 (Executable successive-edge scan).

$$\forall A\in Type,edge\in (A\to (A\to Bool)),c\in \mathrm{List}\left(A\right),\mathrm{checkSteps}\left(edge,c\right)=true\iff \left(\forall i\in Nat,i+1<\mathrm{length}\left(c\right)\Rightarrow edge\left(\mathrm{at}\left(c,i\right),\mathrm{at}\left(c,i+1\right)\right)=true\right)$$

Formalization. D5/S3/Combinatorics/Dice/EaslickCycleSeeds.checkSteps (✓ std3).

Source. Repository-derived.

Acknowledgement. Terry Easlick (2026). Computer-assisted results for n-sided non-transitive dice taking face values in [n]. URL: https://arxiv.org/abs/2610.40321v1.

Commentary.

For arbitrary encoded vertices and a Boolean edge function, recursively scan each adjacent pair. Empty and singleton lists have no edge obligation. This executable operation takes no semantic chain law.

Definition 1.3 (Executable die validation).

$$\forall n\in Nat,d\in \mathrm{List}\left(Nat\right),\mathrm{checkDie}\left(n,d\right)=true\iff \left(\left(\mathrm{length}\left(d\right)=n\wedge \left(\forall i\in Nat,i+1<\mathrm{length}\left(d\right)\Rightarrow \mathrm{at}\left(d,i\right)\le \mathrm{at}\left(d,i+1\right)\right)\right)\wedge \left(\forall x\in Nat,x\in d\Rightarrow \left(1\le x\wedge x\le n\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Dice/EaslickCycleSeeds.checkDie (✓ std3).

Source. Repository-derived.

Acknowledgement. Terry Easlick (2026). Computer-assisted results for n-sided non-transitive dice taking face values in [n]. URL: https://arxiv.org/abs/2610.40321v1.

Commentary.

At arbitrary face count n, check the exact list length, successive nondecreasing labels and the lower and upper label bounds. Repeated labels are allowed. Soundness derives global pairwise order using transitivity.

Definition 1.4 (Executable arbitrary cycle validation).

$$\forall n\in Nat,c\in \mathrm{List}\left(\mathrm{List}\left(Nat\right)\right),\mathrm{checkCycle}\left(n,c\right)=true\iff \left(\left(\left(c\ne \mathrm{nil}\left(\right)\wedge \mathrm{length}\left(\mathrm{dedup}\left(c\right)\right)=\mathrm{length}\left(c\right)\right)\wedge \left(\forall d\in \mathrm{List}\left(Nat\right),d\in c\Rightarrow \mathrm{checkDie}\left(n,d\right)=true\right)\right)\wedge \left(\forall i\in Nat,i<\mathrm{length}\left(c\right)\Rightarrow \mathrm{winCount}\left(\mathrm{at}\left(c,i\right),\mathrm{at}\left(c,\left(i+1\right)\mathrm{mod}\mathrm{length}\left(c\right)\right)\right)=\mathrm{threshold}\left(n\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Dice/EaslickCycleSeeds.checkCycle (✓ std3).

Source. Repository-derived.

Acknowledgement. Terry Easlick (2026). Computer-assisted results for n-sided non-transitive dice taking face values in [n]. URL: https://arxiv.org/abs/2610.40321v1.

Commentary.

For arbitrary n and any finite list of encoded dice, check nonemptiness, duplicate removal preserving length, die validation and exact win counts on the closed list. This scans the actual input and never assumes validity, distinctness or a graph law.

Theorem 1.5 (General cycle checker soundness).

$$\forall n\in Nat,c\in \mathrm{List}\left(\mathrm{List}\left(Nat\right)\right),\left(3\le n\wedge \mathrm{checkCycle}\left(n,c\right)=true\right)\Rightarrow \mathrm{HasCycle}\left(n,\mathrm{length}\left(c\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Dice/EaslickCycleSeeds.checkCycle_sound (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Terry Easlick (2026). Computer-assisted results for n-sided non-transitive dice taking face values in [n]. URL: https://arxiv.org/abs/2610.40321v1.

Commentary.

For every n at least three and every encoded finite input c, successful checkCycle reconstructs HasCycle(n,length(c)) in the original graph defined by actual minimum unconditional win probabilities. Its only checking premise is the executable Boolean result; the true-minimum bridge supplies the interpretation of the tested edge counts.

Theorem 1.6 (Actual first checker inputs).

$$\forall n\in Nat,\left(n=6\vee \left(n=7\vee \left(n=8\vee \left(n=9\vee \left(n=10\vee n=11\right)\right)\right)\right)\right)\Rightarrow \mathrm{checkCycle}\left(n,\mathrm{sourceSeed}\left(n\right)\right)=true$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Dice/EaslickCycleSeeds.sourceSeed_check (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Terry Easlick (2026). Computer-assisted results for n-sided non-transitive dice taking face values in [n]. URL: https://arxiv.org/abs/2610.40321v1.

Commentary.

The unchanged six source and derived seed lists, at n in 6,7,8,9,10,11, pass checkCycle by kernel reduction. This is a computed first-instance certificate for the general checker. It is consumed by checkCycle_sound in finite_cycle_witnesses and then by the complete conjecture proof; it is not an independent finite-case resolution.

Theorem 1.7 (The verified finite cycle lengths).

$$\left(\left(\left(\left(\mathrm{HasCycle}\left(6,6\right)\wedge \mathrm{HasCycle}\left(7,14\right)\right)\wedge \mathrm{HasCycle}\left(8,29\right)\right)\wedge \mathrm{HasCycle}\left(9,10\right)\right)\wedge \mathrm{HasCycle}\left(10,110\right)\right)\wedge \mathrm{HasCycle}\left(11,14\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Dice/EaslickCycleSeeds.finite_cycle_witnesses (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Terry Easlick (2026). Computer-assisted results for n-sided non-transitive dice taking face values in [n]. URL: https://arxiv.org/abs/2610.40321v1.

Commentary.

There is a simple minimum-advantage cycle of length six for six-face dice, length fourteen for seven-face dice, length twenty-nine for eight-face dice, length ten for nine-face dice, length one hundred ten for ten-face dice, and length fourteen for eleven-face dice. Every die is sorted with valid labels, all vertices in each cycle are distinct, and every edge including the closing edge has the true minimum probability above one half. These assertions supply finite seeds and do not assert the unbounded parameter statement or the global upper bound at six.

References

• Truth anchor: D5/S3/Combinatorics/Dice/EaslickCycleSeeds.checkCycle
• Truth anchor: D5/S3/Combinatorics/Dice/EaslickCycleSeeds.checkCycle_sound
• Truth anchor: D5/S3/Combinatorics/Dice/EaslickCycleSeeds.checkDie
• Truth anchor: D5/S3/Combinatorics/Dice/EaslickCycleSeeds.checkSteps
• Truth anchor: D5/S3/Combinatorics/Dice/EaslickCycleSeeds.finite_cycle_witnesses
• Truth anchor: D5/S3/Combinatorics/Dice/EaslickCycleSeeds.sourceSeed
• Truth anchor: D5/S3/Combinatorics/Dice/EaslickCycleSeeds.sourceSeed_check
• Dependency: D5/S3/Combinatorics/Dice/EaslickMinimalAdvantage