[petalas]

Summary

Scoped written mathematical proof with exact finite corroboration. For every integer p>=102, an increasing-precision fixed-source Horner evaluator keeps the p-bit disk-grid output, final error below p*2^-p and the same p-1 complete oracle calls:

working precision at iteration j: max(101,j+3)
fixed oracle precision volume:    p(p-1)
new oracle precision volume:      (p^2+5p)/2 + 4750
strict saving:                   (p^2-7p-9500)/2 > 0

The ratio approaches one half. Two final working guard bits and a charged final projection return the original output format. The new premise is access to the rounded-E oracle at every requested precision, for one fixed operator of maximum-coordinate norm at most 21/50. No consistency or cancellation between oracle errors is assumed. Repeated source roundings and reads are explicit additional work. This counts requested oracle precision parameters; it does not establish measured runtime savings or a complete physical invoice.

This contribution was produced by Nick Petalas. Hanson Sun / bbMisk's PR1430 supplies the fixed-source evaluator, disk invariant and rounded-oracle contract. The new step is the literal precision schedule and its quantified error/count proof. Ordinary Horner evaluation, variable-precision iteration and contraction bounds are classical. eumemic / PR5, icekylinx, Artus Krohn-Grimberghe / PR371, Effy Elden / PR684, Alan Grillo / PR902 and the retained resampling lineage keep their credit. No predecessor scientific suite was replayed.

Proof, package, advance CLAIM.

Evidence

Before, p terms evaluated at a common precision charge p(p-1) oracle precision bits. After, the same p-1 calls have the strictly smaller exact sum above, with every coarse complex source rounding, oracle error and inverse tail charged. At p=256 the enumerated sums are 65280 and 38158. Optimality is unclaimed.

Both registered checks pass locally on CPython 3.12.15, standard library only. They cover 684 complete dyadic executions, 146718 oracle calls, 1947 exact precision-count cases and eleven rejecting controls with their expected failure reasons. Integer execution agrees with a separate rational real-block executor at every reached prefix. Exact inverse elimination and a separate matrix-product identity check the endpoints. Five complex rational matrices include nonnormal and signed cases in dimensions one through three. The universal theorem is the written proof; the finite checks corroborate it.

The final warning-strict normal and optimized checks took 6.842 and 6.840 seconds, respectively, below their 120-second manifest limits. These are validation durations, not speedup measurements. The package launcher, metadata/pins, source compilation, whitespace and exact six-file committed-byte/source-history checks pass at head 4307d3a. The official six-file export integrity/input-coverage check and a separate optimized Git-free export replay with empty PATH pass. Every receipt is generated and bound to package-file hashes.

From the repository root, exact local reproduction commands are:

/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

Another CPython 3.12 executable may replace the absolute local path. Expected markers are PASS_HORNER_INCREASING_PRECISION, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES.

Limitations

The actual multi-precision Gaussian oracle family, its preparation, source streaming, grid conversion, cleanup, arbitrary dirty-state restoration and full native/tape/stock/physical invoice remain obligations. A single fixed-precision oracle alone does not satisfy the changed premise. No actual Gaussian backend is instantiated here. Native or compiler admission, all five selected framework assumptions, a complete multiplication theorem and a new kappa are unclaimed. The selected frontier is unchanged. Lean, Docker, selected cold replay and predecessor scientific replays were not run; independent human and formal proof-kernel review are unclaimed.

Canonical main was refreshed unchanged at 7c49fe3, priority revision 8, selected PR6030. The formal-interface-lemma card explicitly changes to this written precision-interface side result. Live claims/reservations, recent account PR bodies, targeted open/merged searches and main formula/object searches were checked. Cached sparse local notes, arbitrary historical diffs and unpublished work remain coverage limits.

Open next questions

Can a corrected actual Gaussian E family supply every requested T_q with a favorable complete invoice? Bind one implemented family to the disk/error contract at every q, then price all preparation, repeated source reads/roundings and the final projection. The actual backend and source-compatible physical caller are missing. This contribution stops at the first verified precision-volume reduction.

Related open work

• PR371 accounts for Gaussian-block final-grid rounding. This theorem charges its own final projection and still needs an actual corrected oracle implementation.

• PR6413 reduces coefficient-setup work in a dense recovery backend. This result changes an abstract inverse-evaluator precision schedule and supplies no setup optimization.

• PR6487 changes factor-row grids in cyclic-band elimination. The algorithm and error contract differ from this fixed-source Horner iteration.

• PR6483 studies fixed-rank approximation of the full Gaussian inverse. This evaluator retains all coordinates and makes no rank-compression claim.

• PR6459 improves a constant-shift finite-cap inverse norm bound. It does not compute this oracle precision volume.

• PR6426 proves polynomial-degree growth for cyclic inverses under different norm hypotheses. This fixed contraction schedule makes no locality or polynomial-degree claim.

• PR6482 changes centered residue packing for a finite Gaussian numerical backend. It retains that backend and changes an exact residue lane, independently of this abstract oracle precision schedule.

• PR6481 lowers a sufficient orthogonal-witness detector guard using Euclidean accumulation. Its detector and separation contract differ from this fixed-source inverse iteration.

• PR6496 relaxes a QQ16 producer's local operation tolerance by one bit. It uses a different producer ledger and does not compute this oracle precision volume.

Completion refresh inspected this account's fourteen other open PRs created since the advance CLAIM, including the entries above. None supplies a competing fixed-source Horner precision-volume formula in the inspected bodies. No shared computed-number disagreement was identified. No extra mathematical computations checked these PRs. The exact PR1430/fixed-source-Horner open-work searches found no competing precision schedule in the inspected coverage.

CI notes

Both hosted checks passed at exact head 4307d3a0cb8921b58ec2f229fdad41db25849932 in run 41556033667: plan and replay (research/horner-increasing-precision). The completed checks were read once; separate run metadata confirms completed success at that head.

Both registered normal/optimized checks and all required local checks also passed. Hosted replay covers the registered finite corroboration and package/source validation. The universal theorem remains a written proof; no independent human or formal proof-kernel acceptance, physical backend or complete multiplication theorem is implied. No CI failure remains, and no required local check was deferred to CI.

Merge Danger

Door: two-way.

Blast Radius: isolated.

Six new research-package files. Shared code, frozen predecessor sources, other contributors' credit and selected-frontier files are unchanged.