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

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,\ldots,B_k$ in a finite-dimensional nondegenerate real Clifford algebra, $k\geq1$, put $c_i=\cos(\theta_i/2)$, $s_i=\sin(\theta_i/2)$, $w_i=s_i^2$, $U_i=c_i+s_iB_i$, and $\Theta_k(\tau)=(U_1\cdots U_k)(\widetilde U_{\tau(1)}\cdots\widetilde U_{\tau(k)})$. Then the proved statement is

$$ \langle\Theta_k(\tau)\rangle_0 =\sum_{S\subseteq{1,\ldots,k}} \eta(|S|)(-1)^{\iota(\tau,S)} \prod_{i\in S}w_i\prod_{i\notin S}(1-w_i), \qquad \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

| Source clause | Lean counterpart | Scope | | --- | --- | --- | | Real finite-dimensional space and nondegenerate quadratic form | claim binders V, real module and finite-dimensional instances, q, q.Nondegenerate | All source signatures | | Positive family size | k, 1 ≤ k | Every positive natural size | | Homogeneous bivectors, square $-1$, pairwise anticommutation | IsBivector, the three conjuncts of AnticommutingUnitFamily | No independence assumption | | Native scalar coefficient and reversion | scalarProjection, CliffordAlgebra.reverse in returnProduct | The exterior equivalence reads grades only; multiplication remains Clifford multiplication | | All real angles and all return permutations | θ, τ in claim | Zero sine and cosine values included | | Ordered products, subset weights and restricted inverse inversions | subsetProduct, rotor, chain, returnProduct, loop, a, c, s, w, inversionCount, eta | Fin k is the increasing relabelling of the one-based source indices | | Removal of the star condition | StarCondition is defined, but is absent from claim | No replacement hypothesis |

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.

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.

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.

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.

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.

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_1B_2B_3=-1$, and its rationally rotated family. They check all six return permutations for each of these families, all $873$ permutations for $1\leq k\leq6$, 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.

| Item | Status | Evidence kind and scope | | --- | --- | --- | | Anticommuting conjugations remove nonempty trace components except possible odd full support, whose aggregate cancels by balanced exterior parity | proved | Kernel-checked JenzerPermutedRotorLoopAlgebra.TraceSupport.tracial_subset_vanishing, TraceSupport.tracial_off_diagonal_zero, and JenzerPermutedRotorLoopWords.ExteriorSum.signed_top_sum_zero, combined by JenzerPermutedRotorLoop.result | | The unchanged source claim for every positive family size, permutation, angle and source signature, with no nonzero sine/cosine or independence assumption | proved | Kernel-checked JenzerPermutedRotorLoop.result : JenzerPermutedRotorLoopAlgebra.claim | | Native scalar cyclicity for degenerate forms and without finite dimension | proved | Kernel-checked JenzerPermutedRotorLoopAlgebra.NativeBridge.scalar_cyclic; its telescope has neither restriction | | Exact finite triangle, rational rotation, permutation and signature cases return ALL_CHECKS_OK | computed | The pinned experiment above, command exit 0 and recorded SHA-256; precisely $1\leq k\leq6$ and the geometric cases in dimensions $2,3,4$ | | A separately packaged general tracial-algebra rotor theorem and star-family classification | open | Neither is a conclusion of the settling theorem |

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.

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.