Attain exact factor-one Stein bounds with at most 2r terms (no κ)

research/exact-unit-stein-splitting/PROOF.md

@@ -0,0 +1,131 @@
+# Exact unit bounds by splitting orthogonal residuals
+
+This contribution was produced by Nick Petalas. It is a scoped written
+proof over Q(i), with a bounded exact implementation and finite
+corroboration. It is not a complete multiplication theorem.
+
+## Statement
+
+For every E in Q(i)^(m by n), of rank r, there are s<=2r columns g_j in
+Q(i)^m and rows a_j in Q(i)^n such that
+
+    E = sum_j g_j a_j,
+    ||g_j||_2 <= 1,
+    ||a_j||_2 <= ||E||_2.
+
+In fact, with G having columns g_j and A having rows a_j,
+
+    GG* = P_col(E),       A = G*E.
+
+Zero E has s=0. All nonzero emitted terms are retained. The bound 2r is
+an upper bound, not an asserted global minimum. The coefficient row uses
+an adjoint exactly once, in G*E. The standard coordinate factorization
+uses m terms with the same unit bounds. The present bound depends on r
+and is useful for low-rank displacements in a larger ambient space.
+
+## Construction and proof
+
+Use the exact nonzero orthogonal residuals v_1,...,v_r of E's columns,
+as in Jose Manuel / jmbarrancoml's [PR4198](https://github.com/CrocSwap/integer-mult-bounds/pull/4198),
+`research/rational-stein-generators/PROOF.md`, section 1. Write
+n_k=v_k*v_k>0. The inherited projection identity is
+
+    sum_k v_k v_k* / n_k = P_col(E).
+
+For each k, choose z_k1,z_k2 in Q(i) with
+
+    |z_k1|^2 + |z_k2|^2 = n_k.
+
+Such a choice always exists. For example, clear a common positive integer
+denominator D from v_k, and write v_k=w/D with Gaussian-integer w.
+The positive integer N=w*w is a sum of four integer squares a^2+b^2+c^2+d^2
+by Lagrange's theorem. Then z_k1=(a+bi)/D and z_k2=(c+di)/D work.
+The classical theorem is not a new claim here; a primary formal source
+is [Mathlib's SumFourSquares module](https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/SumFourSquares.html).
+No Lean replay of this package is claimed.
+
+Define, omitting each zero z,
+
+    g_kl = v_k z_kl / n_k,       a_kl = g_kl* E.
+
+There are at most two terms per residual, and
+
+    sum_l g_kl g_kl*
+      = v_k v_k* (sum_l |z_kl|^2) / n_k^2
+      = v_k v_k* / n_k.
+
+Thus GG*=P_col(E), and GA=GG*E=E. Also
+
+    ||g_kl||_2^2 = |z_kl|^2/n_k <= 1,
+    ||a_kl||_2 = ||g_kl* E||_2 <= ||g_kl||_2 ||E||_2 <= ||E||_2.
+
+This proves the stated arbitrary-dimensional rational construction.
+It also proves the stronger positive-semidefinite inequality
+
+    E*E - a_kl* a_kl = E*(I-g_kl g_kl*)E >= 0.
+
+If N is a sum of two integer squares, the implementation uses one term
+for that residual. Its finite search finds such a representation whenever
+one exists within the complete range 0..floor(sqrt(N)). Otherwise the
+four-square representation gives two nonzero terms. No optimality of the
+aggregate count is inferred from this per-residual choice.
+
+## Stein and dirty-state interface
+
+For a square E=T-ZTZ*, with Z the nilpotent lower shift, finite telescoping
+gives the credited identity
+
+    T = sum_(h=0)^(m-1) Z^h E (Z*)^h
+      = sum_j L(g_j) U(a_j).
+
+The second equality is the coefficient-row convention of PR4198. Each
+new term can be passed to its existing compensated dirty-source macro,
+with that macro's own legal near-identity normalizer and all four calls
+paid. Summing complete macros restores the arbitrary source bank and adds
+Tx to the arbitrary target bank. This is a logical exact interface only.
+We have not run those child macros or implemented physical coefficient
+pages in this package.
+
+PR4198 uses r terms with row norms below 2||E||. Nick Petalas's
+[PR6228](https://github.com/CrocSwap/integer-mult-bounds/pull/6228)
+already gives r terms below (1+2^-p)||E|| and an exact-factor-one
+obstruction in the rank-minimal class. Those results are credited
+background, not replay targets. The new step here changes the term-count
+contract and attains the exact factor one.
+
+## Encoding and implementation scope
+
+For a residual with rational components of height H, one common
+denominator D uses at most 2mH bits. The Gaussian-integer coordinates of w
+then use at most (2m+1)H+1 bits. Each four-square coordinate has magnitude
+at most sqrt(N), so its bit length is bounded by half the bit length of N,
+rounded upward. Forming g and a uses rational products and finite sums.
+The construction therefore has finite rational output of polynomial
+encoding length, using the inherited rational residual height bound.
+This statement does not assert polynomial bit running time for our
+exhaustive four-square enumerator.
+
+The implementation first removes the common integer gcd of w. This only
+changes D's rational scale and leaves N smaller. It accepts at most eight
+rows and eight columns, input component height at most 256, and primitive
+N<=65,536 at every residual. Capacity exhaustion rejects explicitly.
+The theorem has no such finite limits; the implementation and its finite
+checks do.
+
+Every square loop is bounded by floor(sqrt(N))+1, its pair table has
+N+1 entries, and its split loop has N+1 iterations. Matrix operations
+have at most sixteen term columns and eight data rows or columns. There
+is no recursion, external solver or predecessor execution. Managed Python
+allocation is a Power of Ten rule 3 deviation, bounded by those capacities.
+Warnings are treated as errors in every registered command. The source
+and manifest checks are separate from mathematical verification.
+
+## Limits
+
+The construction can double the number of compensated generator macros.
+It proves no decrease in total gate count, precision, memory, runtime or
+recursive moment. Gaussian-rational coefficients may have odd denominators.
+Exact coefficient preparation, rounded children, physical delivery,
+restoration under rounding, compiler/native admission, stock/tape costs
+and the outer theorem retain their existing obligations. The selected
+frontier and all five framework assumptions are unchanged.

research/exact-unit-stein-splitting/README.md

@@ -0,0 +1,86 @@
+# Exact factor-one rational Stein generators
+
+Scoped written proof with exact finite corroboration. For every rectangular
+Gaussian-rational matrix E of rank r, the new construction gives
+
+    E = sum_(j=1)^s g_j a_j,     s <= 2r,
+    ||g_j||_2 <= 1,             ||a_j||_2 <= ||E||_2.
+
+The columns form a rational Parseval frame for col(E), and a_j=g_j*E.
+This improves the coefficient norm contract of Jose Manuel's
+[PR4198](https://github.com/CrocSwap/integer-mult-bounds/pull/4198)
+from a factor below two to exact factor one by permitting extra terms.
+Nick Petalas's [PR6228](https://github.com/CrocSwap/integer-mult-bounds/pull/6228)
+already approaches one with r terms. Its fixed-term normalizer is not
+used here. No new kappa is claimed. The standard coordinate factorization already
+gives the unit bounds with m terms; this construction bounds the count
+by 2r independently of the ambient row dimension m.
+
+The new step represents each rational residual norm as the sum of two
+Gaussian-rational squared norms, then splits its orthogonal projector.
+The rational residual interface and Stein/dirty-shear identities are
+credited to PR4198; Lagrange's four-square theorem is classical.
+[PROOF.md](PROOF.md) gives the arbitrary-dimensional argument and limits.
+
+## Evidence
+
+The verifier passes 414 matrix fixtures, containing total rank 698 and
+901 emitted terms. Exactly 123 fixtures use extra terms. It checks 2,048
+positive integer square decompositions and seventeen rejection controls.
+For E=(1,1,1)^T, it emits two terms with squared column norms 1/3 and 2/3
+and squared row norms 1 and 2. The exact matrix norm squared is three.
+
+The standalone checker independently row-reduces every input, reconstructs
+every matrix entry, checks the full Parseval projector and verifies
+E*E-a_j*a_j is positive semidefinite by exact Hermitian elimination.
+It also checks the complete two-square preference against a separate
+small enumeration. Counts and the explicit rank-one witness are emitted
+by the verifier, with hashes of every package source file. No receipt is
+handwritten and no predecessor scientific verifier is executed.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/exact-unit-stein-splitting/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/exact-unit-stein-splitting/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/exact-unit-stein-splitting
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/exact-unit-stein-splitting --check-source-history
+```
+
+Any CPython 3.12 path can replace the local interpreter. Expected markers
+are PASS_EXACT_UNIT_STEIN_SPLITTING, PASS_REGISTERED_RESEARCH_PACKAGE and
+PASS_RESEARCH_COMMIT_BYTES. The default replay is read-only. Optional
+`--receipt /absolute/new/path.json` writes a source-bound receipt and
+refuses to overwrite an existing file.
+
+## Limitations
+
+The written theorem has arbitrary finite dimensions. The executable
+accepts dimensions at most eight, component height at most 256, and
+primitive residual squared norm at most 65,536. It rejects exhaustion.
+Its exhaustive integer-square search is not a polynomial bit-time claim.
+The 2r term bound is not claimed optimal. Additional compensated macros
+may outweigh the smaller coefficients. No physical precision or supplier
+saving, complete multiplier, human review or formal-kernel acceptance is
+claimed. All five framework assumptions remain.
+
+## Open next questions
+
+- Can a rational Parseval construction always use fewer than 2r terms?
+  Start with the embedding of a rank-two rational Hermitian form into a
+  three-coordinate standard form. This could reduce the added macros;
+  arbitrary rational-form embedding and its preparation costs are open here.
+- Can an actual rounded child benefit after all extra terms are charged?
+  Start with one emitted tuple and its full compensated execution, including
+  coefficient preparation, rounding and delivery. The physical contract
+  and full caller invoice are missing. AAAmirinu's
+  [PR6239](https://github.com/CrocSwap/integer-mult-bounds/pull/6239)
+  already cautions that a smaller coefficient row alone need not reduce
+  child precision.
+
+This contribution was produced by Nick Petalas. Credit Jose Manuel /
+jmbarrancoml and Vlado Vojdanovski for the residual and dirty-shear compiler,
+Cinna Davis and the retained Gaussian/phase/caller authors, and classical
+Gram-Schmidt and four-square theory. Apache-2.0.

research/exact-unit-stein-splitting/SOURCES.json

@@ -0,0 +1,45 @@
+{
+  "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/rational-stein-generators/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "075e828b68dca080ab20461fba57047e46b3b271",
+      "sha256": "90e5681d0e32be1926df7f3fd2715aa43f983fa7e4c01ee42a15322f9d19e639"
+    }
+  ],
+  "references": [
+    {
+      "pr": 4198,
+      "author": "jmbarrancoml",
+      "role": "Main predecessor: exact orthogonal residual and Stein/dirty-shear interface."
+    },
+    {
+      "pr": 6228,
+      "author": "petalas",
+      "role": "Background only: near-unit fixed-term normalization; no construction or executable reused."
+    },
+    {
+      "pr": 6239,
+      "author": "AAAmirinu",
+      "role": "Background only: coefficient norm need not reduce rounded-child precision."
+    },
+    {
+      "url": "https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/SumFourSquares.html",
+      "role": "Classical Lagrange four-square theorem; no Lean replay claimed."
+    }
+  ]
+}

research/exact-unit-stein-splitting/TASK.json

@@ -0,0 +1,96 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its 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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "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": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "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 unit-norm Gaussian-rational Stein generators with at most twice the rank-many terms.",
+  "scope_change_reason": "The donor requests an original result, not an audit. This changes the coefficient term-count contract at PR4198 rather than reviewing a selected framework assumption.",
+  "bottleneck_link": "Side result on the coefficient preparation boundary. Exact smaller norms could affect a rounded child, but extra generator macros and physical costs must be paid first.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first exact factor-one construction and its bounded verification; do not expand into rounded/native implementation.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the general construction; verify.py checks exact rational finite fixtures and emits a source-bound receipt.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a universal rational Parseval construction use fewer than 2r terms?",
+      "why_it_matters": "Fewer added compensated generator macros could reduce overhead.",
+      "first_step": "Study a rank-two rational Hermitian form embedded into three standard coordinates.",
+      "blocked_by": "A rational embedding theorem and exact coefficient preparation algorithm are not supplied here."
+    },
+    {
+      "question": "Does an actual rounded child benefit after all extra terms are charged?",
+      "why_it_matters": "Coefficient norm alone does not determine physical precision or cost.",
+      "first_step": "Bind one emitted tuple to the complete compensated rounded child and charge preparation, delivery and every extra call.",
+      "blocked_by": "Physical coefficient delivery and complete caller costs remain missing."
+    }
+  ],
+  "environment": {
+    "implementation": "CPython",
+    "version": "3.12.15",
+    "system": "Darwin",
+    "machine": "arm64",
+    "dependencies": "standard library only"
+  }
+}

research/exact-unit-stein-splitting/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": 120,
+      "checks": "Complete exact reconstruction, Parseval projector, independent rank and Hermitian PSD checks, square enumeration and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same full contract with assertions disabled."
+    }
+  ]
+}