Share the paired residue sampler bank in 84,578 bytes (no new κ)

research/shared-residue-dispatcher/PROOF.md

@@ -0,0 +1,118 @@
+# A minimal shared forward dispatcher
+
+## Model and inherited graph
+
+Fix `a,b` in `{1,...,12}`. The four output labels are ordered `00,01,10,11`.
+Use zxv's ordered-coin graph from [PR #6072](https://github.com/CrocSwap/integer-mult-bounds/pull/6072),
+at `9011bf83e85ecd0443c789cf03259442f750877d`. This section states the graph
+definition so the new result has no runtime dependency on that pending PR.
+Its sampling law and expected-bit optimality are inherited, not new claims.
+
+Put `D=169`, `L=156` and
+
+\[
+w=((13-a)(13-b),(13-a)b,a(13-b),ab),\qquad
+r_{i,k}=2^k w_i\bmod D,\qquad
+n_k=\frac{\sum_i r_{i,k}}D.
+\]
+
+Internal states are `(k,j)` with `0<=k<L`, `0<=j<n_k`, ordered by phase and
+then node. The root is `(0,0)`. Let `d_i=floor(2 r_{i,k}/D)`. Form a list of
+the output labels `i` with `d_i=1`, in increasing order. From `(k,j)`, coin
+`u` selects child index `v=2j+u`. If `v<sum_i d_i`, return the label at
+zero-based index `v` in that list. Otherwise go to
+`((k+1) mod L, v-sum_i d_i)`. This is the subtraction rule
+of #6072 written as an ordered list. Each pair has 312 internal states.
+
+Take the disjoint union for all 144 ordered pairs, and identify only the four
+matching output labels. Its internal states are `s=312*(12*(a-1)+b-1)+q`,
+where `q` is the local phase/node index. There are 44,928 internal states and
+four output states. Add absorbing self-loops at each output for the proof.
+They are not stored as transition rows in the emitted table.
+
+A state has observation `pending`, `00`, `01`, `10` or `11`. Equivalence means
+equal observation after **every finite binary continuation**. Thus it preserves
+the first stopping depth, output, and also nontermination for every infinite
+tape. The configuration may be used to select an entry state. After entry,
+all information governing transitions must be in the counted state. The model
+does not grant a separate free parameter oracle, output relabelling or coin
+reordering.
+
+## Stable refinement is exact equivalence
+
+Let `P_0` group states by their empty-word observation. Obtain `P_(k+1)` by
+grouping states with the same observation and the same two `P_k` successor
+classes. Induction on `k` proves that two states share a `P_k` class exactly
+when all continuations of length at most `k` have equal observations.
+
+These partitions refine monotonically. If two consecutive partitions have
+the same number of classes, they are the same equivalence relation. Successor
+classes then define a well-defined quotient. Induction on continuation length
+proves equality of all finite observations in each quotient class. Conversely,
+each pair separated during refinement already has a finite distinguishing
+continuation. Thus the stable partition is exactly the required equivalence.
+This is classical Moore state minimization, not a new minimization algorithm.
+
+The complete finite refinement certificate gives these class counts, including
+the four distinct output labels:
+
+```text
+depth     0   1   2    3     4     5      6      7      8      9     10
+classes   5  15  56  282  1850  7426  14824  20274  22450  22486  22486
+```
+
+Consequently the minimal quotient has **22,482 internal states**. The verifier
+checks every refinement using separately sorted signatures, every original
+transition under the quotient map, all 144 entry pointers, output separation
+and reachability of every state from the entries. It checks all 89,864 original
+edges including the eight artificial absorbing edges. These are complete finite
+checks, not a statistical sample.
+
+All distinct residual behaviors have a distinguishing continuation of length
+at most nine. Nine is needed: states 244 and 8149 share their depth-eight class
+but separate at depth nine. The verifier extracts continuation `111111100`
+and checks their different observations directly.
+
+## Minimality in this model
+
+Every original state is reachable from some entry by a finite coin prefix.
+Suppose a deterministic forward dispatcher implements all 144 same finite-tape
+functions. If two such prefixes reach the same counted internal state, their
+remaining finite-tape observations must agree. Therefore distinct residual
+classes cannot share that state. The 22,482 reachable pending classes require
+at least 22,482 internal states. The quotient attains the bound.
+
+This is a state minimum for these **fixed ordered-coin functions**, not a
+minimum among all samplers with the same probability law, a ROM byte minimum,
+or a lower bound for a machine with extra uncounted registers. Four terminal
+codes are included in the encoding; a physical implementation need not retain
+four halted controller states.
+
+## Packed bank and exact preservation
+
+Assign consecutive codes to the quotient's internal states and then its four
+outputs. All 22,486 codes fit 15 bits. Each of the 22,482 internal states has
+two stored targets. The transition payload therefore has
+
+\[
+\left\lceil\frac{2\cdot22482\cdot15}{8}\right\rceil=84308
+\]
+
+bytes. Lexicographically ordered entries for all 144 pairs use
+`144*15/8=270` bytes. The complete packed bank payload is **84,578 bytes**.
+The separate resident bank in #6072 uses `144*702=101088` bytes, with the
+configuration selecting its table and every local entry equal to zero.
+The shared payload saves **16,510 bytes**, including the new entry table.
+These counts omit interpreter code and headers on both sides.
+
+Every code is packed and independently unpacked in the replay. Since the
+quotient preserves each original transition and preserves pending versus
+output, induction on consumed coins preserves output and stopping depth on
+every tape. Hence any inherited sampling law and expected number of draws
+are unchanged. The separate 36,864 eight-coin tape comparisons are controls;
+the complete homomorphism is what covers arbitrary tape length.
+
+The quotient certificate does not require predecessor uniqueness. No reverse
+transition or transfer of [PR #6102](https://github.com/CrocSwap/integer-mult-bounds/pull/6102)'s
+cleanup contract follows. No bounded stopping time, fresh returned randomness,
+physical lookup/selection tariff, complete caller or new kappa is proved.

research/shared-residue-dispatcher/README.md

@@ -0,0 +1,123 @@
+# A smaller shared bank for paired denominator-13 sampling
+
+The 144 ordered-coin graphs of zxv's [PR #6072](https://github.com/CrocSwap/integer-mult-bounds/pull/6072)
+have a shared forward dispatcher with **22,482 internal states**, down from
+44,928 in their disjoint union. Its packed transition bank and 144 entry pointers
+use **84,578 bytes**, down from 101,088 bytes for all separate resident tables.
+This saves **16,510 bytes** while preserving every finite coin-tape output and
+its first stopping depth. The state count is minimal for those fixed ordered-coin
+functions when all residual information is in the counted controller state.
+
+Claim type: **finite certificate with a scoped proof of minimality**.
+This answers the logical state-sharing part of #6072's second Open next question.
+The physical control-cost question remains open. This is a new shared
+construction, not a re-check of its predecessor's sampling law or optimal means.
+No supplier or new kappa is claimed.
+
+## What is compared
+
+The comparison is between a resident bank of all 144 configurations and one
+shared resident bank. The predecessor can instead generate and store only one
+702-byte configuration. The shared bank is not smaller than that single-table
+working set, and no runtime speedup is measured.
+
+The new encoding stores two 15-bit targets per internal state, plus 144 15-bit
+entry codes. It needs 84,308 transition bytes and 270 entry bytes. The last
+transition byte has four unused high bits. Interpreter code, layout headers,
+table preparation, parameter selection, lookup, random-tape motion, outputs
+and cleanup are outside these payload counts.
+
+## Evidence and reproduction
+
+From the repository root, with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/shared-residue-dispatcher
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/shared-residue-dispatcher --check-source-history
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/shared-residue-dispatcher/verify.py
+```
+
+The first command runs both registered normal and optimized checks. The
+publication check requires the package to have been committed. Elsewhere,
+replace the absolute interpreter path with a local CPython 3.12 executable.
+
+Expected status is `PASS_SHARED_RESIDUE_DISPATCHER`, with 144 configurations,
+22,482 minimal internal states, 84,578 shared bytes, 36,864 literal tape controls
+and five rejected certificate corruptions. Default replay writes no files.
+
+To produce the actual packed bank and a generated hash-bound receipt, point
+both output options at a scratch directory outside the checkout:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/shared-residue-dispatcher/verify.py --emit-dir "$HOME/.cache/imb-shared-bank" --receipt "$HOME/.cache/imb-shared-bank/receipt.json"
+```
+
+The exact packed payload hashes are:
+
+```text
+transitions.bin  a91f1d6fd9ba664e6e7de4ebda0121a5049ae129753669780f72651b0da0f8d1
+entries.bin      08debab375f7fb0cdb7b07d43305239e36cf2edb8b3186ca052324a86e8b1d69
+```
+
+[PROOF.md](PROOF.md) defines the entire input graph and proves the refinement,
+minimality and payload claims. `dispatcher.py` constructs the quotient;
+`verify.py` checks the complete transition homomorphism, all refinement splits
+using a separate sorting implementation, reachability, packing, finite tapes
+and rejection controls. Distinguishing continuations of length at most nine
+separate every inequivalent pair; a checked pair needs nine.
+
+## Sources, scope and limitations
+
+The exact predecessor is #6072 head
+`9011bf83e85ecd0443c789cf03259442f750877d`, especially its
+[`make` definition](https://github.com/CrocSwap/integer-mult-bounds/blob/9011bf83e85ecd0443c789cf03259442f750877d/research/paired-residue-sampler/verify.py)
+and [written graph specification](https://github.com/CrocSwap/integer-mult-bounds/blob/9011bf83e85ecd0443c789cf03259442f750877d/research/paired-residue-sampler/README.md).
+The graph is stated and constructed locally. Replay needs no network, pending
+Git objects, predecessor imports or third-party packages. `SOURCES.json` pins
+the historical task and selection as provenance, not scientific inputs.
+
+The original `supplier-boundary-audit` card is changed to a constructive
+sampler-table question rather than an audit or admission replay. This side
+result reduces one logical inventory that a future stochastic inverse service
+could use. It does not resolve that service's physical bill. The selected
+record at base `721c03822c421b7f7fcbb2598993b947c4d88419` is PR6030,
+conditional kappa 0.003125804, with all five assumptions retained.
+
+Minimality requires unchanged output order and unchanged behavior on each
+ordered coin tape. A different sampler with the same law, a parameter oracle,
+output recoding, arithmetic control or compressed ROM can escape the statement.
+The state minimum does not prove a byte minimum. Unbounded stopping remains.
+Phase sharing can lose the inverse uniqueness needed by #6102; that reversal
+is not transferred. No physical tape/native replay, selected scientific replay,
+formal proof-kernel check or independent human review was run.
+
+## Implementation bounds
+
+The standard-library implementation uses dynamic allocation with explicit
+finite limits, rather than fixed-memory real-time execution. There are at most
+44,932 graph states, 144 roots, 16 refinement rounds and 16 bits per packed
+code. Failure to stabilize within the cap raises an error; the declared graph
+stabilizes at round ten. No recursion is used. The retained histories and sorted
+signatures are bounded by these limits. Every function stays below 60 lines.
+Warnings are errors in both registered modes. No repository-wide analyzer or
+configuration changes are made for this isolated research package.
+
+## Open next questions
+
+- Can a physical finite-tape dispatcher exploit the shared bank after charging
+  residue selection, packed lookup, output storage and coin movement? Start
+  with one actual nonadaptive residue pair and compare against on-demand table
+  generation. Neither side's physical bill is supplied here.
+- What retained information would make a phase-merged dispatcher reversible?
+  Start with #6102's predecessor-uniqueness condition and one merged pair.
+  Forward equivalence alone does not permit transferring its cleanup protocol.
+
+## Credit
+
+This result was produced by Nick Petalas. Apache-2.0. zxv's #6072 supplies the
+ordered-coin graphs, denominator-13 catalogue, sampling law, expected-bit
+optimum and the sharing question. Moore refinement and residual-state
+minimality are classical. The new contribution is this exact shared quotient,
+its scoped state minimum, complete certificate and packed-bank construction.
+JoyboyBrian's inverse and #6102 reversal, the classical DDG lineage, and the
+retained arithmetic predecessors keep their attribution.

research/shared-residue-dispatcher/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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"
+    }
+  ]
+}