slug: jen2610
bibkey: jenzer2026starorderedrotorloops
doi: 10.48550/arXiv.2610.21593
url: https://arxiv.org/abs/2610.21593v1
triage: theorem
motivation_gids:
  - D5/S3/QuadraticForms/JenzerPermutedRotorLoop.result

Jenzer’s permuted rotor-loop formula without the star condition

Problem

Nik Jenzer, Star-Ordered Rotor Loops in Clifford Algebras, arXiv:2610.21593v1, Theorem 5.5 and the following scope remark, TeX Remark 5.7, rendered Remark 5.5, page 19, asks whether the permuted loop formula remains true without the star condition:

Nevertheless, numerical evidence suggests that the formula also holds without the star condition in that case: tested on the triangle family from Remark 4.4, which violates the star condition, under all six permutations of {1, 2, 3} with random parameter sets; the largest deviation encountered was in the range of double machine precision. A general proof would have to capture the cancellation of the odd off-diagonal terms in coarser groups than pairs; we have not determined such a grouping.

For an anticommuting unit bivector family $B_1,\dots ,B_k$ in a finite-dimensional nondegenerate real Clifford algebra, $k\ge 1$, put $c_i=\cos ({\theta }_i/2)$, $s_i=\sin ({\theta }_i/2)$, $w_i=s_i^2$, $U_i=c_i+s_i{B}_i$, and ${\Theta }_k(\tau )=(U_1\cdots U_k)({\tilde{U}}_{\tau (1)}\cdots {\tilde{U}}_{\tau (k)})$. Then the proved statement is

$$⟨{\Theta }_k(\tau ){⟩}_0=\sum _{S\subseteq \{1,\dots ,k\}}\eta (|S|)(-1{)}^{\iota (\tau ,S)}\prod _{i\in S}{w}_i\prod _{i\notin S}(1-w_i),\eta (m)=(-1{)}^m(-1{)}^{m(m+1)/2}.$$

Here $\iota (\tau ,S)$ counts pairs $i<j$ in $S$ with ${\tau }^{-1}(i)>{\tau }^{-1}(j)$. No star condition is assumed.

Statement echo

The canonical names in the table belong to D5.S3.QuadraticForms.JenzerPermutedRotorLoopAlgebra. The settling theorem is D5.S3.QuadraticForms.JenzerPermutedRotorLoop.result. The public definitions retain the source expressions and the binding conventions in #22266.

Motivation

The external named scope conjecture is preregistered in https://github.com/the-omega-institute/trureturing/issues/22266. Its settling declaration is D5/S3/QuadraticForms/JenzerPermutedRotorLoop.result, with admission basis open-problem-resolution (#22266; Proved). The scalar-cyclicity and exterior-word modules supply consumed parts of this proof.

Gap

The source’s termwise pairing for the identity permutation does not give the arbitrary-permutation formula. A family may have a nonzero odd full-support scalar coefficient, so discarding every nonempty subset coefficient would assume the star condition that the question removes.

The source and literature screen recorded in #22266 located no settlement in its successfully inspected scope. The arXiv author/title screen, available Codeberg repository and issue metadata, Zenodo metadata and Crossref title screen do not establish completeness. OpenAlex and Semantic Scholar requests were rate-limited; MathOverflow API requests failed; the Zenodo attachment and versions endpoints were inaccessible. Literature completeness is ASSUMED-UNVERIFIED.

Route

JenzerPermutedRotorLoopAlgebra.NativeBridge.scalar_cyclic proves cyclicity of the native scalar coefficient. Its tracial support lemmas eliminate all unequal subset pairs except complementary odd full support. JenzerPermutedRotorLoopWords.ExteriorSum.signed_top_sum_zero proves that the balanced exterior word has zero odd top coefficient. The private JenzerPermutedRotorLoop.scalar_pair_split expresses the exceptional terms with that common coefficient. Their sum is zero; the diagonal subset-square and squared trigonometric-weight formulas supply exactly the source sum. These names are relative to D5.S3.QuadraticForms.

Falsifier

A source-family instance, real angle vector and permutation violating the displayed identity would refute the claim. A construction that changes the native scalar projection, replaces bivectors by arbitrary even elements, or assumes vanishing full support does not address this claim. Finite experiments alone do not settle the universal statement.

Evidence

The canonical Lean sources are D5/S3/QuadraticForms/JenzerPermutedRotorLoopAlgebra.lean, D5/S3/QuadraticForms/JenzerPermutedRotorLoopWords.lean and D5/S3/QuadraticForms/JenzerPermutedRotorLoop.lean, with their corresponding Blueprint Scribes. JenzerPermutedRotorLoop.result proves the unchanged JenzerPermutedRotorLoopAlgebra.claim.

Exact finite experiment

The experiment is published in trureturing-experiments, pinned rotor-loop directory. The program check.py has SHA-256 314438c29013e5ae8ec9dde252f9b29c526854c6c591d11d9c661242b055a759. The reproduction command from the lane worktree is git -C ../trureturing-experiments show 8bb94a407557328c74589fd7b9dd31ed49b061e0:docs/reports/permuted-rotor-loop/check.py | python3; it exits 0 and returns ALL_CHECKS_OK.

The exact integer/rational polynomial checks reproduce the source triangle in ${\mathrm{Cl}}_{0,3}$, where $B_1{B}_2{B}_3=-1$, and its rationally rotated family. They check all six return permutations for each of these families, all $873$ permutations for $1\le k\le 6$, including the vanishing odd exceptional coefficient, and $142$ canonical bivector subset families with $326$ return orders across every nondegenerate signature in dimensions $2,3,4$. These are computed finite results, independent of the universal Lean proof.

Triage

What the settlement shows

The decisive mechanism is aggregate cancellation: cyclicity removes the proper off-diagonal supports, and the odd full-support obstruction is the odd top coefficient of a balanced exterior word. The named theorems in the first row prove these parts and their use in the settling identity. The source claim retains its full finite-dimensional nondegenerate scope, while native scalar cyclicity is proved for every real quadratic form on a real module, including degenerate forms and infinite-dimensional modules. No nonvanishing trigonometric coefficient is required.

The result removes the star hypothesis from source Theorem 5.5, resolving its following scope remark. It makes no star-family classification, no higher-grade claim and no separately packaged general tracial rotor theorem. The source’s reverse-order corollary remains its inverse-factor cancellation statement; it is not an additional resolution claim here.

Four-slot escape registration remains unfinished for the public theorems, with the template and bridge gaps recorded in https://github.com/the-omega-institute/trureturing/issues/22564. No declared-validated registration is asserted.

ASSUMED-UNVERIFIED

Literature completeness beyond the successfully inspected sources is ASSUMED-UNVERIFIED; inaccessible and unindexed results are not ruled out. The finite checker does not certify an unbounded theorem. Escape-audit registration is unfinished as linked above and is separate from kernel verification of the mathematical declarations.