JenzerPermutedRotorLoop

Abstract

Permuted rotor loops obey the subset formula without the star condition.

Theorem 1.1 (Permuted rotor loops without the star condition).

$$\forall (V:Type),[\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(\mathbb{R},V\right)][\mathrm{FiniteDimensional}\left(\mathbb{R},V\right)]\forall (q:\mathrm{QuadraticForm}\left(\mathbb{R},V\right)),((q).\mathrm{Nondegenerate})\Rightarrow (\forall (k:\mathbb{N}),(1\le (k))\Rightarrow (\forall (B:(\mathrm{Fin}\left(k\right)\to \mathrm{CliffordAlgebra}\left(q\right))),(\mathrm{AnticommutingUnitFamily}\left(q,k,B\right))\Rightarrow (\forall (theta:(\mathrm{Fin}\left(k\right)\to \mathbb{R})),\forall (tau:\mathrm{Equiv}.\mathrm{Perm}\left(\mathrm{Fin}\left(k\right)\right)),\mathrm{scalarProjection}\left(q,\mathrm{loop}\left(B,theta,tau\right)\right)=(\sum _{S\in ((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right))).\mathrm{powerset}}((((\mathrm{eta}\left((S).\mathrm{card}\right))\cdot (((-(1):\mathbb{R}){)}^{\mathrm{inversionCount}\left(tau,S\right)}))\cdot (\prod _{i\in S}(w\left(theta,i\right))))\cdot (\prod _{i\in ((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)))\setminus (S)}((1)-(w\left(theta,i\right)))))))))$$

Proof. Machine-checked in Lean as D5/S3/QuadraticForms/JenzerPermutedRotorLoop.result (✓ std3). ∎

Resolves. Problems/jen2610 (proved) by D5/S3/QuadraticForms/JenzerPermutedRotorLoop.result.

Source. Repository-derived.

Acknowledgement. Nik Jenzer (2026). Star-Ordered Rotor Loops in Clifford Algebras. DOI: 10.48550/arXiv.2610.21593. URL: https://arxiv.org/abs/2610.21593v1.

Commentary.

Anticommuting conjugations remove all off-diagonal scalar terms except possible odd full support. The top coefficient of the balanced exterior word cancels that aggregate. The remaining diagonal terms give the full subset formula for every source signature, angle and permutation. No nonzero sine or cosine assumption is used.

References

• Truth anchor: D5/S3/QuadraticForms/JenzerPermutedRotorLoop.result
• Dependency: D5/S3/QuadraticForms/JenzerPermutedRotorLoopAlgebra
• Dependency: D5/S3/QuadraticForms/JenzerPermutedRotorLoopWords