A mixed-sign Gaussian refutes Galindo–Rowell Conjecture 10.6

Abstract

A mixed-sign Gaussian in dimension fifteen refutes the Pauli-direction rigidity conjecture for cyclic unitary Yang–Baxter operators.

Definition 1.1 (The cyclic clock matrix).

$$\forall w:\mathbb{C},\forall d:\mathbb{N},\mathrm{clockZ}\left(w,d\right)=\mathrm{diagonal}\left(\lambda j:\mathrm{ZMod}\left(d\right)\mapsto w^{\mathrm{val}\left(j\right)}\right)$$

Formalization. D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.clockZ (✓ std3).

Citation. C. Galindo; E. C. Rowell (2026). Unitary Yang–Baxter Operators: Towards a Classification. URL: https://arxiv.org/abs/2608.16865.

Commentary.

The source fixes the clock by (arXiv:2608.16865v1, §10.2): “Ze_j=w^je_j”. The diagonal entry at j is w raised to the canonical ZMod representative.

Definition 1.2 (The Pauli-direction operator).

$$\forall d:\mathbb{N},[\mathrm{NeZero}\left(d\right)],\forall w:\mathbb{C},\forall alpha:\mathrm{Units}\left(\mathrm{ZMod}\left(d\right)\right),P\left(w,alpha\right)=\mathrm{kronecker}\left(\mathrm{shiftMatrix}\left(d\right),\mathrm{clockZ}{\left(w,d\right)}^{\mathrm{val}\left(\mathrm{val}\left(alpha\right)\right)}\right)$$

Formalization. D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.P (✓ std3).

Citation. C. Galindo; E. C. Rowell (2026). Unitary Yang–Baxter Operators: Towards a Classification. URL: https://arxiv.org/abs/2608.16865.

Commentary.

The source writes (arXiv:2608.16865v1, §10.2): “P_α=X⊗Z^α”. The Lean definition is the Kronecker product of the shift and the α-th clock power. The inner val is Units.val and the outer val is ZMod.val.

Definition 1.3 (The cyclic coefficient operator).

$$\forall d:\mathbb{N},[\mathrm{NeZero}\left(d\right)],\forall w:\mathbb{C},\forall alpha:\mathrm{Units}\left(\mathrm{ZMod}\left(d\right)\right),\forall a:\mathrm{ZMod}\left(d\right)\to \mathbb{C},R\left(w,alpha,a\right)=\mathrm{sum}\left(t\in \mathrm{ZMod}\left(d\right),at\cdot P{\left(w,alpha\right)}^{\mathrm{val}\left(t\right)}\right)$$

Formalization. D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.R (✓ std3).

Citation. C. Galindo; E. C. Rowell (2026). Unitary Yang–Baxter Operators: Towards a Classification. URL: https://arxiv.org/abs/2608.16865.

Commentary.

The source writes (arXiv:2608.16865v1, §10.2): “R(a)=∑_{t=0}^{d−1}a_tP^t”. The Lean sum ranges over ZMod d and uses the literal P power and coefficient scalar multiplication.

Definition 1.4 (The braid Yang–Baxter equation).

$$\forall d:\mathbb{N},[\mathrm{NeZero}\left(d\right)],\forall r:\mathrm{Matrix}\left((\mathrm{ZMod}\left(d\right)\times \mathrm{ZMod}\left(d\right)),(\mathrm{ZMod}\left(d\right)\times \mathrm{ZMod}\left(d\right)),\mathbb{C}\right),\mathrm{BraidYBE}\left(r\right)=((\mathrm{mul}\left(\mathrm{mul}\left(\mathrm{reindex}\left(\mathrm{prodAssoc}\left(\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right)\right),\mathrm{prodAssoc}\left(\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right)\right),\mathrm{kronecker}\left(r,1\right)\right),\mathrm{kronecker}\left(1,r\right)\right),\mathrm{reindex}\left(\mathrm{prodAssoc}\left(\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right)\right),\mathrm{prodAssoc}\left(\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right)\right),\mathrm{kronecker}\left(r,1\right)\right)\right))=(\mathrm{mul}\left(\mathrm{mul}\left(\mathrm{kronecker}\left(1,r\right),\mathrm{reindex}\left(\mathrm{prodAssoc}\left(\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right)\right),\mathrm{prodAssoc}\left(\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right),\mathrm{ZMod}\left(d\right)\right),\mathrm{kronecker}\left(r,1\right)\right)\right),\mathrm{kronecker}\left(1,r\right)\right)))$$

Formalization. D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.BraidYBE (✓ std3).

Citation. C. Galindo; E. C. Rowell (2026). Unitary Yang–Baxter Operators: Towards a Classification. URL: https://arxiv.org/abs/2608.16865.

Commentary.

