Reduce Horner oracle precision volume with increasing grids (no κ)

research/horner-increasing-precision/PROOF.md

@@ -0,0 +1,142 @@
+# Increasing-precision fixed-source Horner evaluation
+
+This scoped written theorem and construction were produced by Nick Petalas.
+The fixed-source inverse evaluator and disk-grid contract are Hanson Sun's
+[PR1430](https://github.com/CrocSwap/integer-mult-bounds/pull/1430).
+Variable-precision iteration, Horner evaluation and geometric error damping
+are classical. The new step is the explicit schedule and precision-volume
+improvement under that rounded-oracle interface.
+
+## Statement and changed premise
+
+Use the maximum complex-coordinate norm. Let E be a complex linear map with
+norm at most c=21/50. Let D_q consist of complex vectors with coordinates in
+2^-q Z[i] and norm at most one. For each integer q>=101, suppose an oracle
+T_q:D_q -> D_q satisfies
+
+    ||T_q(z)-Ez|| < (q/3) 2^-q, for every z in D_q.
+
+No linearity, homogeneity, oddness, consistency between precisions or
+correlation of oracle errors is assumed. Supplying this whole oracle family
+is an additional premise compared with access to only one fixed T_p.
+
+For any integer p>=102 and u in D_p, set
+
+    q_j = max(101,j+3),                       j=0,...,p-1,
+    v_j = componentwise inward rounding of u/2 to grid 2^-q_j,
+    y_0 = v_0,
+    y_j = v_j - T_(q_j)(y_(j-1)),            j=1,...,p-1.
+    w = componentwise inward rounding of y_(p-1) to grid 2^-p.
+
+Coarser dyadic values embed exactly in every finer grid. The subtraction
+is exact on that grid. Every oracle input and every y_j belongs to D_(q_j).
+The final output w belongs to D_p and obeys
+
+    ||w - (I+E)^(-1)u/2||
+      < [25(2p+13)/96 + 137/58] 2^-p
+      < p 2^-p.                                             (1)
+
+The working computation uses two final guard bits; the last inward rounding
+returns the original p-bit output format. Its error and work are charged.
+
+There are exactly p-1 complete oracle calls. The sum of their requested
+precision parameters is exactly
+
+    V(p) = sum_(j=1)^(p-1) q_j
+         = (p^2+5p)/2 + 4750 < p(p-1).                        (2)
+
+Thus the same p-term fixed-source evaluation can retain its published
+p*2^-p error allowance with a strictly smaller oracle precision volume.
+This is a deterministic instruction-parameter count, not a runtime
+measurement or a complete bit-cost saving. It approaches half the fixed
+p oracle volume as p tends to infinity. Optimality is not claimed.
+
+## Disk and grid invariants
+
+Inward componentwise rounding cannot increase the modulus, so ||v_j||<=1/2
+and ||v_j-u/2||<sqrt(2)*2^-q_j<(3/2)*2^-q_j. Both complex
+components are charged, including when q_j is coarser than p. The sequence
+q_j is nondecreasing.
+Therefore a y_(j-1) in D_(q_(j-1)) is an exact valid grid input at q_j.
+For q>=101,
+
+    1/2 + c + (q/3)2^-q < 1.
+
+It suffices to check q=101 because q*2^-q decreases. Induction gives
+||y_j||<1 and grid membership at every iteration. Oracle outputs belong
+to D_(q_j) by the supplied contract. Every subtraction is between two
+values on that grid; the norm estimate bounds its result before it is
+used again. No uncharged projection is used to repair the invariant.
+
+## Rounded error and inverse tail
+
+Set x_0=u/2 and x_j=u/2-E x_(j-1). Then
+
+    x_(p-1) = (1/2) sum_(a=0)^(p-1) (-E)^a u.
+
+Writing d_j=||y_j-x_j||, the input rounding and oracle contract give
+
+    d_0 < (3/2)2^-q_0,
+    d_j < c*d_(j-1) + (3/2+q_j/3)2^-q_j.
+
+Put Q=p+2. For d=p-1-j, q_j>=Q-d and q_j<=Q. Including the initial
+error with the same larger coefficient gives
+
+    d_(p-1)
+      < (3/2+Q/3) 2^-Q sum_(d=0)^(p-1) (2c)^d
+      < (3/2+Q/3) 2^-Q / (1-2c)
+      = 25(2p+13) 2^-p / 96.                               (3)
+
+This estimate allows arbitrary errors at each precision and every repeated
+use of T_101. In particular it assumes no cancellation between calls.
+
+Since c<1/2, E^p has norm at most c^p<2^-p. The inverse exists by the
+convergent Neumann series, and its omitted tail has norm less than
+
+    2^-p / (2(1-c)) = (25/29)2^-p.
+
+The final inward projection costs less than (3/2)2^-p and cannot increase
+the norm, so w belongs to D_p. Adding (3), the inverse tail and this last
+rounding proves the first inequality in (1), since 25/29+3/2=137/58.
+The second is equivalent to 1334p>16001, which holds for all p>=102.
+
+## Exact precision count
+
+The p-1 calls have indices j=1,...,p-1. Relative to the baseline ramp
+j+3, the floor at 101 adds
+
+    sum_(j=1)^97 (98-j) = 97*98/2 = 4753.
+
+Also sum_(j=1)^(p-1)(j+3)=(p^2+5p)/2-3. This proves the equality in (2).
+The baseline difference is
+
+    p(p-1)-V(p) = (p^2-7p-9500)/2.
+
+It is 95 at p=102 and increases by p-3 on replacing p by p+1. This proves
+strict improvement for every p>=102 without a finite extrapolation.
+At p=128 the exact volumes are 16256 and 13262. At p=256 they are
+65280 and 38158. These count requested precision bits across calls,
+excluding the dimension multiplier and all implementation tariffs.
+
+## Wrapper and scope obligations
+
+The algorithm retains the original input u, the current state and one oracle
+result. It prepares v_j at each iteration, rather than rounding u/2 once.
+All those source roundings and source reads are additional explicit work.
+Embedding a coarser numerator at a finer grid uses a shift, and subtraction
+needs a sign/carry bit before the proved disk bound is applied. The largest
+requested grid precision is p+2. In a sequential binary fraction layout,
+preparation, embedding, subtraction and head returns use O(s*q_j) bit work
+per iteration for s complex coordinates, plus O(sp) initial/final work,
+including the charged final projection to the original p-bit grid.
+This statement counts these wrapper operations; it does not provide a
+source-bound multitape implementation or a favorable complete constant.
+
+No extra bank is provided free. Read buffers, oracle workspace, cleanup and
+arbitrary productive dirty inputs need their actual caller contracts.
+The norm proof alone does not authorize replacing precision in an emitted
+native word. An actual Gaussian T_q family, its preparation/analytic error,
+source streaming, grid conversions, final output use, stock, restoration and
+the complete physical bill remain obligations. The five selected framework
+assumptions and the selected frontier are unchanged. No new kappa, complete
+multiplication theorem, human review or formal-kernel proof is claimed.

research/horner-increasing-precision/README.md

@@ -0,0 +1,127 @@
+# Increasing precision lowers the Horner oracle volume
+
+For every integer p>=102, the fixed-source inverse evaluator can request
+strictly fewer total oracle precision bits while retaining p-1 oracle calls,
+a p-bit disk-grid output and error less than p*2^-p. This is a scoped written
+proof with exact finite corroboration.
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Let ||E||<=21/50 in the maximum complex-coordinate norm. Assume access to
+the rounded-E oracle of Hanson Sun's
+[PR1430](https://github.com/CrocSwap/integer-mult-bounds/pull/1430) at every
+integer precision q>=101, with error less than (q/3)2^-q on the whole disk
+grid. This family is an explicit additional premise compared with a single
+fixed-precision oracle. No consistency between its errors is needed.
+
+At iteration j=0,...,p-1 use q_j=max(101,j+3). Round the unchanged source
+u/2 inward to each working grid and perform the fixed-source Horner update.
+The last oracle uses precision p+2. A final charged inward rounding returns
+the output to the original p-bit disk grid. [PROOF.md](PROOF.md) proves every
+grid/disk invariant, source-rounding charge and inverse-tail bound.
+
+The exact sum over the p-1 oracle calls is
+
+```text
+fixed precision:       p(p-1)
+increasing precision: (p^2+5p)/2 + 4750
+strict saving:        (p^2-7p-9500)/2 > 0, for every p>=102
+```
+
+The ratio approaches one half. At p=128 the counts are 16256 and 13262;
+at p=256 they are 65280 and 38158. These are enumerated sums of requested
+precision parameters, not runtime measurements, memory bounds, paid recursive
+histograms or a complete supplier invoice. The work of repeatedly preparing
+the source is explicitly additional. There is no new kappa or selected-frontier
+change, and no optimality claim.
+
+## Evidence and reproduction
+
+The standalone verifier uses integer dyadic execution and a separate rational
+real-block executor. Every reached prefix agrees. Exact rational elimination
+of I+E supplies an independent final inverse. Its five rational complex
+matrices have dimensions one through three and include a nonnormal case.
+Six requested precisions are 102, 103, 128, 192, 256 and 512. Three oracle
+modes include input-dependent signed local errors and ordinary inward rounding.
+
+The generated output reports 684 complete executions and 146718 oracle calls.
+It checks the disk and grid conditions and the proved final error bound at
+every applicable point. All 1947 integer precisions p=102,...,2048 have their
+literal precision sums compared with the closed form and strict-saving test.
+Eleven rejecting controls cover bad precision arguments, a frozen coarse
+schedule, wrong update sign, missing source halving, decreasing grids, excess
+oracle error and an invalid operator bound. All checks use explicit exceptions
+and remain enabled under optimization.
+
+From the worktree root, standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/horner-increasing-precision/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/horner-increasing-precision/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/horner-increasing-precision
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/horner-increasing-precision --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. Direct execution prints
+a generated receipt with all six package-file SHA256 hashes and the exact
+interpreter version, then PASS_HORNER_INCREASING_PRECISION. It writes no files
+and needs neither Git nor external inputs. The registered commands run normal
+and optimized checks. Source documents in SOURCES.json are provenance only;
+no predecessor executable, scientific verifier or receipt is imported or replayed.
+The universal conclusion rests on the written proof, not a finite census.
+
+## Scope, coordination and credit
+
+The original formal-interface-lemma card is explicitly changed to a written
+precision-interface result. No proof-assistant formalization is claimed.
+The selected-source orientation passed at canonical main
+7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, selected PR6030.
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363411)
+records the target before substantive work. Live claims and reservations,
+recent account PR bodies, open/merged searches and main README searches were
+checked. Cached sparse local notes and unpublished work remain coverage limits.
+
+Hanson Sun / bbMisk's PR1430 supplies the fixed-source evaluator, its oracle
+interface and the disk-invariant proof method. Its first Open next question
+asks for a corrected actual Gaussian implementation. This is a new precision
+schedule for that interface, not the missing backend or an audit of its result.
+eumemic / PR5, icekylinx, the Harvey-van der Hoeven resampling lineage,
+Artus Krohn-Grimberghe / PR371, Effy Elden / PR684 and Alan Grillo / PR902
+retain their source/interface/analytic credit. Ordinary Horner evaluation,
+variable-precision iteration and contraction bounds are classical; global
+literature priority is unclaimed. All predecessor files and credit are unchanged.
+
+The actual multi-precision Gaussian oracle, its preparation, source reads,
+head returns, grid conversion, workspace cleanup, dirty restoration, native
+legality, stock and complete physical cost remain obligations. The proof
+does not discharge any of the five selected framework assumptions. No selected
+cold replay, Lean, Docker, physical backend, independent human review or formal
+proof-kernel review is claimed.
+
+## Open next questions
+
+Can a corrected actual Gaussian E family supply the requested oracles with a
+favorable complete invoice? Begin with one implemented family, prove the same
+disk/error contract at every q, and price its preparation together with all
+repeated source roundings and the final p-bit projection. An actual backend
+and source-compatible physical caller are the blockers. TASK.json records
+the same question. No further precision optimization is undertaken here.
+
+## Verifier bounds
+
+The verifier has no external numeric input. Every matrix has at most three
+complex coordinates, each registered execution has a fixed set of 684 cases,
+and the independent arithmetic sweep has 1947 iterations with at most 2048
+precision entries each. Functions have at most 44 physical lines. The call
+graph is nonrecursive, state is local, file reads are capped at 256 KiB, and
+no subprocess, dynamic code generation or callback dispatch is used.
+
+Python's managed allocation is a deviation from fixed storage. Its scope is
+this terminating bounded verifier: at most six scalar coordinates per state,
+2048 precision entries, six bounded file reads and fixed-size elimination
+matrices. Checks validate input/domain bounds and every disk/grid transition.
+A fixed-storage implementation is required before using the verifier in a
+runtime that forbids managed allocation. Warning-strict normal/optimized
+execution and in-memory source compilation provide the local diagnostics.
+External Python linters were unavailable locally; no broader static-analysis
+or repository-wide analyzer configuration change is claimed.

research/horner-increasing-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/neumann-rounding-audit/README.md",
+      "usage": "provenance",
+      "git_blob": "6c6c0899fc00144c2ba97f1760ecd50a22ba6d57",
+      "sha256": "332a166718e3671b0db06c8cb73ca7673ee0224ac2645eea61972041d50a110e"
+    }
+  ]
+}