slug: sp322844-serpentine-higher
bibkey: spezia2018a322844
doi: null
url: https://oeis.org/A322844
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Matrix/SpeziaSerpentineHigherExteriorTrace.result

The higher exterior traces of Spezia’s serpentine matrix

Problem

Stefano Spezia, OEIS A322844, COMMENTS revision 68, states:

For k > 2, the trace of the k-th exterior power of the matrix M(n) is equal to zero.

The matrix definition is shared with A317614 revision 194. With one-based indices $1\le i,j\le n$, its integer entries are $M_{ij}=j+n(i-1)$ for odd $i$ and $M_{ij}=ni-j+1$ for even $i$. Put $\epsilon =n\mathrm{mod}2$ and

$$a(n)=\frac{n^2}{12}(3(1+n^2)-2(2+n^2)\epsilon ).$$

Statement echo

All declaration names in this table have prefix D5.S3.Quantum.Matrix.. The source calls the two coefficient/minor descriptions equivalent views of the first conjecture. No additional source conjecture is counted from those equivalent descriptions.

Motivation

The two conjectures ask for uniform identities across every matrix order. A common two-dimensional factorization explains both the second coefficient and the disappearance of all higher coefficients. The settlements correspond to preregistrations #21795 and #21796.

Gap

The source labels the two statements conjectures. No settlement was located in the readable literature scope recorded in those preregistrations. Literature completeness is ASSUMED-UNVERIFIED. The formal statements use the preregistered characteristic-coefficient convention, rather than a separately constructed exterior-power operator or a separately formalized trace/minor equivalence.

Route

Over $\mathbb{Q}$, set $w_i=i-(n+1)/2$, $u_i=ni-(n-1)/2$, and $s_i=(-1{)}^{i+1}$ for source indices $i=1,\dots ,n$. Let the $i$th row of $U$ be $(u_i,s_i)$ and the $j$th column of $V$ be $(1,w_j)$. The entry identity $M=UV$ is the private factorization lemma of the second-trace module. The public charpoly_factor applies Matrix.charpoly_mul_comm_of_le to give, for $n\ge 2$,

$${\chi }_{M_{\mathbb{Q}}}(x)=x^{n-2}{\chi }_{VU}(x).$$

The private centered-moment lemmas evaluate the four entries of $VU$ as

$$VU=\left(\begin{array}{cc}n(n^2+1)/2& \epsilon \\ n^2(n^2-1)/12& -n(1-\epsilon )/2\end{array}\right).$$

The private small_det and coefficient_two give $[x^{n-2}]{\chi }_M=-a(n)$, after the rational scalar map. The private a_nonneg gives $a(n)\ge 0$. The first result therefore proves the absolute-value formula. The second result uses charpoly_factor and Polynomial.coeff_X_pow_mul' to annihilate every coefficient indexed by $k>2$ with $k\le n$; for $k>n$ the defining zero branch applies.

Falsifier

A counterexample to the first binding claim would have $n>1$ and an integer second trace whose absolute value, cast to $\mathbb{Q}$, differs from $a(n)$. A counterexample to the second would have natural $n,k$ with $k>2$ and nonzero binding exterior trace. The two universal result theorems exclude these counterexamples within the stated convention.

Evidence

Settlement: Proved, by D5.S3.Quantum.Matrix.SpeziaSerpentineHigherExteriorTrace.result. The companion settlement is the other module’s result. Both modules have generality: I and utility: none: their assertions quantify unbounded orders and contain no fixed numerical certificate.

The public theorem surface includes the frozen owner’s alternating_sum, the second-trace module’s charpoly_factor and result, and the higher-trace module’s result. Every other lemma is private. The escape audits of these four theorem statements are unfinished: alternating_sum is tracked in issue #22464, and the three serpentine declarations are tracked in issue #21995. No validated four-slot registration is asserted.

Exact finite computation

The immutable experiment is spezia-a322844 at commit 72e99409d60c1747efec95cc67de4f5dd612c133. The committed check.py bytes have the SHA-256 below. The implementation seat ran python3 /tmp/op-sp322844/check.py, exit 0, final verdict ALL_CHECKS_OK. Script SHA-256: 2573b4928f9051382c4692a3d3d1680b30d477d8d5d8c898145398a8d08f5159.

The exact tested scope is $0\le n\le 40$ and $3\le k\le 42$: 10,660 principal two-minors, 101,270 principal three-minors, 741 higher coefficients, and all 1,816 principal minors of order at least three for $n\le 10$. Exact ranks in this range are $\min (n,2)$. These computations are finite evidence, separate from the universal Lean theorems.

Triage

1. Proved (kernel-checked): centered rational factorization. The second-trace module’s private factorization proves $M_{\mathbb{Q}}=UV$ for every $n$, with dimensions $n\times 2$ and $2\times n$.
2. Proved (kernel-checked): the second coefficient and absolute-value claim. Its private coefficient_two gives $[x^{n-2}]{\chi }_M=-a(n)$ for $n\ge 2$, its private a_nonneg gives $a(n)\ge 0$, and its public result gives exactly the first binding claim.
3. Proved (kernel-checked): every higher exterior trace vanishes. D5.S3.Quantum.Matrix.SpeziaSerpentineHigherExteriorTrace.result covers every natural $n$ and $k>2$, including $n<k$.
4. Computed: the exact finite checks. The experiment entry above records the command, exit 0, script hash, ALL_CHECKS_OK, and the complete tested scope and all four counts. It also checks rank $\min (n,2)$ for $0\le n\le 40$; no uniform exact-rank theorem is inferred from this computation.
5. Open (formalization boundary): separate exact rank and complete expanded characteristic polynomial. Neither a separate uniform exact-rank theorem nor a separately expanded full characteristic-polynomial theorem is delivered. These are neighbouring formalization tasks, not assertions that the corresponding elementary mathematical facts are unknown.

What the settlement shows

Proved (kernel-checked): the decisive mechanism is factorization through dimension two, followed by the signed coefficient identity and the nonnegativity needed for absolute value. The companion higher-trace settlement follows from the same public charpoly_factor; it needs no bound on $n$ and includes $n<k$. The first claim retains the source’s $n>1$ guard.

Computed: exact ranks are $\min (n,2)$ for $0\le n\le 40$, with evidence in the experiment entry. Open (formalization boundary): a uniform exact-rank theorem, a separately expanded full characteristic polynomial, and an exterior-power operator realization are outside this delivery.

The source identifies no further theorem conditional on these two conjectures. The result changes their status in the characteristic-coefficient formulation; it makes no claim about unrelated Spezia matrix families or a new general rectangular-product identity.

ASSUMED-UNVERIFIED

Literature completeness is ASSUMED-UNVERIFIED. The preregistrations report readable OEIS, arXiv metadata, Crossref, MathOverflow, Math StackExchange, repository and GitHub-code scopes without a located settlement. OpenAlex and Semantic Scholar requests returned HTTP 429, arXiv full-text and general-web searches were unavailable or unusable, and the later-author bibliography was incomplete. No exhaustive citation inventory, priority claim, or identification of the OEIS contributor with a same-named paper author is asserted. No source DOI, arXiv manuscript or journal version is identified.

The standard exterior-power/coefficient interpretation is the binding source convention. A constructed exterior-power linear map and a separate formal equivalence to its trace are not supplied. The unfinished audit in #21995 concerns registration evidence, not the kernel-checked mathematical proof.