JenzerPermutedRotorLoopWords

Abstract

Balanced exterior words cancel odd full-support coefficients.

Theorem 1.1 (Subset expansion of the chain).

$$\forall (V:Type),[\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(\mathbb{R},V\right)]\forall (q:\mathrm{QuadraticForm}\left(\mathbb{R},V\right)),\forall (k:\mathbb{N}),\forall (B:(\mathrm{Fin}\left(k\right)\to \mathrm{CliffordAlgebra}\left(q\right))),\forall (theta:(\mathrm{Fin}\left(k\right)\to \mathbb{R})),\mathrm{chain}\left(B,theta\right)=(\sum _{S\in ((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right))).\mathrm{powerset}}((a\left(theta,S\right))\cdot (\mathrm{subsetProduct}\left(B,S\right))))$$

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

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.

Distributing the ordered rotor product gives one increasing product for each subset, weighted by a. This expansion needs no anticommutation assumption.

Theorem 1.2 (Square of an increasing subset product).

$$\forall (V:Type),[\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(\mathbb{R},V\right)]\forall (q:\mathrm{QuadraticForm}\left(\mathbb{R},V\right)),\forall (k:\mathbb{N}),\forall (B:(\mathrm{Fin}\left(k\right)\to \mathrm{CliffordAlgebra}\left(q\right))),(\mathrm{AnticommutingUnitFamily}\left(q,k,B\right))\Rightarrow (\forall (S:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)),(\mathrm{subsetProduct}\left(B,S\right))\cdot (\mathrm{subsetProduct}\left(B,S\right))=((((-(1):\mathbb{R}){)}^{\mathrm{Nat}.\mathrm{div}\left(((S).\mathrm{card})\cdot (((S).\mathrm{card})+(1)),2\right)})\cdot ((1:\mathrm{CliffordAlgebra}\left(q\right)))))$$

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

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

Commentary.

The square depends only on the subset size. Nat.div is natural-number division. This is the Square of a Subset Product identity in Jenzer, Lemma 3.2.

Theorem 1.3 (Complementary subset coefficients).

$$\forall (k:\mathbb{N}),\forall (theta:(\mathrm{Fin}\left(k\right)\to \mathbb{R})),\forall (S:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)),(a\left(theta,S\right))\cdot (a\left(theta,((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)))\setminus (S)\right))=(\prod _{i\in (\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right))}((s\left(theta,i\right))\cdot (c\left(theta,i\right))))$$

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

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.

Multiplying coefficients for complementary subsets selects one sine and one cosine at every index, including when one of them is zero.

Theorem 1.4 (Subset expansion of the return product).

$$\forall (V:Type),[\mathrm{AddCommGroup}\left(V\right)][\mathrm{Module}\left(\mathbb{R},V\right)]\forall (q:\mathrm{QuadraticForm}\left(\mathbb{R},V\right)),\forall (k:\mathbb{N}),\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{returnProduct}\left(B,theta,tau\right)=(\sum _{S\in ((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right))).\mathrm{powerset}}((((((-(1):\mathbb{R}){)}^{(S).\mathrm{card}})\cdot (((-(1):\mathbb{R}){)}^{\mathrm{inversionCount}\left(tau,S\right)}))\cdot (a\left(theta,S\right)))\cdot (\mathrm{subsetProduct}\left(B,S\right)))))$$

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

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

Commentary.

Reversion contributes one minus sign per selected bivector. Sorting the return order contributes the inversion parity on that subset. Every factor is retained in the coefficient; this is the return-product subset expansion and inversion-sign identity in the proof of Jenzer Theorem 5.5, before the star condition is used.

Theorem 1.5 (Complementary scalar pairs and exterior coefficients).

$$\forall (A:Type\ast ),[\mathrm{Ring}\left(A\right)][\mathrm{Algebra}\left(\mathbb{R},A\right)]\forall (k:\mathbb{N}),\forall (B:(\mathrm{Fin}\left(k\right)\to A)),(\forall (i:\mathrm{Fin}\left(k\right)),\forall (j:\mathrm{Fin}\left(k\right)),(i\ne (j))\Rightarrow ((B\left(i\right))\cdot (B\left(j\right))=(-((B\left(j\right))\cdot (B\left(i\right))))))\Rightarrow (\forall (t:\mathrm{LinearMap}\left(\mathbb{R},A,\mathbb{R}\right)),\forall (b:\mathrm{Module}.\mathrm{Basis}\left(\mathrm{Fin}\left(k\right),\mathbb{R},(\mathrm{Fin}\left(k\right)\to \mathbb{R})\right)),\forall (S:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)),t\left(((((S).\mathrm{sort}\left((\mathrm{fun}u\mapsto (\mathrm{fun}v\mapsto u\le (v)))\right)).\mathrm{map}\left(B\right)).\mathrm{prod})\cdot ((((((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)))\setminus (S)).\mathrm{sort}\left((\mathrm{fun}u\mapsto (\mathrm{fun}v\mapsto u\le (v)))\right)).\mathrm{map}\left(B\right)).\mathrm{prod})\right)=((((b).\mathrm{ExteriorAlgebra}).\mathrm{repr}\left(((b).\mathrm{ExteriorAlgebra}\left(S\right))\cdot ((b).\mathrm{ExteriorAlgebra}\left(((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)))\setminus (S)\right))\right)\left((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right))\right))\cdot (t\left(((((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right))).\mathrm{sort}\left((\mathrm{fun}u\mapsto (\mathrm{fun}v\mapsto u\le (v)))\right)).\mathrm{map}\left(B\right)).\mathrm{prod}\right))))$$

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

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.

