Prove exact sparse tensor-annihilator coefficient valuations (no κ)

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.

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.

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"
+    }
+  ]
+}