Reduce compact rounded-ADD residue control to linear size (no κ)

research/reverse-horner-residue/PROOF.md

@@ -0,0 +1,137 @@
+# A linear signed-residue phase during numerator rewind
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped constructive proof, corroborated by exact finite execution.
+No new kappa or complete multiplication theorem is claimed.
+
+## Contract and new statement
+
+Use CubeJerry's compact rounded ADD compiler from [PR6990](https://github.com/CrocSwap/integer-mult-bounds/pull/6990).
+For a fixed reduced rational coefficient `a/b`, write `b=2^d o`, with `o`
+positive and odd. Let `L=max(bitlength(abs(a)),bitlength(b))`, `K=L+2`.
+The inherited numerator construction supplies the signed integer
+
+    N = b*x + a*y + floor(b/2)
+
+in `M=W+K` two's-complement bits on private port 2. Its local layout is
+marker 6, the M bits in least-significant-first order, delimiter 2. At
+`offset-done`, the port-2 head is on that delimiter. Public heads and the
+other private bank obey the inherited contract. Numerator correctness,
+its width bound, subsequent exact division and the lifecycle are credited
+premises here, not new theorems or audit deliverables.
+
+For `o>1`, replace only the outgoing rewind-to-residue edge at each of
+the two component parities. The new phase has exactly `8o+2` graph labels
+and `14o+4` six-opcode rows, counting both parities. It returns the head
+to the first numerator bit and enters the original `drop` state with
+carry `-r`, where `r` is the unique element of `[0,o)` congruent to N.
+It writes nothing, reads no public field and uses no new bank.
+
+For every positive M the phase uses exactly `M+1` virtual reads, `M+2`
+virtual unit moves and `3M+4` executed rows, including the exit goto and
+excluding the first row of `drop`. The old route uses `3M+3` reads,
+`3M+4` moves and `7M+10` rows with the same boundary convention.
+Thus the replacement saves `2M+2` reads, `2M+2` moves and `4M+6` executed
+rows per component. Integral and dyadic coefficients have `o=1`; their
+compiled tables remain identical.
+
+The mathematical graph construction is valid for every finite odd o.
+The executable retains `o<=125` and additionally bounds L by 24, matching
+the coefficient-size range of the cited current compact ADD application.
+No full coefficient catalogue is constructed here.
+
+## Signed backward Horner recurrence
+
+Let the bits be `n_0,...,n_(M-1)` and `s=n_(M-1)`. Then
+
+    N = sum_(j=0)^(M-1) n_j 2^j - s 2^M.
+
+Move once left from the delimiter and read s. Start the finite residue
+state at `h=-s mod o`. Process the bits in descending index order,
+including this first sign bit, using
+
+    h <- (2h+n_j) mod o.
+
+After t processed bits, induction gives
+
+    h = -s 2^t + sum_(j=M-t)^(M-1) n_j 2^(j-(M-t)) mod o.
+
+At t=M this is N modulo o. The final left move encounters marker 6;
+one right move returns to the first bit. The marker separates successive
+components, so the phase cannot cross into a preceding numerator. Neither
+the width nor a power of two needs to be stored. This is classical Horner
+evaluation applied to the supplied signed tape boundary.
+
+The source quotient accepts carry `-r` because `N-r` is divisible by o.
+Its original low-bit discard therefore produces
+
+    floor((N-r)/(o*2^d)) = floor(N/(o*2^d)).
+
+Indeed, writing `N=oQ+r` with `0<=r<o`, the fractional addition
+`r/(o*2^d)` cannot cross the next integer after `Q/2^d`. This argument
+also holds for negative Q. The output is the original nearest-up ADD,
+including representability, cancellation and signed ties. The unchanged
+staging and lifecycle retain whole-target protection on detected failure,
+source preservation, success head return and private-history retirement.
+The proof makes no stronger assertion about malformed external encodings,
+failure rollback or full recursive Controller execution.
+
+## Graph and literal instruction counts
+
+For each parity the labels are one start, `2o` digit labels `(h,bit)`, o
+scan labels and o end labels. A start emits a left move and a sign branch.
+A digit emits a left move and a goto. A scan emits one bit/marker branch.
+An end emits a right move and a goto to the original quotient. Thus there
+are `4o+1` labels and `7o+2` rows per parity. Every residue scan label is
+generated: start with sign zero, then binary strings represent every
+residue once sufficiently many low bits are allowed. Each scan generates
+both digit labels and its marker exit. The counts are consequently exact
+for the generated graph, rather than a minimum-state claim.
+
+During an M-bit execution there is one initial sign read, M digit visits,
+M scan visits including the marker, and one end visit. This gives the
+new operation counts above. The old phase has two full rewinds around
+one forward residue scan. Each rewind takes `M+2` moves and `M+1` reads;
+the forward scan takes M moves and `M+1` reads. Its row count follows
+from two move/branch rewind loops, their move/goto exits, the bit branches,
+the digit move/goto pairs and the res-done goto. No payload writes occur
+on either route.
+
+For canonical nonblank codes in the retained CodedPort, a virtual read
+costs four raw reads and six raw moves. A successful virtual move in
+either direction costs one raw read and three raw moves. The saved
+physical action count is therefore
+
+    10(2M+2) + 4(2M+2) = 28(M+1).
+
+The corresponding reduction in physical actions plus executed rows is
+`32M+34` per component. These are exact operation counts under that
+executor, not wall-time measurements or a supplier-tariff conversion.
+No visited extent or backing requirement increases. The prior positive
+complete primitive bound remains valid; its recursive invoice is not
+changed by this package.
+
+The numerator Horner phases and quotient retain their inherited graph
+bounds. Replacing the residue/power product by this linear phase changes
+the compact graph bound from `O(LK+o^2+Ko)` to `O(LK+Ko+o)`. Nothing here
+claims logarithmic size in the divisor, minimal finite control, a physical
+random-access table lookup, or a better recursive exponent.
+
+## Source adapter and evidence boundary
+
+`adapter.py` authenticates four immutable source files against SOURCES.json.
+It loads the exact named compiler definition in a private namespace with
+an explicit Builder dependency. The new Builder redirects only the two
+exact `rewind(residue(0,1 mod o,2,parity))` edges. It reserves the existing
+quotient entries, lets the original compiler finish its other states,
+then appends the new phase before resolving labels. No predecessor file
+is edited or copied, and no runtime numerical callback is added. Runtime
+tables still contain only branch, write, unit move, goto, halt and reject.
+
+The direct verifier separately interprets every tested new phase, and
+executes complete changed tables through the retained literal lifecycle
+and coded ports. An integer-floor oracle supplies the expected values.
+The old compiler is run only as a resource comparator for the new step,
+not as a scientific audit. The universal result rests on this proof;
+finite execution and source hashes alone do not establish its quantifiers.

