Metadata

slug: sp330700
bibkey: spezia2019a330700
doi: null
url: https://oeis.org/A330700
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Matrix/SpeziaPerimeterHigherExteriorTraces.result

Higher exterior traces of Spezia’s perimeter matrix

Problem

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 $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 $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 \leq 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.

Motivation

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.

Gap

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.

Route

For source indices $1 \leq i, j \leq n$ , put $v_{i} = i$ and $w_{i} = max (i - 2, 0)$ . Then

$M (n) = v v^{T} - w w^{T} = A B, A = [v w], B = [v^{T} - w^{T}] .$

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.

Falsifier

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.

Evidence

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 \leq i, j \leq 40$ ; 22,140 entry-factorization checks for $0 \leq n \leq 40$ ; 741 higher characteristic coefficients for $3 \leq k \leq n \leq 40$ ; 899 empty-space cases for $0 \leq n \leq 40$ , $3 \leq k \leq 42$ , $k > n$ ; 1,816 principal minors of order at least three for $n \leq 10$ ; and 3,747 higher compound entries for $3 \leq n \leq 7$ . The 38 principal minors on ${1, 3}$ for $3 \leq n \leq 40$ 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.

Triage

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 \leq n \leq 40$ . 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.

ASSUMED-UNVERIFIED

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.

Keyboard shortcuts

trureturing — Discovering truth