Higher exterior traces of Spezia's perimeter matrix

Stefano Spezia's OEIS A330700, COMMENTS, revision 23, gives this second line in its Conjectures block:

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

The same block and OEIS A330287, COMMENTS, revision 31, specify:

The matrix M(n) is defined as M[i,j,n] = ij if i < 3 or j < 3 and M[i,j,n] = 2(i + j) - 4 otherwise.

Indices are one-based. For every positive natural $n$, interpret the integer entries in $\mathbb C$ and take every natural $k>2$, including $k>n$. The exterior power is represented by the existing compoundMatrix; its trace is Matrix.trace. The target is exactly this second conjecture, as preregistered in #21999.

Statement echo

| Source clause or convention | Lean counterpart | Fidelity | | --- | --- | --- | | The literal piecewise entry formula | SpeziaPerimeterHigherExteriorTraces.M | Source indices are i.val+1, j.val+1; the comparison is in natural numbers and entries and subtraction are in $\mathbb C$. | | A square matrix of positive order | claim quantifies over natural $n>0$ | Positivity is the explicit preregistered scope. | | Every exterior order $k>2$ | claim quantifies over natural $k>2$ | No upper bound $k\le n$ is added. | | Trace of the exterior power equals zero | Matrix.trace (compoundMatrix (M n) k) equals zero | The existing ordered-subset basis also includes the empty-space case. | | The universal conjecture holds | SpeziaPerimeterHigherExteriorTraces.result | The theorem proves claim without factorization or rank hypotheses. |

The settling GID is D5/S3/Quantum/Matrix/SpeziaPerimeterHigherExteriorTraces.result. The source note is spezia2019a330700. This is a universal symbolic statement about a source-defined family; it is not a finite certificate.

The bounded source and literature screen in #21999 identifies no settlement in its readable searched scope. The general compound-matrix construction and rectangular Cauchy–Binet formula are classical and already available in D5.S3.Quantum.Schatten.CompoundMatrices; the source-specific entry identity supplies the application. Literature completeness remains ASSUMED-UNVERIFIED.

For source indices $1\le i,j\le n$, put $v_i=i$ and $w_i=\max(i-2,0)$. Then

$$M(n)=vv^{\mathsf T}-ww^{\mathsf T}=AB,\qquad A=[v;w],\qquad B=\begin{bmatrix}v^{\mathsf T}\-w^{\mathsf T}\end{bmatrix}.$$

If $i<3$ or $j<3$, at least one of $w_i,w_j$ is zero, so this entry equals $ij$. Otherwise

$$ij-(i-2)(j-2)=2(i+j)-4.$$

These are precisely the two branches of the public matrix definition. For any $k$-element row and column subsets $S,T$, restriction gives $M[S,T]=A[S,:]B[:,T]$. The imported cauchyBinet writes its determinant as a sum indexed by $k$-element subsets of a two-element set. For $k>2$ there are no such subsets, hence every such determinant is zero. Thus the entire higher compound matrix is zero. The live local facts factor, hempty and hz implement this derivation inside result; they are not separately published theorems. Taking the trace gives the claimed zero. For $k>n$, no $k$-element row or column subset exists and the trace is an empty sum.

A positive natural $n$ and natural $k>2$ with a nonzero exterior trace of the literal matrix would refute the claim. Finite agreement, the vanishing of only the full determinant, or a rank hypothesis assumed rather than proved would not settle it.

The named kernel theorem is D5.S3.Quantum.Matrix.SpeziaPerimeterHigherExteriorTraces.result. Its proof applies the existing compoundMatrix, cauchyBinet, Matrix.submatrix_mul, card_finset_fin_le, finite-sum elimination and Matrix.trace_zero. The result is classified bind-only; its admission basis is open-problem-resolution (#21999; Proved), with generality: I and utility: none.

The escape audit is unfinished for the sole public theorem result: #22170. The original guarded telescope has no delivered source reconstruction, realization bridge, actual-positive law, whole-family variation, slot sensitivity or observational-dependence evidence. No Reg registration or declared_validated status is claimed.

Finite experiment

The independent program and data are in trureturing-experiments at f4a398f72a5e051252b37b9c34f9958599594ca5. The script is docs/reports/spezia-a330700-exterior-traces/check.py, SHA-256 d42745479718c59b0f7fbd52dfc4e4d52d235b4b925d329868716da9fc073288. Its bytes were checked against that commit. Command: (cd /Users/auric/trureturing-experiments && python3 docs/reports/spezia-a330700-exterior-traces/check.py); exit 0, ALL_CHECKS_OK, Python 3.14.8, SymPy 1.14.0.

The finite scope is: 1,600 geometric perimeter comparisons for $1\le i,j\le40$; 22,140 entry-factorization checks for $0\le n\le40$; 741 higher characteristic coefficients for $3\le k\le n\le40$; 899 empty-space cases for $0\le n\le40$, $3\le k\le42$, $k>n$; 1,816 principal minors of order at least three for $n\le10$; and 3,747 higher compound entries for $3\le n\le7$. The 38 principal minors on ${1,3}$ for $3\le n\le40$ equal $-1$. At $n=3$ the second exterior trace is $-5$ and the source's separate scalar formula is $29$. These finite computations do not supply the universal proof.

What the settlement shows

| Target item | Status and evidence kind | Result and scope | | --- | --- | --- | | Mechanism | Proved in prose in Route; the trace conclusion is kernel-checked by result | The literal matrix factors through two columns. Cauchy–Binet has no intermediate $k$-subset for $k>2$, so the whole higher compound matrix vanishes before taking its trace. | | Extent | Proved in prose in Route | The argument covers every higher mixed minor for every positive $n$ and $k>2$, including the vacuous $k>n$ case. The local hz is used in result; no separate minor theorem is delivered. | | Surviving second exterior order | Computed by the finite experiment above, exit 0 and the stated SHA-256 | The second trace at $n=3$ is $-5$; the ${1,3}$ principal minor is $-1$ for each $3\le n\le40$. Higher-order vanishing is not a zero-matrix artifact. | | Separate first conjecture | Computed by the same finite experiment, exit 0 and the stated SHA-256 | At $n=3$ the literal scalar formula is $29$, while the absolute second trace is $5$. This diagnostic is separate from the proved second conjecture. | | Unformalized neighbours | Open as separately delivered formal results | Uniform exact rank two and an exact second-exterior-trace formula have no separately delivered Lean statements here. |

The source lists no theorem conditional on this conjecture. Its scalar definitions and generating functions acquire no additional proof from this settlement. The separate first conjecture and other sequences retain their own statements.

Literature status is partial. Completeness of citing-work discovery, author identification and full-text coverage is ASSUMED-UNVERIFIED: #21999 records rate-limited OpenAlex and Semantic Scholar queries, unusable web full-text results, and bounded arXiv, Crossref, MathOverflow, MathDB and repository screens. No exhaustive priority claim is made. No DOI or arXiv identifier is assigned to this OEIS source. The unfinished escape audit remains #22170.