CycleTwentyOneNoUniformMixing

Abstract

Orbit sums, support masks and an exact integer Laurent identity exclude instantaneous uniform mixing on the cycle with twenty-one vertices.

Theorem 1.1 (no_uniform_mixing_of_no_common_nonzero_root).

$$\forall (t:\mathbb{R}),(\forall (x0x1x2x3x4x5:\mathbb{C}),x0\ne 0\to x1\ne 0\to x2\ne 0\to x3\ne 0\to x4\ne 0\to x5\ne 0\to D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g1x0x1x2x3x4x5=0\to D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g2x0x1x2x3x4x5=0\to D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g3x0x1x2x3x4x5=0\to D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g4x0x1x2x3x4x5=0\to D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g5x0x1x2x3x4x5=0\to D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g6x0x1x2x3x4x5=0\to D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g7x0x1x2x3x4x5=0\to D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g8x0x1x2x3x4x5=0\to D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g9x0x1x2x3x4x5=0\to D5.S3.Quantum.Dynamics.CycleUniformMixing.SupportMaskChecker.Ring.g10x0x1x2x3x4x5=0\to \mathrm{False})\to (\neg (\forall ab:\mathrm{ZMod}21,Complex.normSq(NormedSpace.exp(SMul.smul(((t:\mathbb{C})\cdot Complex.I))(D5.S3.Quantum.Dynamics.CycleUniformMixing.OrbitIndexedSums.Fourier.cycleA))ab)=1/21))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/CycleTwentyOneNoUniformMixing.no_uniform_mixing_of_no_common_nonzero_root (✓ std3). ∎

Source. Repository-derived.

Commentary.

If the ten cleared phase equations have no common nonzero complex root, the Fourier correlations prevent uniform mixing on C21. The six actual exponential phases are nonzero and obey all ten equations whenever uniform mixing holds.

Definition 1.2 (claim).

$$\mathrm{claim}=\forall t:\mathbb{R},\exists uv:\mathrm{ZMod}21,Complex.normSq(NormedSpace.exp(SMul.smul(t)((SMul.smul((-Complex.I))(Matrix.reindex(ZMod.finEquiv21).\mathrm{toEquiv}(ZMod.finEquiv21).\mathrm{toEquiv}((SimpleGraph.cycleGraph21).\mathrm{adjMatrix}\mathbb{C})))))uv)\ne 1/21$$

Formalization. D5/S3/Quantum/Dynamics/CycleUniformMixing/CycleTwentyOneNoUniformMixing.claim (✓ std3).

Citation. A. Ahmadi; R. Belk; C. Tamon; C. Wendler (2003). On mixing in continuous-time quantum walks on some circulant graphs. DOI: 10.26421/qic3.6-4. URL: https://arxiv.org/abs/quant-ph/0209106v5.

Commentary.

“No complete cycle $C_n$, except for $C_3,C_4$, has the instantaneous uniform mixing property under the continuous-time quantum walk model.” (Ahmadi–Belk–Tamon–Wendler, quant-ph/0209106v5, p. 7, Conjecture 1). The claim here is its C21 case: real time, exp(t • ((−Complex.I) • A)), and an existential pair of vertices. The adjacency is Mathlib cycleGraph(21).adjMatrix, reindexed through ZMod.finEquiv(21).

Theorem 1.3 (result).

$$\mathrm{claim}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CycleUniformMixing/CycleTwentyOneNoUniformMixing.result (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Alison Gray; Pransu Patel; Isaiah Young (2026). The cycle C9 does not admit uniform mixing. URL: https://arxiv.org/abs/2607.28345v1.

Commentary.

At every real time at least one entry of the transition-probability matrix of C21 differs from 1/21. Fourier correlations give ten cleared polynomial equations; the integer Laurent identity excludes a common nonzero root. This excludes C21 and is partial progress on the Ahmadi–Belk–Tamon–Wendler conjecture.

References

• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/CycleTwentyOneNoUniformMixing.claim
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/CycleTwentyOneNoUniformMixing.no_uniform_mixing_of_no_common_nonzero_root
• Truth anchor: D5/S3/Quantum/Dynamics/CycleUniformMixing/CycleTwentyOneNoUniformMixing.result
• Dependency: D5/S3/Quantum/Dynamics/CycleUniformMixing/OrbitIncidenceChecker