research/reverse-horner-residue/README.md

@@ -0,0 +1,155 @@
+# Linear signed residues with two fewer numerator traversals
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped constructive proof with exact finite corroboration.
+The compact rounded ADD of CubeJerry's [PR6990](https://github.com/CrocSwap/integer-mult-bounds/pull/6990)
+can compute its signed odd residue during the existing numerator rewind.
+The new phase has exactly `8o+2` graph labels and `14o+4` literal rows,
+counting both component parities. It stores no power of two. The complete
+graph bound becomes `O(LK+Ko+o)` in place of `O(LK+o²+Ko)`.
+
+For an M-bit numerator, the change saves exactly `2M+2` virtual reads,
+`2M+2` virtual moves and `4M+6` executed rows per component. Under the
+retained coded-port executor, this is `28(M+1)` physical tape actions.
+Both private banks, the complete rounded map, staging, cancellation,
+source preservation and successful cleanup contracts are retained.
+[PROOF.md](PROOF.md) states the boundaries and all-width proof.
+
+The three source-compatible coefficient fixtures give these generated
+fixed-table row counts. The old compiler is a resource comparator for
+the new step; its scientific result is not audited here.
+
+| Coefficient | Original rows | New rows | Rows removed |
+|---|---:|---:|---:|
+| -14729531/163840 | 100,033 | 99,807 | 226 |
+| -1379/250 | 187,806 | 38,300 | 149,506 |
+| 1085645/393216 | 76,560 | 76,494 | 66 |
+
+These are enumerated instruction counts, not timing measurements. No
+new kappa, selected-frontier change or complete multiplication theorem
+is claimed. This is an opt-in compiler adapter; no production file changes.
+
+## Reproduction and evidence
+
+From the repository root, use CPython 3.12 and its standard library:
+
+```sh
+/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
+```
+
+Substitute another CPython 3.12 path on another machine. The direct marker
+is `PASS_REVERSE_HORNER_RESIDUE` in a generated JSON stdout receipt bound
+to all package-file hashes. Nothing is written by replay. The last command
+requires committed package bytes and full Git history.
+
+The verifier separately interprets 63,240 signed phase executions, covering
+every bit string of widths one through eight, both parities and every odd
+divisor from 3 through 125. It enumerates 31,868 phase labels and 55,800
+phase rows across those 62 graphs and checks the exact operation counts.
+Complete changed tables execute through the retained Controller primitive,
+coded ports and lifecycle on 2,720 exhaustive ADD calls, with 2,298 successes
+and 422 correct range rejections. Three additional cancellation fixtures
+produce `(-80,0)`, `(-4,0)` and `(1,0)`. Their physical-action and executed-row
+savings agree with the proved formulas.
+
+Two deliberately damaged signed-Horner constructions each fail on four of
+eight enumerated three-bit words. Long-to-short dirty-bank reuse, a late
+whole-field overflow, reuse after that rejection, and invalid coefficient
+guards are checked. Dyadic and integral tables equal the original tables
+exactly. All checks remain active under optimized Python. The written proof
+supplies the universal statement; these finite domains do not replace it.
+
+## Scope, source binding and limits
+
+The question refines the economical fixed-graph opening in CubeJerry's
+[PR6988](https://github.com/CrocSwap/integer-mult-bounds/pull/6988), Open next
+question 1. PR6990 already supplies the compact numerator construction;
+this package contributes the smaller, shorter signed-residue phase.
+Horner evaluation, two's-complement arithmetic and graph substitution are
+classical. No global literature-priority claim is made.
+
+The executable accepts exact rational coefficients with `L<=24`, odd part
+`o<=125`, and a finite construction cap of 500,000 labels and 2,000,000 rows.
+Exceeding a cap rejects explicitly. The mathematical local phase works for
+all positive bit widths and finite odd divisors. The inherited numerator,
+quotient, external-format and lifecycle premises remain required.
+
+The adapter reads four exact live sources declared in [SOURCES.json](SOURCES.json)
+and [VERIFY.json](VERIFY.json). It injects a private Builder into the exact
+named source compiler definition, replaces two known construction edges
+and emits ordinary immutable six-opcode tables. Runtime payload execution
+contains no adapter callbacks. Source hashes are checked before parsing or
+execution, and Python bytecode caches are bypassed by compiling those bytes.
+No predecessor file or attribution line is changed or copied.
+
+Base is canonical main `e54523517d0f03e58352e647c403a5af3e525a57`, priority
+revision 8, selected #7000. The selected metadata baseline passed; it is not
+a scientific replay. The `uniform-transfer-audit` card explicitly changes
+scope to a local implementation improvement. Its five-assumption goal is
+not claimed. [The advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19542452)
+records this boundary. Main README searches, merged/open PR searches,
+recent account work, live handoffs and local reservations were checked.
+The overlap helper covers all 558 cached open PRs and 7,226 Discussion
+records, but only 222 of 10,178 local notes. Unpublished work, omitted notes
+and arbitrary historical diffs remain coverage limits.
+
+Full catalogue/recursive source binding, complete physical supplier tariffs,
+native operators, production coefficient installation, outer recovery and
+the selected cold replay remain unrun. No independent human or formal
+proof-kernel review is claimed. The selected five framework assumptions
+retain their status.
+
+## Implementation bounds
+
+New functions are shorter than 60 lines. There is no recursion, network,
+child process, shared-file mutation or persistent payload cache. Coefficient
+and graph caps bound the inherited construction queue; the new-phase loop
+has at most `8o+2` iterations. Test domains and literal phase step budgets
+are explicit. Inherited runtime loops are justified by their cited finite
+word and lifecycle contracts and by the local decreasing-width proof.
+Warning-strict normal and optimized development-mode execution provide
+local Python diagnostics. Ruff, Mypy and Pyright are unavailable on PATH.
+
+Power-of-ten rule 3 has a managed-Python allocation deviation. Graph
+construction and exact verification allocate bounded Python collections
+and integers. No fixed-allocation runtime claim is made for the verifier;
+the generated table carries the target's finite control. A larger-domain
+backend would need a separate capacity contract. Rules 8 and 9 have a
+construction-only source-loading and dependency-injection deviation.
+Only four hash-authenticated source files, fixed named definitions and two
+Builder classes are admitted. The new local interpreter, complete coded
+execution, identical dyadic controls and negative constructions check this
+seam. A future production integration can expose a direct Builder parameter
+instead; modifying frozen predecessors is outside this package.
+
+## Open next questions
+
+1. Install this phase through an explicit public Builder parameter in a
+   versioned production compiler. Begin with the two redirected edges and
+   preserve source pins, primitive lifecycle and finite-control charges.
+   Shared-code adoption and its downstream consumers remain separate.
+2. Share the power-free residue graph among the full current coefficient
+   catalogue while retaining exact source tokens. First group coefficients
+   by odd divisor and bind each quotient continuation. Full catalogue and
+   recursive field delivery are not supplied here.
+
+## 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. The open rounded
+MOVE, inverse-code recovery and tensor-extraction packages have different
+operators and contracts. No numerical agreement or disagreement is inferred.
+
+## Credit
+
+CubeJerry / Jerry Chen supplied PR6988's rounded scalar boundary, PR6990's
+compact ADD compiler, exact Builder, coded-port lifecycle and physical
+fixtures. DreamingOfClouds supplied the #6936 word and #6937 rounded-division
+proposal. The original packages retain their full contributor lineage,
+including Nick Petalas's older one-carry work. The new signed-residue
+construction, source adapter, scoped proof and verifier were produced by
+Nick Petalas.

research/reverse-horner-residue/SOURCES.json

@@ -0,0 +1,66 @@
+{
+  "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/compact-rounded-add/tables.py",
+      "usage": "input",
+      "git_blob": "b90ecb6052e270095fdd048f992f9fc786f3f8c7",
+      "sha256": "fe8a28fd523ebb7ec78dce4ba0855b3070a6cbff470602cd62f8d3ff445e0f0a"
+    },
+    {
+      "path": "research/compact-rounded-add/vendor/exact_scalar_tables.py",
+      "usage": "input",
+      "git_blob": "1cc22f75fbe53d48b84be42782e581c04820cd49",
+      "sha256": "654e9734ef80a9394807ca508543b1bc164afb5768d23d0e5a88c790d2f13bac"
+    },
+    {
+      "path": "research/compact-rounded-add/vendor/machine.py",
+      "usage": "input",
+      "git_blob": "acf475e4fccaff2fb64bd5b0b3f3fc0d246dc592",
+      "sha256": "ec597bce13275003ff30e4be481c936401826c1d4af642b55eec0c410774d1df"
+    },
+    {
+      "path": "research/compact-rounded-add/vendor/physical_fixture.py",
+      "usage": "input",
+      "git_blob": "027b563887fd748438d0d0dc7a75f356b29986bd",
+      "sha256": "b0eb6f2db2deff9104cdf786a8ae84b0d4864b09a1f9b99178cb08c1666d014e"
+    },
+    {
+      "path": "research/current-rounded-scalar-tables/README.md",
+      "usage": "provenance",
+      "git_blob": "06f74137fa17e34bebbd66d588eb6d514affdb0e",
+      "sha256": "9f3b3674f43dc16c3487412cf2be36f20c8772c12624419b7f484803fb1312c1"
+    },
+    {
+      "path": "research/current-rounded-scalar-tables/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "498145c6ac72b3c2ef7a0adf166570f4073b68ca",
+      "sha256": "ebf8634a004ef9371831171ae5ed1bcbe55e9c2931b56d8113556f27f8ded830"
+    },
+    {
+      "path": "research/compact-rounded-add/README.md",
+      "usage": "provenance",
+      "git_blob": "e10734f0b270562707dc2f67166fd3641a093d3e",
+      "sha256": "1fb0f5c63875e42592d02ca2e0d9ad134190b87017c5ac55d11a66c643e66067"
+    },
+    {
+      "path": "research/compact-rounded-add/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "07d0ad2d714c5e6e4b0b03db78657bf8d6a63bf9",
+      "sha256": "80035605d92c0a1cceb1f802f4adcfeb1b60590a4b7335b612f8c4f67079ceb0"
+    }
+  ]
+}