For complementary supports, the Clifford sign is the top exterior coefficient of the corresponding pair. No cyclicity of the linear functional is required here.

Theorem 1.6 (Top exterior coefficients require complementary supports).

$$\forall (k:\mathbb{N}),\forall (b:\mathrm{Module}.\mathrm{Basis}\left(\mathrm{Fin}\left(k\right),\mathbb{R},(\mathrm{Fin}\left(k\right)\to \mathbb{R})\right)),\forall (S:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)),\forall (T:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)),(T\ne (((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)))\setminus (S)))\Rightarrow (((b).\mathrm{ExteriorAlgebra}).\mathrm{repr}\left(((b).\mathrm{ExteriorAlgebra}\left(S\right))\cdot ((b).\mathrm{ExteriorAlgebra}\left(T\right))\right)\left((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right))\right)=(0))$$

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

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.

Repeated generators annihilate an exterior word, while a support missing an index cannot have the top coefficient. Thus only complementary supports contribute.

Theorem 1.7 (A nonempty index set has no self-complementary subset).

$$\forall (k:\mathbb{N}),(1\le (k))\Rightarrow (\forall (S:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)),S\ne (((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right)))\setminus (S)))$$

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

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.

At any chosen index, membership in a subset is the negation of membership in its complement.

Theorem 1.8 (Cancellation of the odd full-support coefficient).

$$\forall (k:\mathbb{N}),\forall (b:\mathrm{Module}.\mathrm{Basis}\left(\mathrm{Fin}\left(k\right),\mathbb{R},(\mathrm{Fin}\left(k\right)\to \mathbb{R})\right)),\forall (tau:\mathrm{Equiv}.\mathrm{Perm}\left(\mathrm{Fin}\left(k\right)\right)),(\mathrm{Odd}\left(k\right))\Rightarrow (\sum _{S\in ((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right))).\mathrm{powerset}}(\sum _{T\in ((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right))).\mathrm{powerset}}(((((-(1):\mathbb{R}){)}^{(T).\mathrm{card}})\cdot (((-(1):\mathbb{R}){)}^{\mathrm{inversionCount}\left(tau,T\right)}))\cdot (((b).\mathrm{ExteriorAlgebra}).\mathrm{repr}\left(((b).\mathrm{ExteriorAlgebra}\left(S\right))\cdot ((b).\mathrm{ExteriorAlgebra}\left(T\right))\right)\left((\mathrm{Finset}.\mathrm{univ}:\mathrm{Finset}\left(\mathrm{Fin}\left(k\right)\right))\right))))=(0))$$

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

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.

The balanced exterior word has even parity for every permutation. Its odd top coefficient vanishes; expansion identifies that coefficient with the displayed double sum.

References

• Truth anchor: D5/S3/QuadraticForms/JenzerPermutedRotorLoopWords.canonical_complementary_trace
• Truth anchor: D5/S3/QuadraticForms/JenzerPermutedRotorLoopWords.canonical_exterior_top
• Truth anchor: D5/S3/QuadraticForms/JenzerPermutedRotorLoopWords.chain_expansion
• Truth anchor: D5/S3/QuadraticForms/JenzerPermutedRotorLoopWords.coefficient_complement
• Truth anchor: D5/S3/QuadraticForms/JenzerPermutedRotorLoopWords.complement_ne_self
• Truth anchor: D5/S3/QuadraticForms/JenzerPermutedRotorLoopWords.return_expansion
• Truth anchor: D5/S3/QuadraticForms/JenzerPermutedRotorLoopWords.signed_top_sum_zero
• Truth anchor: D5/S3/QuadraticForms/JenzerPermutedRotorLoopWords.subsetProduct_square
• Dependency: D5/S3/QuadraticForms/JenzerPermutedRotorLoopAlgebra