Section 2 of arXiv:2608.16865v1 displays “(R⊗I)(I⊗R)(R⊗I) = (I⊗R)(R⊗I)(I⊗R)”. The symbols prodAssoc, reindex and kronecker denote Equiv.prodAssoc, Matrix.reindex and Matrix.kronecker. Both identity matrices have type Matrix (ZMod d) (ZMod d) Complex. The reindexed first placement and the second placement act on ZMod d × (ZMod d × ZMod d).

Definition 1.5 (Projective unitarity).

$$\forall d:\mathbb{N},[\mathrm{NeZero}\left(d\right)],\forall r:\mathrm{Matrix}\left((\mathrm{ZMod}\left(d\right)\times \mathrm{ZMod}\left(d\right)),(\mathrm{ZMod}\left(d\right)\times \mathrm{ZMod}\left(d\right)),\mathbb{C}\right),\mathrm{ProjectivelyUnitary}\left(r\right)=(\exists c:\mathbb{C},c\ne 0\wedge c\cdot r\in \mathrm{unitaryGroup}\left((\mathrm{ZMod}\left(d\right)\times \mathrm{ZMod}\left(d\right)),\mathbb{C}\right))$$

Formalization. D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.ProjectivelyUnitary (✓ std3).

Source. Repository-derived.

Commentary.

Projectively unitary means that some nonzero complex scalar multiple of the operator is a member of the Mathlib Matrix.unitaryGroup object. Its matrix index type is ZMod d × ZMod d and its scalar type is Complex.

Definition 1.6 (Galindo–Rowell Conjecture 10.6).

$$\forall d:\mathbb{N},(2\le d)\Rightarrow \neg (4\mid d)\Rightarrow \forall w:\mathbb{C},\mathrm{IsPrimitiveRoot}\left(w,d\right)\Rightarrow \forall alpha:\mathrm{Units}\left(\mathrm{ZMod}\left(d\right)\right),\forall a:\mathrm{ZMod}\left(d\right)\to \mathbb{C},a\left(0\right)=1\Rightarrow (\forall t:\mathrm{ZMod}\left(d\right),\mathrm{norm}\left(a\left(t\right)\right)=1)\Rightarrow \mathrm{BraidYBE}\left(R\left(w,alpha,a\right)\right)\Rightarrow \mathrm{ProjectivelyUnitary}\left(R\left(w,alpha,a\right)\right)\Rightarrow \exists eps:\mathrm{ZMod}\left(d\right),(eps=1\vee eps=-1)\wedge (\forall s:\mathrm{ZMod}\left(d\right),\forall t:\mathrm{ZMod}\left(d\right),a\left(s+t\right)=a\left(s\right)\times a\left(t\right)\times w^{\mathrm{val}\left(eps\times \mathrm{val}\left(alpha\right)\times s\times t\right)})$$

Formalization. D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.claim (✓ std3).

Citation. C. Galindo; E. C. Rowell (2026). Unitary Yang–Baxter Operators: Towards a Classification. URL: https://arxiv.org/abs/2608.16865.

Commentary.

Galindo–Rowell, Conjecture 10.6, arXiv:2608.16865v1, p. 43, §10.2.7: “Let d≥2 with 4∤d, let α∈(Z/dZ)^×, and put P_α=X⊗Z^α, τ_α(s,t)=w^{αst} (s,t∈Z/dZ). Suppose that a=(1,a_1,…,a_{d−1})∈T_d^{coef} and that R_α(a)=∑{t∈Z/dZ}a_tP_α^t satisfies the Yang–Baxter equation and is projectively unitary. Then a belongs to one of the two signed Gaussian torsors for τ_α: there exists ε∈{+1,−1} such that a{s+t}=a_sa_tτ_α(s,t)^ε (s,t∈Z/dZ).” The encoding uses ZMod d, primitive roots in Complex, unit alpha, a 0 = 1, and the unit-modulus phase-torus condition for every index.

Theorem 1.7 (Conjecture 10.6 is refuted).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.result (✓ std3). ∎

Resolves. Problems/galindo-rowell-2026-pauli-rigidity-mixed-sign-refutation (refuted) by D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.result.

Source. Repository-derived.

Commentary.

At d=15, α=1, and a_t=w^(2t²) for a primitive fifteenth root, the coefficient-to-braid identity and a translation of the finite character sum prove the braid equation. Character orthogonality gives R R†=15·I, hence projective unitarity. At s=t=1 the two signs would require w^8=w^5 or w^8=w^3, both impossible for a primitive fifteenth root.

References

• Truth anchor: D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.BraidYBE
• Truth anchor: D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.P
• Truth anchor: D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.ProjectivelyUnitary
• Truth anchor: D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.R
• Truth anchor: D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.claim
• Truth anchor: D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.clockZ
• Truth anchor: D5/S3/Quantum/Algebra/CyclicYangBaxterPauliRigidityRefutation.result
• Dependency: D5/S3/Observer/WindowRegister
• Dependency: D5/S3/Quantum/Algebra/WeylDisplacementAdjoint