Prove smaller bulk precision for cyclic-band solves (no κ)

research/row-adaptive-band-precision/PROOF.md

@@ -0,0 +1,201 @@
+# Row-dependent precision in cyclic-band elimination
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Claim and predecessor boundary
+
+This is a scoped written mathematical proof, with finite exact corroboration.
+It changes the precision allocation in Ali Romman's
+[PR5284](https://github.com/CrocSwap/integer-mult-bounds/pull/5284),
+[cyclic-band proof](../cyclic-band-gap-solver/PROOF.md). That predecessor supplies
+one-round fixed-integer elimination, the cyclic fill pattern, variable-gap
+stability and its common-grid solve. Its row residual uses `N K h` in every
+row. The new step permits monotone, unequal row grids and replaces that
+residual by a row-support bound. The arithmetic method and classical
+row-dominance estimates retain their predecessor credit.
+
+Let A be a real N by N dyadic matrix on the p-bit fractional grid. Suppose
+
+    a_ii - sum_(j != i) |a_ij| >= delta > 0,
+    max_i sum_j |a_ij| <= M,
+    a_ij = 0 when min(|i-j|, N-|i-j|) > W,    0 <= W < N.
+
+No symmetry or sign condition on off-diagonal entries is required. Let b be
+real or complex on a supplied dyadic grid. In the complex case use the norm
+`max_i (|Re b_i| + |Im b_i|)` and assume it is at most Y>0. Choose a desired
+absolute solution error t>0. Input formation and final-grid errors are outside
+this contract.
+
+Take a symmetric symbolic elimination pattern containing the cyclic band,
+closed under natural-order Schur updates. Let m_i count the strictly lower
+factor positions and the diagonal/upper positions in row i, including positions
+whose numerical value is zero. Write
+
+    K = max(1,2M),
+    p <= q_0 <= ... <= q_(N-1),       S_i = 2^q_i,
+    h_i = 1/S_i,                    e = max_i m_i K h_i.
+
+The following construction gives factors B=LU with `||B-A||_infinity <= e`.
+If e<=delta/2, all its pivots are positive and
+
+    ||U|| <= 3M/2,     gap(U) >= delta/2,
+    ||L|| <= 2M/delta, ||B^-1|| <= 2/delta,
+    ||L^-1|| <= 3M/delta.
+
+Every norm on a real matrix is its absolute row-sum norm.
+
+## Exact mixed-grid construction
+
+Store unfinished Schur row i at scale S_i squared. Initialize
+`C_ij = a_ij S_i^2`, exactly. At pivot k perform
+
+    U_int[k,j] = trunc(C[k,j]/S_k),                         j>=k,
+    L_int[i,k] = trunc(C[i,k]/(U_int[k,k] 2^(q_i-q_k))),    i>k,
+    C[i,j] -= L_int[i,k] U_int[k,j] 2^(q_i-q_k),           i,j>k.
+
+Visit the declared symbolic positions only. Here trunc rounds toward zero,
+`U[k,j]=U_int[k,j]/S_k`, `L[i,k]=L_int[i,k]/S_i`, and L has unit diagonal.
+The nonnegative exponent `q_i-q_k` is essential. It lets each update be an
+exact integer subtraction on the row-i grid without increasing that grid.
+It also makes the lower formula precisely rounding `C_real[i,k]/U[k,k]`
+to row i's factor grid. No multiplication or Schur update is rounded.
+
+Expanding row i's exact updates shows that a completed upper position has
+residual less than h_i, and a completed lower position has residual less than
+`h_i |U[j,j]|`. The same identities apply to a partial factorization: put
+these residuals at completed positions of A and zero at unfinished positions.
+Its completed factors are exact factors of this partially perturbed matrix.
+Outside the symbolic factor pattern the residual is zero, since the pattern
+is closed under elimination. Consequently a partial row residual is at most
+`m_i K h_i` whenever completed pivots have magnitude at most 2M.
+
+For completeness, the needed classical exact row-dominance facts are as
+follows. Eliminating multiplier l from a row of a positive-diagonal matrix
+with row gap g and row norm R increases the surviving row gap by at least
+`|l| g` and decreases its absolute row sum by at least `|l| g`. Pivots stay
+positive. If s is the accumulated absolute multiplier sum in one row, its
+final gap is at least `g(1+s)` while its final row norm is at most `R-gs`.
+Thus `||L|| <= (R+g)/(2g)`, `||U||<=R`, `gap(U)>=g`, and
+`||B^-1||<=1/g`. These are the estimates used in PR5284, cited here as
+predecessor mathematics rather than an audit target.
+
+Apply these facts to each partially perturbed matrix with
+`R=M+e`, `g=delta-e`. Since e<=delta/2<=M/2, a newly completed pivot has
+magnitude at most `M+e<=3M/2<2M` and is at least delta/2. This closes the
+induction from the first pivot, proves every division is defined and proves
+the factor residual claim. The L bound follows from
+`(M+delta)/(2(delta-e))<=2M/delta`. Finally
+`L^-1=U B^-1` gives `||L^-1||<=3M/delta`. The same arguments hold for every
+leading principal factor pair, since deleting columns cannot decrease a
+row-dominance margin.
+
+## An independently chosen solve grid
+
+Choose a common solve grid step `h_s=2^(-q_s)` containing b's input grid.
+Accumulate each triangular dot product exactly, then round the solved
+coordinate once. A lower or upper row-i product has grid `S_i 2^q_s`, so the
+mixed factor grids introduce no extra numerical rounding. Execute separately
+on the real and imaginary components. The triangular equations obey
+
+    L z = b + f,       ||f|| <= 2 h_s,
+    U x = z + g,       ||g|| <= 3 M h_s.
+
+Hence `B x=b+r`, with
+
+    ||r|| <= R_s = 2 h_s (1+3M^2/delta).
+
+The factor two is a sufficient common bound for the complex component norm;
+a real solve is covered too. The resolvent identity and `||A^-1||<=1/delta`
+give
+
+    ||x-A^-1 b|| <= (eY + delta R_s)/(delta(delta-e)).
+
+In particular it suffices to choose
+
+    e <= min(delta/2, t delta^2/(4Y)),
+    h_s <= t delta^2/(8delta+24M^2).
+
+The first contribution is at most `2eY/delta^2<=t/2`, and the second is at
+most `2R_s/delta<=t/2`. Factor precision and solution precision can therefore
+be chosen separately. If b has a finer input grid, increase q_s to include it.
+
+## The cyclic-band improvement
+
+For N>2W put the last W indices in the border. Natural-order elimination of
+a bulk index connects only its next W bulk indices and the W border indices.
+A bulk row has at most W earlier bulk neighbors and at most 2W later
+neighbors. Therefore
+
+    m_i <= min(N,3W+1)   for i<N-W,
+    m_i <= N            for i>=N-W.
+
+This is also the usual fill argument in PR5284, now used to price residuals
+row by row. If N<=2W, use the dense count N everywhere. The formulas above
+then still give the same safe allocation because `min(N,3W+1)=N`. If W=0,
+every row has one position and no border is needed.
+
+For a funded e-budget define
+
+    q_bulk = max(p, ceil(log2(min(N,3W+1) K / e_budget))),
+    q_high = max(p, ceil(log2(N K / e_budget))).
+
+Assign q_bulk to the first N-W rows and q_high to the final W rows. These
+precisions are nondecreasing, so the mixed-grid theorem applies. The full
+length enters only the border factor precision. For fixed W, delta, M, Y,
+p and t, the required precision on every bulk factor row is independent of N.
+This removes a logarithmic length term from those rows' sufficient guards.
+The common-grid allocation using the same e-budget requires q_high on every
+row. No assertion is made that either sufficient allocation is optimal.
+
+The arithmetic schedule still has at most `4 N W^2` factor products and
+`8 N W` products per complex solve. There are at most `(4W+1)N` stored factor
+positions. The new shifts are exact rescalings, not additional oracle calls.
+This is an arithmetic/precision statement; it does not certify a native
+instruction tariff, variable-record tape layout, wall-time gain or complete
+recursive bill. A machine choosing one common word width still pays its
+maximum required width.
+
+## Integer ranges
+
+One can retain the predecessor's dimension-free magnitude bounds. Put
+
+    L_0=2M/delta, U_0=3M/2,
+    Z=(3M/delta)(Y+2h_s), X=(2/delta)(Y+R_s),
+    C=max(1,M+L_0 U_0,Y+L_0 Z,Z+U_0 X,L_0,U_0,Y,Z,X).
+
+Absolute partial dot sums are bounded by their row sums. Thus factor row i's
+Schur entries, update products and division numerators need magnitude at
+most `C S_i^2`. Its divisor `U_int[k,k] 2^(q_i-q_k)` has magnitude at most
+`U_0 S_i`. A signed width `2q_i+ceil(log2 C)+2` suffices for factor work.
+Solve row i's accumulators need at most `C S_i 2^q_s`, so width
+`q_i+q_s+ceil(log2 C)+2` suffices there. Forward prefixes use the leading
+principal estimates above. Backward intermediates are already coordinates
+of the final x, so the final bound covers them. Finite Python execution uses
+unbounded integers; these are written sufficient range bounds, not an emitted
+bounded-word implementation certificate.
+
+## First strict fixture and finite evidence
+
+Take N=65, W=1, diagonal 1, and cyclic adjacent entries -63/128. Its row gap
+is delta=1/64. Use M=2, Y=1, alternating right-hand side 1,-1, and target
+`t=2^-16`. The chosen e-budget is `2^-30`. The allocation is
+
+    factor rows 0..63: q=34,   factor row 64: q=39,
+    common solve grid: q_s=35, matched common factor grid: q=39.
+
+There are 319 symbolic factor positions, 254 in bulk rows. Their declared
+fraction-bit total falls from 12,441 to 11,171, a saving of 1,270. This counts
+fractional precision per symbolic factor position, including zeros; it is
+not a measurement of Python memory or a physical encoded representation.
+The constructor performs 253 factor update products. The exact original-
+matrix residual is `1443/4398046511104`, and the general sufficient error
+bound is `1793/268435440 < 2^-16`. Independently, residual divided by delta
+also certifies the requested solution accuracy.
+
+The verifier additionally checks the support bounds on 1,125 symbolic patterns
+with 1,171,245 row positions, and checks 252 signed and unsigned, generally
+nonsymmetric small dyadic systems against an independent pivoted rational
+solver. These are finite corroboration of the written all-size result, not a
+replacement for it. No predecessor scientific suite is replayed. Complex
+vectors are covered by the written two-real-solve argument; the executable
+fixtures use real right-hand sides.

research/row-adaptive-band-precision/README.md

@@ -0,0 +1,110 @@
+# Smaller bulk guards for cyclic-band elimination
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written mathematical proof with exact finite corroboration.
+For a real dyadic cyclic-band matrix of half-width W and row-dominance gap
+delta>0, natural-order elimination can use lower factor precision on its first
+N-W rows. Its final W border rows retain the full-length guard:
+
+```text
+predecessor factor residual: N K 2^(-q) in every row
+new factor residual:        max_i m_i K 2^(-q_i)
+bulk support count:         m_i <= min(N,3W+1)
+border support count:       m_i <= N
+```
+
+[PROOF.md](PROOF.md) proves the mixed-grid update identity, stability induction,
+separate solve precision, integer ranges and all-size cyclic support bound.
+The precisions q_i must be nondecreasing. This is an original precision
+allocation step on Ali Romman's [PR5284](https://github.com/CrocSwap/integer-mult-bounds/pull/5284)
+algorithm, not an audit of that result.
+
+On the first strict 65-row tridiagonal fixture, bulk factor precision is 34
+fractional bits instead of the matched uniform allocation's 39; the final row
+uses 39. The abstract factor fraction-bit total is 11,171 instead of 12,441.
+Exact residuals certify the same 2^-16 solution target. No optimality,
+wall-time, native/tape bill, Gaussian-family admission, new kappa or selected-
+frontier change is claimed. The five selected framework assumptions remain.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/row-adaptive-band-precision
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/row-adaptive-band-precision --check-source-history
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/row-adaptive-band-precision/verify.py
+```
+
+The absolute interpreter path records the local environment. A different
+CPython 3.12 executable can replace it. VERIFY.json registers normal and
+optimized warning-strict runs. Each must print
+`PASS_ROW_ADAPTIVE_BAND_PRECISION`, `errors=0`, 252 small exact solve comparisons,
+1,125 symbolic patterns, and the strict 65-row precision reduction. JSON stdout
+also binds all package-file hashes. Receipts are generated, not handwritten.
+No output files or bytecode caches are created by the verifier.
+
+The all-size theorem is written mathematics. Finite fixtures are real,
+N<=129 for pattern checks and N<=65 for numerical checks; the implementation's
+explicit capacity is N<=257, W<=8, q<=512. Small numerical systems are checked
+against an independently transcribed pivoted rational solver. This does not
+claim independent human or formal proof-kernel review. The complex extension
+is a written two-real-solve argument. No full predecessor, selected supplier,
+Lean, Docker, native backend or physical-tape replay is required or claimed.
+
+## Scope and credit
+
+Ali Romman / PR5284 supplies the variable-gap solver, one-round factor-entry
+method, diagonal-dominance stability estimates and cyclic fill. The new work
+is the monotone row-grid theorem, its support-priced residual and reduced bulk
+allocation. Dugongue / PR4554 supplies the earlier band/Woodbury interface;
+Ryanson Jonathan / PR4556 supplies its independent check, cited as context and
+not replayed. PR5260 and PR5326 are prior fixed-source and Gaussian Reference
+consumers. Classical Gaussian elimination and row dominance retain their
+classical status. No worldwide novelty claim is made for those methods.
+Frozen predecessor files and their credit lines are unchanged.
+
+The assigned uniform-transfer-audit card is explicitly changed to this
+numerical-interface result. It addresses precision costs that a future paid
+Gaussian caller must fund; it does not discharge the selected precision_tape
+assumption. SOURCES.json pins the exact predecessor proof and originating
+catalogue. The verifier imports no predecessor code.
+
+The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363375)
+reserved this question. Live overlap covered 430 open PR bodies and 6,404
+Discussion records with complete remote pagination at the recorded snapshot.
+The initial sparse local search covered 115 of 8,917 tracked notes. Relevant
+proofs were then read directly, and main/merged searches covered mixed row
+precision and cyclic-band terms. Arbitrary diffs, unmaterialized notes and
+unpublished work remain outside that coverage. No novelty certificate is
+claimed.
+
+## Open next questions
+
+Can an actual Gaussian production caller use the row allocation to reduce its
+paid precision/storage bill? First freeze its coefficient error, row gap,
+symbolic fill and record representation, then account for the W high-precision
+border rows and solve buffers. Source generation, fixed-tape layout, native
+operations and the complete recursive invoice remain blockers. A single common
+machine-word representation may obtain no storage benefit.
+
+Can a different elimination order lower the number of high-precision rows
+without increasing fill or the required row-residual budget? First derive its
+symbolic row counts and a valid mixed-grid schedule. The monotone grid rule in
+this result may prevent a naive permutation from applying directly. No such
+optimization is included here.
+
+## Verifier constraints
+
+Every loop is bounded by explicit matrix, bandwidth, precision or fixture
+limits. Functions are under 60 lines. Invalid shapes, grids and divisors fail
+with explicit errors retained under optimized Python. The verifier uses no
+recursion, dynamic code generation, subprocesses or network calls. Python's
+managed allocation is a Power of Ten rule 3 deviation, bounded here by N<=257,
+W<=8, q<=512, finite fixture counts and a registered 60-second timeout.
+Package hashing is bounded to eight files of at most one MiB each. There is no
+claim of a fixed physical Python heap. Reassess storage if those limits change.
+Warnings-as-errors in both interpreter modes are the available diagnostics;
+no additional static analyzer is configured for this isolated standard-library
+research verifier.

research/row-adaptive-band-precision/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/cyclic-band-gap-solver/PROOF.md",
+      "usage": "input",
+      "git_blob": "924929376c304d743a15e67aed2ac7712fd89892",
+      "sha256": "508fd707fcfe1490ee3de0047b7d4d699cf341d2d22dfce1ea297e16e9beebb9"
+    }
+  ]
+}