From 025e0a934635dbcd0e1321dba36decdd96235c9a Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Wed, 11 Nov 2026 12:49:19 +0000
Subject: [PATCH] feat(research): bound sparse tensor annihilator heights

---
 .../PROOF.md                                  | 148 +++++++++
 .../README.md                                 | 179 +++++++++++
 .../SOURCES.json                              |  30 ++
 .../TASK.json                                 | 107 +++++++
 .../VERIFY.json                               |  34 +++
 .../verify.py                                 | 280 ++++++++++++++++++
 6 files changed, 778 insertions(+)
 create mode 100644 research/sparse-tensor-annihilator-heights/PROOF.md
 create mode 100644 research/sparse-tensor-annihilator-heights/README.md
 create mode 100644 research/sparse-tensor-annihilator-heights/SOURCES.json
 create mode 100644 research/sparse-tensor-annihilator-heights/TASK.json
 create mode 100644 research/sparse-tensor-annihilator-heights/VERIFY.json
 create mode 100644 research/sparse-tensor-annihilator-heights/verify.py

diff --git a/research/sparse-tensor-annihilator-heights/PROOF.md b/research/sparse-tensor-annihilator-heights/PROOF.md
new file mode 100644
index 0000000000..0a58d2aa74
--- /dev/null
+++ b/research/sparse-tensor-annihilator-heights/PROOF.md
@@ -0,0 +1,148 @@
+# Sparse supports retain the coefficient-height obstruction
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+Put pi=2+i, rho=2-i and alpha=pi/rho=(3+4i)/5. These are the
+fixed Gaussian primes and generator of zxv's #5436. Nick Petalas's
+#5934 determines the coefficient heights for consecutive powers. The
+new result allows every strictly increasing integer exponent support,
+including arbitrarily high degree and Laurent supports, at the same
+minimum term count. Gaussian unique factorization and the Vandermonde
+determinant are classical inputs.
+
+## Statement
+
+Let f>=1, n=f+1, and m_0<...<m_n be integers. Set
+delta_s=m_(s+1)-m_s for 0<=s<n. There is a unique nonzero relation
+line over Q(i)
+
+    sum_(j=0)^n c_j alpha^(k m_j)=0,   k=0,...,n-1.
+
+Its primitive Gaussian-integer coefficient vector c is unique up to a
+Gaussian unit. Every c_j is nonzero, and its exact valuations are
+
+    A_j = v_pi(c_j)  = sum_(s=j)^(n-1) (n-1-s) delta_s,
+    B_j = v_rho(c_j) = sum_(s=0)^(j-1) s delta_s.
+
+Empty sums are zero. In particular the primitive vector's total
+split-prime valuation mass is exactly
+
+    M(m) = sum_j (A_j+B_j)
+         = sum_(s=0)^(n-1) [n-1+2s(n-1-s)] delta_s.
+
+Consequently
+
+    M(m) >= 2 binom(n+1,3),
+
+with equality if and only if every delta_s=1. Thus consecutive supports,
+up to translation, uniquely minimize this valuation mass. This optimizes
+that exact arithmetic quantity, not the actual largest complex modulus.
+
+Every nonzero Gaussian-integer relation on this support, primitive or
+otherwise, satisfies
+
+    |c_j|^2 >= 5^(A_j+B_j),
+    max_j |c_j| >= 5^(binom(n,2)/2),
+    sum_j log_2 |c_j| >= log_2(5) binom(n+1,3).
+
+Here A_j,B_j refer to the primitive vector. For a nonprimitive relation
+the actual valuations can only increase. The inequalities therefore
+exclude an asymptotic improvement of the quadratic maximum coefficient
+bit height or cubic explicit coefficient-list storage merely by choosing
+nonconsecutive powers. The consecutive upper bounds are prior #5934.
+
+For D=diag(1,alpha), the eigenvalues of D^tensor f are exactly
+alpha^k for k=0,...,f. Since (D^m)^tensor f=(D^tensor f)^m for every
+integer m, these are exactly the coefficient relations among the n+1
+specified lifted powers. No physical tensor array needs to be stored
+to state this implication.
+
+## Vandermonde cofactors and primitive normalization
+
+Write x_j=alpha^m_j. These numbers are distinct: v_pi(alpha)=1, so
+alpha^t=1 implies t=0. The matrix with entries x_j^k has n rows
+and n+1 columns. Any n-column minor is the nonzero Vandermonde product
+
+    Delta_j = product_(a<b; a,b != j) (alpha^m_b-alpha^m_a).
+
+It therefore has rank n. Its signed minors (-1)^j Delta_j give a
+nonzero kernel vector, and all its coordinates are nonzero. A common
+denominator gives a Gaussian-integer vector. Divide by its Gaussian
+greatest common divisor to obtain a primitive vector. Because Z[i] is
+a principal ideal domain, any other integral vector on this rational
+line is an integral multiple of the primitive one. One way to see the
+last assertion is to take a Gaussian-integer Bezout combination of the
+primitive entries equal to 1 and apply it to the proposed multiple.
+
+For a<b,
+
+    alpha^m_b-alpha^m_a
+      = alpha^m_a (alpha^(m_b-m_a)-1).
+
+The parenthesized factor has pi valuation zero: its first summand has
+positive valuation and its second has valuation zero. At rho, those
+summands have distinct valuations -(m_b-m_a) and zero. Hence
+
+    v_pi(alpha^m_b-alpha^m_a)=m_a,
+    v_rho(alpha^m_b-alpha^m_a)=-m_b.
+
+This also holds for negative m_a. It follows that
+
+    L_j = v_pi(Delta_j)  = sum_(a<b; a,b != j) m_a,
+    -U_j = v_rho(Delta_j) = -sum_(a<b; a,b != j) m_b.
+
+For any prime, primitive normalization subtracts the minimum valuation
+over all coordinates. Common factors at other Gaussian primes have
+zero valuation at pi and rho and do not change this calculation.
+
+The minimum L_j is L_n, and the maximum U_j is U_0. To compute the
+differences, compare sorted exponent lists before and after omitting
+one element. In an n-element list, the exponent in slot t contributes
+n-1-t times to L and t times to U. Therefore
+
+    L_j-L_n = sum_(s=j)^(n-1) (n-1-s)(m_(s+1)-m_s),
+    U_0-U_j = sum_(s=0)^(j-1) s(m_(s+1)-m_s).
+
+These nonnegative formulas also prove the asserted extrema. They are
+the claimed A_j and B_j, including the ties A_(n-1)=A_n=0 and
+B_0=B_1=0. Translation of the support cancels from both differences.
+
+## Sharp valuation mass and storage consequences
+
+In sum_j A_j, gap delta_s occurs for j=0,...,s, with weight n-1-s.
+In sum_j B_j it occurs for j=s+1,...,n, with weight s. Its combined
+weight is
+
+    (s+1)(n-1-s)+(n-s)s = n-1+2s(n-1-s).
+
+Every weight is strictly positive because n>=2. Every integer gap is
+at least one. Setting every gap to one gives
+
+    A_j=binom(n-j,2),   B_j=binom(j,2),
+    sum_j (A_j+B_j)=2 binom(n+1,3).
+
+Thus this is the sharp minimum mass, and equality forces every gap to
+one. Any missing power strictly increases the mass by the exact
+weighted gap excess
+
+    sum_s [n-1+2s(n-1-s)] (delta_s-1).
+
+A nonzero Gaussian integer with valuations A,B at pi,rho has norm
+at least 5^(A+B), since the remaining factor has positive integer norm.
+This proves the coefficient bounds. For the maximum bound use
+A_0>=binom(n,2) or B_n>=binom(n,2). Summing logarithms gives the
+displayed cubic lower bound.
+
+For an explicit binary coordinate encoding put
+h(c)=log_2 max(1,|Re c|,|Im c|). Since
+max(|Re c|,|Im c|)>=|c|/sqrt(2),
+
+    max_j h(c_j) >= binom(n,2) log_2(5)/2 - 1/2,
+    sum_j h(c_j) >= log_2(5) binom(n+1,3) - (n+1)/2.
+
+Thus even a sparse list containing only the n+1 nonzero coefficients
+needs Omega(f^3) coefficient bits. Recording exponents adds costs and
+cannot remove this lower bound. This is not a lower bound for factored,
+compressed or streamed descriptions, nor for approximate cancellation,
+other generators or relations with more than f+2 terms. It does not
+price a productive native consumer or change the selected frontier.
diff --git a/research/sparse-tensor-annihilator-heights/README.md b/research/sparse-tensor-annihilator-heights/README.md
new file mode 100644
index 0000000000..ef6fea5c92
--- /dev/null
+++ b/research/sparse-tensor-annihilator-heights/README.md
@@ -0,0 +1,179 @@
+# Exact coefficient valuations for every sparse tensor support
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Choosing nonconsecutive powers cannot reduce the quadratic maximum coefficient
+bit height or cubic explicit coefficient-list storage order of the fixed
+Gaussian-rational minimum-term tensor relation. The new theorem computes
+every coefficient's two split-prime valuations for every integer exponent
+support. Consecutive supports uniquely minimize their total valuation mass,
+up to translation.
+
+Claim type: scoped written proof with exact finite corroboration. This answers
+the arithmetic-order part of Open next question 2 in
+[Nick Petalas's #5934](https://github.com/CrocSwap/integer-mult-bounds/pull/5934).
+That result covers consecutive powers. The new proof covers arbitrary gaps,
+arbitrarily high degree and Laurent supports at the same term count. Actual
+complex-height minimization remains open. No new kappa or supplier admission
+is claimed.
+
+## Result
+
+Let f>=1, n=f+1, alpha=(3+4i)/5 and D=diag(1,alpha). Choose any integers
+m_0<...<m_n and put delta_s=m_(s+1)-m_s. The unique primitive
+Gaussian-integer relation, up to a Gaussian unit,
+
+```text
+sum_(j=0)^n c_j (D^m_j)^tensor f = 0
+```
+
+has no zero coefficients. At pi=2+i and rho=2-i its exact valuations are
+
+```text
+A_j = v_pi(c_j)  = sum_(s=j)^(n-1) (n-1-s) delta_s
+B_j = v_rho(c_j) = sum_(s=0)^(j-1) s delta_s
+
+sum_j (A_j+B_j)
+  = sum_(s=0)^(n-1) [n-1+2s(n-1-s)] delta_s
+  >= 2 binom(n+1,3).
+```
+
+Every gap weight is positive. Equality holds exactly when all gaps equal
+one. Each extra missing power raises the mass by its displayed weight.
+Other Gaussian prime factors are not determined by this formula.
+
+Every nonzero integral relation on the support, including nonprimitive
+multiples, consequently satisfies
+
+```text
+|c_j|^2 >= 5^(A_j+B_j)
+max_j |c_j| >= 5^(binom(n,2)/2)
+sum_j log_2 |c_j| >= log_2(5) binom(n+1,3).
+```
+
+The last inequality gives an Omega(f^3) lower bound even when a list stores
+only the f+2 nonzero coefficients. The consecutive upper bounds from #5934
+make both orders sharp. A factored or streaming representation has a
+different storage contract.
+
+For f=2 and support (0,1,3,4), one primitive relation has coefficients
+
+```text
+(24+7i), (-24+18i), (-24-18i), (24-7i).
+```
+
+Their valuation pairs are (4,0), (2,0), (0,2), (0,4). The mass is 12;
+the minimum at this width is 8. This sample is generated by the verifier.
+[PROOF.md](PROOF.md) gives the universal Vandermonde and normalization argument.
+
+## Exact finite evidence
+
+The new standalone verifier imports no predecessor executable. It constructs
+the signed Vandermonde cofactors and separately solves the literal rational
+kernel with its last coefficient fixed to one. Gaussian-integer gcd
+normalization makes the resulting vectors directly comparable.
+
+Its census has 246 supports, including 240 nonconsecutive ones:
+
+- All supports containing zero with n=2,...,5 and remaining exponents chosen
+  from {1,...,8}.
+- Four specified gap families for each n=6,...,9.
+- Translations by -7 and 11 of the first ten small supports, including
+  Laurent examples.
+
+It checks 1,190 coefficient occurrences and 944 exact root residuals, plus
+1,776 literal diagonal entries of the lifted operators for the small and
+translated supports. These counts refer to the main census; the printed
+sample and rejection controls run separately. It checks the weighted mass,
+its sharp equality condition and the coefficient norm lower bounds.
+
+Thirteen controls reject invalid supports, an altered coefficient, a missing
+coefficient, nonprimitive scaling, a zero coefficient and conjugated
+coefficients. All scientific checks use explicit exceptions and remain
+enabled under optimized Python. The all-width and all-support quantifiers
+rest on the written proof. Finite enumeration is corroboration.
+
+## Reproduce
+
+From the repository root with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sparse-tensor-annihilator-heights/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sparse-tensor-annihilator-heights/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sparse-tensor-annihilator-heights
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sparse-tensor-annihilator-heights --check-source-history
+```
+
+Other hosts may substitute their CPython 3.12 interpreter path. Direct replay
+prints `PASS_SPARSE_TENSOR_ANNIHILATOR_HEIGHTS` in a generated JSON receipt
+bound to all six package files. It writes nothing, needs no Git and imports
+no sibling package. The registered runner also checks historical source
+provenance and prints `PASS_REGISTERED_RESEARCH_PACKAGE`. No receipt is
+hand-written or accepted in place of recomputation.
+
+## Scope and implementation limits
+
+The generator alpha, exact equality, Q(i) coefficient field and term count
+f+2 are fixed. More terms, approximate relations and other generators need
+new analysis. The result optimizes split-prime valuation mass; it does not
+claim that consecutive supports minimize every coefficient's actual modulus.
+It supplies neither a productive consumer nor coefficient generation,
+precision, field-pass, restoration, tape or native costs. The five selected
+framework assumptions remain. Independent human and formal proof-kernel
+review are unclaimed. Selected cold replay, predecessor scientific suites,
+Lean and Docker are unrun and outside this claim.
+
+The verifier has no recursion, subprocesses or generated code. Its finite
+domain has at most ten coefficients, a nine-row rational system, exponents
+of absolute value at most 128 and support span at most 64. General power
+evaluation has a 1,024-step limit. Gaussian Euclidean division halves each
+positive remainder norm, and both gcd and prime division have explicit
+bit-length iteration bounds. Functions are below sixty physical lines.
+Python's managed arithmetic allocates dynamically, a Power-of-Ten rule 3
+deviation. These fixed domains bound live data; there is no persistent cache
+or mutable shared state. Warning-strict normal and optimized execution and
+in-memory syntax compilation provide the available diagnostics.
+
+The canonical base is e54523517d0f03e58352e647c403a5af3e525a57, priority
+revision 8. The selected binding orientation passed and selects #7000 at
+conditional kappa 0.00363005817. The historical card context predates that
+selection. [TASK.json](TASK.json) declares the change from the helper-inventory
+card to this arithmetic side result. [SOURCES.json](SOURCES.json) pins the
+question, predecessor proof, catalogue and selected record as provenance.
+There are no live external executable inputs.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541730)
+preceded substantial work. Live claims, local reservations, open/account PRs,
+merged searches and main-tree general-support searches were checked. The
+cached scan fully paginated 545 open PRs and 7,202 Discussion records but
+covered only 196 of 10,178 local note paths. Separate main-tree searches
+covered the distinctive object, arbitrary supports, powers and heights.
+Arbitrary historical diffs and unpublished work remain outside this coverage.
+
+## Open next questions
+
+- Do consecutive supports minimize the actual maximum primitive coefficient
+  modulus? Start at f=2 with the extra prime factors of the four cofactors.
+  A bound on those factors is missing; the sharp valuation objective alone
+  does not settle that comparison.
+- Can one productive consumer use a factored or streamed relation? Specify
+  its endpoint and charge arithmetic, passes, precision and restoration.
+  A complete physical consumer is missing, and an identity producing zero
+  is not itself that consumer.
+
+Structured relevance, first steps and blockers are in [TASK.json](TASK.json).
+
+## Credit
+
+Credit Nick Petalas #5934 for the original two-prime valuation method,
+consecutive-support theorem and explicit sparse-support question; zxv #5436
+for the fixed-generator tensor escape and coefficient-pricing question;
+Anthony Chefles for classical multi-copy independence; and classical
+Vandermonde, Gaussian-integer and valuation methods. The retained native
+and control lineage includes Chris R, Ali Romman, Dillon Amburgey,
+David Ganz, Cinna Davis, Cao Yifan, Jacob Alan Sussman and the source-specific
+contributors. Their results are cited premises, not audit deliverables.
+All predecessor bytes and credit remain unchanged.
+
+The arbitrary-support formula, sharp weighted-gap optimization, storage
+consequence and new verifier were produced by Nick Petalas.
diff --git a/research/sparse-tensor-annihilator-heights/SOURCES.json b/research/sparse-tensor-annihilator-heights/SOURCES.json
new file mode 100644
index 0000000000..35ac4bfcda
--- /dev/null
+++ b/research/sparse-tensor-annihilator-heights/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/support-width-dichotomy/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "15533e0c9c0c48e53cc2eca09ffa64a391628fb1",
+      "sha256": "24482756f27c4ca1e24c37933459dbddad7dde9b81bffa5b62cfd6a6b8d28b93"
+    },
+    {
+      "path": "research/tensor-annihilator-height/README.md",
+      "usage": "provenance",
+      "git_blob": "8990c716a1c89a2b4df93db5f544b5cf3a895b32",
+      "sha256": "8ea606050ee3203ccf94718f4fc47b80945a724a9985a056a9c206fb1a330f36"
+    }
+  ]
+}
diff --git a/research/sparse-tensor-annihilator-heights/TASK.json b/research/sparse-tensor-annihilator-heights/TASK.json
new file mode 100644
index 0000000000..b07f898bfd
--- /dev/null
+++ b/research/sparse-tensor-annihilator-heights/TASK.json
@@ -0,0 +1,107 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "productive helper",
+      "target refinement",
+      "5599",
+      "5614"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact split-prime coefficient valuations for every minimum-term integer-power support of the fixed Gaussian-rational tensor generator, and the sharp weighted-gap valuation-mass minimum.",
+  "scope_change_reason": "A side result answering Open next question 2 of merged PR5934. The task is arithmetic coefficient pricing for the PR5436 growing-support escape, rather than an emitted productive helper inventory or supplier admission.",
+  "bottleneck_link": "Choosing a sparse support cannot lower the quadratic maximum coefficient height or cubic explicit-list storage order for this minimum-term escape. This constrains one proposed coefficient-pricing route but supplies no productive consumer or physical invoice.",
+  "budget_minutes": 60,
+  "stop_rule": "Package the first proved arbitrary-support valuation and storage obstruction with bounded exact corroboration; leave actual complex-height optimization and physical consumer design open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the all-support theorem. verify.py checks 246 supports by Vandermonde cofactors and separate exact rational kernel elimination, 1190 coefficient occurrences, 944 root residuals, 1776 literal tensor diagonal entries and 13 rejected controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Do consecutive supports minimize the actual largest primitive coefficient modulus, rather than just the split-prime valuation mass?",
+      "why_it_matters": "Other Gaussian prime factors are absent from the exact valuation objective, so its minimizer need not settle the actual modulus.",
+      "first_step": "Fix f=2 and bound the extra prime factors of the four Vandermonde cofactors after primitive normalization.",
+      "blocked_by": "A sharp modulus argument controlling primes other than 2+i and 2-i."
+    },
+    {
+      "question": "Can a priced productive consumer use a factored or streaming relation without materializing the coefficient list?",
+      "why_it_matters": "The cubic storage obstruction applies to an explicit coefficient list and leaves these representations open.",
+      "first_step": "Specify one consumer endpoint and account for arithmetic, field passes, precision and restoration.",
+      "blocked_by": "A productive consumer and its complete physical bill."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541730",
+  "claim_type": "scoped written proof with exact finite corroboration",
+  "predecessors": [
+    {
+      "pr": 5934,
+      "author": "Nick Petalas",
+      "role": "Valuation method, consecutive-support theorem and explicit sparse-support question."
+    },
+    {
+      "pr": 5436,
+      "author": "zxv",
+      "role": "Fixed-generator minimum-term tensor escape and coefficient-pricing question."
+    }
+  ],
+  "environment": {
+    "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12",
+    "version": "3.12.15",
+    "dependencies": "Python standard library only"
+  },
+  "overlap": {
+    "canonical_main": "e54523517d0f03e58352e647c403a5af3e525a57",
+    "open_prs": 545,
+    "discussion_records": 7202,
+    "remote_pagination": "complete at 2026-11-11T12:41:05Z and 12:42:26Z",
+    "local_scan": "196 of 10178 note paths materialized; separate origin/main README searches covered sparse/nonconsecutive annihilators, coefficient heights and general exponent supports.",
+    "limits": "No arbitrary historical diff or unpublished-work coverage. No recent account PR references the source or shares this fixed-generator support model."
+  }
+}
diff --git a/research/sparse-tensor-annihilator-heights/VERIFY.json b/research/sparse-tensor-annihilator-heights/VERIFY.json
new file mode 100644
index 0000000000..a5510ce833
--- /dev/null
+++ b/research/sparse-tensor-annihilator-heights/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Full bounded arbitrary-support census, independent kernel comparison, exact valuations, tensor entries, sharp mass equality and all controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same complete checks with optimization; all scientific contracts use explicit exceptions."
+    }
+  ]
+}
diff --git a/research/sparse-tensor-annihilator-heights/verify.py b/research/sparse-tensor-annihilator-heights/verify.py
new file mode 100644
index 0000000000..d29f7aaf91
--- /dev/null
+++ b/research/sparse-tensor-annihilator-heights/verify.py
@@ -0,0 +1,280 @@
+#!/usr/bin/env python3
+"""Exact finite corroboration of the arbitrary-support valuation theorem."""
+
+from fractions import Fraction
+from hashlib import sha256
+from itertools import combinations
+import json
+from math import comb, lcm
+from pathlib import Path
+
+
+Q = tuple[Fraction, Fraction]
+Z = tuple[int, int]
+ZERO: Q = (Fraction(0), Fraction(0))
+ONE: Q = (Fraction(1), Fraction(0))
+ALPHA: Q = (Fraction(3, 5), Fraction(4, 5))
+PI: Z = (2, 1)
+RHO: Z = (2, -1)
+
+
+def require(ok: bool, message: str) -> None:
+    if not ok:
+        raise ValueError(message)
+
+
+def add(a: Q, b: Q) -> Q:
+    return a[0] + b[0], a[1] + b[1]
+
+
+def neg(a: Q) -> Q:
+    return -a[0], -a[1]
+
+
+def mul(a: Q, b: Q) -> Q:
+    return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]
+
+
+def div(a: Q, b: Q) -> Q:
+    norm = b[0] ** 2 + b[1] ** 2
+    require(norm != 0, "division by zero")
+    return (a[0] * b[0] + a[1] * b[1]) / norm, (a[1] * b[0] - a[0] * b[1]) / norm
+
+
+def power(a: Q, exponent: int) -> Q:
+    require(type(exponent) is int and abs(exponent) <= 1024, "power bound")
+    if exponent < 0:
+        a = div(ONE, a)
+    result = ONE
+    for _ in range(abs(exponent)):
+        result = mul(result, a)
+    return result
+
+
+def zmul(a: Z, b: Z) -> Z:
+    return a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]
+
+
+def norm(a: Z) -> int:
+    return a[0] ** 2 + a[1] ** 2
+
+
+def exact_div(a: Z, b: Z) -> Z:
+    d = norm(b)
+    require(d > 0, "integer division by zero")
+    r, s = a[0] * b[0] + a[1] * b[1], a[1] * b[0] - a[0] * b[1]
+    require(r % d == 0 and s % d == 0, "inexact Gaussian division")
+    return r // d, s // d
+
+
+def gcd_pair(a: Z, b: Z) -> Z:
+    # Nearest-coordinate division halves the positive remainder norm.
+    for _ in range(norm(b).bit_length() + 2):
+        if b == (0, 0):
+            return a
+        d = norm(b)
+        r, s = a[0] * b[0] + a[1] * b[1], a[1] * b[0] - a[0] * b[1]
+        quotient = ((2 * r + d) // (2 * d), (2 * s + d) // (2 * d))
+        product = zmul(quotient, b)
+        remainder = a[0] - product[0], a[1] - product[1]
+        require(2 * norm(remainder) <= d, "Euclidean descent")
+        a, b = b, remainder
+    raise ValueError("Euclidean step budget exhausted")
+
+
+def content(coefficients: tuple[Z, ...]) -> Z:
+    require(1 <= len(coefficients) <= 10, "content size")
+    result = (0, 0)
+    for value in coefficients:
+        result = gcd_pair(result, value)
+    return result
+
+
+def primitive(values: tuple[Q, ...]) -> tuple[Z, ...]:
+    require(3 <= len(values) <= 10, "primitive size")
+    denominator = 1
+    for a, b in values:
+        denominator = lcm(denominator, a.denominator, b.denominator)
+    cleared = tuple((a * denominator, b * denominator) for a, b in values)
+    require(all(a.denominator == b.denominator == 1 for a, b in cleared), "denominator clearing")
+    integral = tuple((a.numerator, b.numerator) for a, b in cleared)
+    divisor = content(integral)
+    require(divisor != (0, 0), "zero relation")
+    reduced = tuple(exact_div(value, divisor) for value in integral)
+    units = ((1, 0), (0, 1), (-1, 0), (0, -1))
+    return max(tuple(zmul(value, unit) for value in reduced) for unit in units)
+
+
+def support(exponents: tuple[int, ...]) -> tuple[int, ...]:
+    require(type(exponents) is tuple and 3 <= len(exponents) <= 10, "support size")
+    require(all(type(m) is int and abs(m) <= 128 for m in exponents), "integer exponent")
+    require(all(a < b for a, b in zip(exponents, exponents[1:])), "increasing support")
+    require(exponents[-1] - exponents[0] <= 64, "support span")
+    return exponents
+
+
+def nodes(exponents: tuple[int, ...]) -> tuple[Q, ...]:
+    return tuple(power(ALPHA, m) for m in support(exponents))
+
+
+def cofactors(points: tuple[Q, ...]) -> tuple[Q, ...]:
+    require(3 <= len(points) <= 10, "cofactor size")
+    result = []
+    for omit in range(len(points)):
+        value = ONE
+        for a, b in combinations(range(len(points)), 2):
+            if a != omit and b != omit:
+                value = mul(value, add(points[b], neg(points[a])))
+        result.append(neg(value) if omit % 2 else value)
+    return tuple(result)
+
+
+def independent_kernel(points: tuple[Q, ...]) -> tuple[Q, ...]:
+    """Solve the literal n by n system with the last coefficient fixed to 1."""
+    require(3 <= len(points) <= 10, "kernel size")
+    n = len(points) - 1
+    matrix = [[power(x, k) for x in points[:-1]] + [neg(power(points[-1], k))]
+              for k in range(n)]
+    for column in range(n):
+        pivot = next((r for r in range(column, n) if matrix[r][column] != ZERO), None)
+        require(pivot is not None, "singular Vandermonde")
+        matrix[column], matrix[pivot] = matrix[pivot], matrix[column]
+        scale = matrix[column][column]
+        matrix[column] = [div(value, scale) for value in matrix[column]]
+        for row in range(n):
+            if row != column:
+                scale = matrix[row][column]
+                matrix[row] = [add(a, neg(mul(scale, b)))
+                               for a, b in zip(matrix[row], matrix[column])]
+    return tuple(matrix[row][-1] for row in range(n)) + (ONE,)
+
+
+def valuation(value: Z, prime: Z) -> int:
+    require(value != (0, 0) and prime in (PI, RHO), "valuation domain")
+    bound = norm(value).bit_length() + 1
+    for exponent in range(bound):
+        r = value[0] * prime[0] + value[1] * prime[1]
+        s = value[1] * prime[0] - value[0] * prime[1]
+        if r % 5 or s % 5:
+            return exponent
+        value = r // 5, s // 5
+    raise ValueError("valuation step budget exhausted")
+
+
+def profile(exponents: tuple[int, ...]) -> tuple[tuple[int, int], ...]:
+    support(exponents)
+    n = len(exponents) - 1
+    gaps = tuple(b - a for a, b in zip(exponents, exponents[1:]))
+    return tuple((sum((n - 1 - s) * gaps[s] for s in range(j, n)),
+                  sum(s * gaps[s] for s in range(j))) for j in range(n + 1))
+
+
+def evaluate(coefficients: tuple[Z, ...], points: tuple[Q, ...], k: int) -> Q:
+    require(len(coefficients) == len(points) <= 10 and 0 <= k <= 9, "evaluation shape")
+    total = ZERO
+    for coefficient, point in zip(coefficients, points):
+        scalar = Fraction(coefficient[0]), Fraction(coefficient[1])
+        total = add(total, mul(scalar, power(point, k)))
+    return total
+
+
+def validate(exponents: tuple[int, ...], coefficients: tuple[Z, ...]) -> int:
+    support(exponents)
+    require(len(coefficients) == len(exponents), "coefficient shape")
+    require(all(type(a) is int and type(b) is int for a, b in coefficients), "integral coefficient")
+    require(all(c != (0, 0) for c in coefficients), "zero coefficient")
+    require(norm(content(coefficients)) == 1, "nonprimitive relation")
+    expected = profile(exponents)
+    points = nodes(exponents)
+    for k in range(len(exponents) - 1):
+        require(evaluate(coefficients, points, k) == ZERO, "nonzero root residual")
+    for coefficient, (a, b) in zip(coefficients, expected):
+        require((valuation(coefficient, PI), valuation(coefficient, RHO)) == (a, b),
+                "wrong gap valuation")
+        require(norm(coefficient) >= 5 ** (a + b), "coefficient norm floor")
+    n = len(exponents) - 1
+    gaps = tuple(b - a for a, b in zip(exponents, exponents[1:]))
+    mass = sum(a + b for a, b in expected)
+    weighted = sum((n - 1 + 2 * s * (n - 1 - s)) * gap for s, gap in enumerate(gaps))
+    require(mass == weighted, "gap mass identity")
+    require((mass == 2 * comb(n + 1, 3)) == all(gap == 1 for gap in gaps), "mass equality locus")
+    require(mass >= 2 * comb(n + 1, 3), "mass floor")
+    require(max(norm(c) for c in coefficients) >= 5 ** comb(n, 2), "maximum height floor")
+    return mass
+
+
+def fixtures() -> tuple[tuple[int, ...], ...]:
+    small = tuple((0,) + tail for n in range(2, 6) for tail in combinations(range(1, 9), n))
+    larger = []
+    for n in range(6, 10):
+        larger.extend((tuple(2 * j for j in range(n + 1)),
+                       tuple(j + j // 2 for j in range(n + 1)),
+                       tuple(j + j * (j - 1) // 4 for j in range(n + 1)),
+                       tuple(sum(1 + s % 3 for s in range(j)) for j in range(n + 1))))
+    translated = tuple(tuple(m + shift for m in e) for e in small[:10] for shift in (-7, 11))
+    return small + tuple(larger) + translated
+
+
+def controls() -> int:
+    invalid = ((), (0, 1), (0, 0, 1), (0, 2, 1), (0, 1, 65),
+               (0, True, 2), (0, Fraction(1), 2), (-129, -128, -127))
+    count = 0
+    for exponents in invalid:
+        try:
+            support(exponents)
+        except ValueError:
+            count += 1
+        else:
+            raise ValueError("invalid support accepted")
+    exponents = (0, 1, 3, 7)
+    coefficients = primitive(cofactors(nodes(exponents)))
+    a, b = coefficients[0]
+    changed = ((a + 1, b),) + coefficients[1:]
+    mutants = (changed, coefficients[:-1], tuple(zmul(c, PI) for c in coefficients),
+               ((0, 0),) + coefficients[1:], tuple((a, -b) for a, b in coefficients))
+    for mutant in mutants:
+        try:
+            validate(exponents, mutant)
+        except ValueError:
+            count += 1
+        else:
+            raise ValueError("bad coefficient vector accepted")
+    return count
+
+
+def main() -> None:
+    cases = fixtures()
+    coefficients_checked = roots_checked = tensor_entries = nonconsecutive = 0
+    digest = sha256()
+    for exponents in cases:
+        points = nodes(exponents)
+        coefficients = primitive(cofactors(points))
+        require(coefficients == primitive(independent_kernel(points)), "independent kernel disagreement")
+        mass = validate(exponents, coefficients)
+        n = len(exponents) - 1
+        if n <= 5:
+            for address in range(1 << (n - 1)):
+                require(evaluate(coefficients, points, address.bit_count()) == ZERO, "tensor entry")
+                tensor_entries += 1
+        nonconsecutive += any(b - a > 1 for a, b in zip(exponents, exponents[1:]))
+        coefficients_checked += len(coefficients)
+        roots_checked += n
+        digest.update(json.dumps([exponents, coefficients, mass], separators=(",", ":")).encode())
+    sample_exponents = (0, 1, 3, 4)
+    sample = primitive(cofactors(nodes(sample_exponents)))
+    sample_mass = validate(sample_exponents, sample)
+    package = Path(__file__).resolve().parent
+    filenames = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")
+    hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in filenames}
+    print(json.dumps({"status": "PASS_SPARSE_TENSOR_ANNIHILATOR_HEIGHTS", "fixtures": len(cases),
+                      "coefficient_occurrences": coefficients_checked, "root_residuals": roots_checked,
+                      "literal_tensor_diagonal_entries": tensor_entries,
+                      "nonconsecutive_supports": nonconsecutive, "rejected_controls": controls(),
+                      "case_digest": digest.hexdigest(),
+                      "sample": {"exponents": sample_exponents, "coefficients": sample,
+                                 "valuations": profile(sample_exponents), "mass": sample_mass},
+                      "sha256": hashes}, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()