[petalas]

Summary

Scoped constructive proof with exact finite corroboration: compute the signed odd residue during the compact rounded ADD's numerator rewind. The new phase has exactly 8o+2 labels and 14o+4 literal rows across both component parities. The complete graph bound changes from O(LK+o²+Ko) to O(LK+Ko+o).

 numerator ready at its delimiter
- rewind; forward residue/power scan; rewind
+ backward signed Horner residue during one rewind
 unchanged exact quotient and low-bit discard

For an M-bit numerator, the replacement saves 2M+2 virtual reads, 2M+2 moves, 4M+6 executed rows and 28(M+1) physical coded-tape actions per component. It retains both private banks, rounded semantics, cancellation, source preservation, whole-field staging and successful cleanup.

This contribution was produced by Nick Petalas. Credit CubeJerry / Jerry Chen's #6988 economical-graph question, #6990 compact ADD scaffold, exact Builder, lifecycle and fixtures; DreamingOfClouds' #6936 word and #6937 rounding proposal; and the full retained predecessor lineage. Horner evaluation is classical. The contribution is this source-bound smaller phase and its proof, adapter and verifier.

Evidence

The generated table for -1379/250 has 38,300 rows, compared with 187,806 for the original compiler. The other two supplied coefficient fixtures remove 226 and 66 rows. These are enumerated instruction counts, not wall-time speedups. The original compiler is used as a resource comparator for the new step.

Local checks on 618ff7af4ac85c63ee2c39acc69bf763ed35b60a passed:

• 63,240 independently interpreted signed residue executions, every width-1-through-8 bit string, both parities, and all 62 odd divisors from 3 through 125.
• 2,720 complete changed ADD calls through the retained literal lifecycle: 2,298 successes and 422 correct range rejections. Three further cancellation fixtures produce (-80,0), (-4,0) and (1,0).
• Exact graph and operation counts, identical dyadic/integral tables, two detected semantic mutants, dirty-history reuse, late whole-field overflow and subsequent reuse.
• Normal and optimized warning-strict checks produced identical generated hash-bound receipts. Each took under six seconds locally. Registered replay passed; committed-byte/source-history preflight passed for all 11 package/input files.

From the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/reverse-horner-residue/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -X dev -B research/reverse-horner-residue/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/reverse-horner-residue
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/reverse-horner-residue --check-source-history

Another CPython 3.12 path may be substituted. The direct marker is PASS_REVERSE_HORNER_RESIDUE. Replay writes no files.

Limitations and unrun obligations

The mathematical local phase covers every positive width and finite odd divisor. The executable retains o<=125, bounds coefficient length by 24 and enforces finite graph caps. It authenticates four live source files and injects a private Builder into the exact named compiler definition. Runtime tables use only the existing six opcodes.

The inherited numerator, quotient, canonical-format and lifecycle contracts remain premises. Full coefficient-catalogue and recursive source binding, production installation, complete physical tariff conversion, native/outer recovery and the selected cold replay are unrun. No new kappa, selected-frontier change, complete multiplication theorem, independent human review or formal proof-kernel acceptance is claimed. The five selected framework assumptions remain.

Open next questions

• Expose a direct Builder parameter in a versioned production compiler, preserving the two entry edges, quotient continuations, source pins and lifecycle charges.
• Share power-free residue graphs across the complete coefficient catalogue while retaining exact local source tokens and recursive field delivery.

Related open work

No open PR targeting this signed-residue prepass or compact rounded-ADD table-size quantity was found in the live targeted search. Open rounded MOVE, inverse-code recovery and tensor-extraction work concerns different operators. No numerical comparison with those packages is claimed.

CI notes

CI did not certify this package. At unchanged head 618ff7af4ac85c63ee2c39acc69bf763ed35b60a, run 43030221243, plan job 130555044132, failed in "Onboarding helper tests". The package replay job was skipped because plan failed.

I read the checks and job log. The step ran 760 tests with 24 skipped and exactly one failure:

test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record
AssertionError: '`make frontier7000-verify`' not found in the CI verification document
FAILED (failures=1, skipped=24)

This mismatch is present in the base main commit e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md still opens with "Current selected-family replay: #6030" and names make frontier6030-verify. This PR changes neither file; it adds only research/reverse-horner-residue/.

I also read the failed logs of run 42905094314, run 42903313790, and run 43029932349. Each shows the same single failing test, the missing make frontier7000-verify assertion, 760 tests run and 24 skipped. No broader run coverage is claimed.

The verification evidence for this package remains the local normal/optimized, registered replay and committed-byte/source-history checks listed above. No fix, retrigger commit or workflow rerun was made.

Merge Danger

Door: two-way.

Blast Radius: package. Only the new scoped research directory changes.