Certify sharp payload/key storage for selected BIT owner routes

research/selected-route-live-volume/README.md

@@ -0,0 +1,114 @@
+# Sharp live payload/key storage for the selected BIT owner route
+
+This closes one storage component of Jose Manuel's pending [PR2697](https://github.com/CrocSwap/integer-mult-bounds/pull/2697), pinned at `a53fdf4bcbe33c6732f0bec1badc8c023380f9d1`. Its complete first-node caller leaves route temporaries as `O_q(v)+O(V/W)` and total numerical reserve open. Here the unchanged `route_packet` has an exact live-content peak, including its borrowed input:
+
+```text
+w > 1:  2v + 3H(R+J)
+w = 1:  2v + 2HR + HJ
+```
+
+These are proved for the source routine's well-formed successful runs. Eight complete small fixtures attain the formulas when executing that same routine. This is a component certificate and a scoped caller corollary. It does not establish a total reserve, admit a supplier or change kappa.
+
+Coordination: [Discussion2319 claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-18954841). Base main `b5ea56e0a5ac4552166253b1fa4be0753bb38c30`, priority revision 5. The selected record remains unchanged.
+
+## Contract and counted storage
+
+Let q be an odd prime, d the fixed matrix dimension, w a positive payload precision, and `cap=q^(w-1)`. Set
+
+```text
+H = cap^(d*d)                complete high matrices per old prefix
+C >= 1                      physical old-prefix count, repetitions retained
+R >= 1                      payload symbols in one high-matrix fibre
+t = HR                      one complete high cube
+v = CHR                     one packet
+J = d*d*(ell+1)              serialized route key
+```
+
+Here ell is the actual residue arena's fixed binary word length, including its supplied padding. Each of the d*d key words contributes ell binary symbols and one WORD_END delimiter. No minimal encoding assumption is needed. The compiled route must act bijectively on the complete high cube and satisfy the retained source context/word-margin contracts. Every factory invocation creates a fresh, distinct, initially empty tape. The input is exactly v contiguous binary payload symbols and is retained unchanged.
+
+The count is the number of simultaneously nonblank payload and embedded-key symbols on route tapes, excluding each tape's LEFT marker. Cleared symbols cease to contribute even if the Python bytearray remains allocated. Numerical arena words, counters, context, fixed compilation, tape markers, provenance dictionaries and other Python heap capacity are excluded. This is deliberately narrower than occupied tape volume or process memory. The source's exact abstract tape semantics and ordinary ownership discipline are premises.
+
+## Lifetime proof
+
+Write `K=H(R+J)=t+HJ` for one decorated cube. Its content has a fixed length independent of key values, bucket balance, route chart or input bits.
+
+In `partition`, the current decorated cube retains K symbols. During bucket filling, the two buckets have combined content at most K; the separate key scratch has at most J symbols and the following output is empty. Thus the total is at most `2K+J <= 3K`, since H and R are positive. During bucket concatenation the key scratch has been cleared, while the buckets, current input and growing following output contribute at most 3K. At the final appended output symbol they contribute exactly 3K. The buckets are only cleared in `partition`'s finally block. Clearing current occurs later in `route_cube`, after partition returns.
+
+During decoration, `route_cube` has at most K decorated symbols, plus numerical scratch excluded above. During key stripping it retains the decorated input and grows a pure output of size at most t, giving at most `K+t <= 3K`. A partition therefore determines its sharp internal peak when cap>1. There is at least one partition because d>=1, ell>=2 and cap>1. If cap=1 there are no partitions, H=1, and the sharp internal peak is K+t at completion of key stripping.
+
+For old prefix p, numbered 0 through C-1, `route_packet` retains its original v-symbol input, the already completed outer output of length pt, and a separate local cube of length t while `route_cube` runs. Consequently for cap>1 its peak is
+
+```text
+v + pt + t + 3K <= 2v + 3K.
+```
+
+Equality occurs in the final partition of the final old prefix, before any bucket or current cleanup. The copy from the returned pure cube into the outer output has at most `v+pt+3t <= 2v+2t`, below that peak. For cap=1, replace 3K by K+t and obtain `2v+K+t = 2v+2t+HJ`, attained at the final prefix's key-stripping completion. The final result and borrowed source each have size v; all other counted content is cleared.
+
+This proves both universal equalities for the fixed routine, rather than a lower bound for every possible routing algorithm. Different disposal timing or a different route can change the result.
+
+## Consequence for the caller's gather/route/return/scatter phases
+
+In PR2697, let N be the number of low GL classes, W the number of family streams, `V=WNv`, and r the number of staged roles. Its stated selected values are W=28416 and r=661. Treat these as the caller's authenticated geometry; this package does not replay the full selected catalogue or node.
+
+When the last role is gathered and routed, r-1 completed packets remain alongside the route input. During inverse routing, all r staged packets remain, but one is already included in the route's borrowed-input charge. Thus both phases are bounded by
+
+```text
+(r+1)v + 3H(R+J).
+```
+
+Scatter has a different overlap. All r staged packets and the returned packet of size v survive while `selection.scatter` builds a replacement whole family of size Nv. The old family is already counted among the W live families and is cleared only after scatter returns. Hence gather, routing, return and scatter, apart from the retained source/peeled/family streams, are bounded by
+
+```text
+(r+1)v + max(Nv, 3H(R+J)).
+```
+
+`Node.run` retains at most 3V in protected input, peeled output and live family streams during those phases. Final merge can add a full V before cleanup. A joint bound for these phases and final merge is therefore
+
+```text
+max(4V, 3V + 662v + max(Nv, 3H(R+J))).
+```
+
+This excludes literal local-word execution, COPY, residual/primitive interiors, peel interiors, directory production, counters and numerical/control storage. In particular COPY can briefly retain 661 roles, a cloned input and a returned private packet, 663v before residual-internal work. The displayed phase bound must not be applied to that interval. No historical `5V+19v` reserve or complete-node allocation is imported.
+
+## Replay and evidence
+
+Use Python 3.12 with only the standard library:
+
+```sh
+python3.12 scripts/research_package.py --package research/selected-route-live-volume --check-only
+python3.12 scripts/research_package.py --package research/selected-route-live-volume
+python3.12 -I -O -B research/selected-route-live-volume/verify.py
+```
+
+`SNAPSHOTS.json` records exact PR2697 paths, Git blobs and SHA256 hashes. The verifier checks all 16 snapshots before importing any retained code. Twelve required runtime modules are retained byte-for-byte, together with the caller proof, driver, node and attribution notice. These runtime bytes came through PR2569; their inherited notices and dependencies are preserved. The new checker changes no source file or route operation. It supplies a measuring Tape factory and temporarily replaces only the route's private key-tape constructor.
+
+The eight fixtures use q=3 or 5, d=1 or 2, w=1 through 3, C=1 through 3 and R=1 through 5. Each exercises the complete declared high cube, up to 625 matrices. The 1,298 Boolean positions carry independent origin labels through actual copy operations. A separate integer modular-multiplication oracle checks every output origin and bit. Both partitioned and nonpartitioned cases attain the proof's exact peak. A direct scan of every retained measuring tape independently counts the first attained peak, and the exit census checks source preservation, head reset and cleared temporaries.
+
+Seventeen behavioral checks reject input/output-only budgets and premature current/bucket disposal budgets for all eight fixtures, then exercise a nonbinary payload failure with preserved borrowed input and erased owned payload buffers. Seven integrity groups cover a Git-free optimized replay, corrupt route/record/driver snapshots, a bool-for-integer receipt mutation, overwrite refusal and internal-output refusal. The receipt is checked with exact type-sensitive JSON comparison. To regenerate, use `--write-result` with a new path outside the package and compare it with RESULT.json.
+
+Validation passed on macOS arm64 with CPython 3.12.15 through the registered launcher and its seven integrity groups, and on CPython 3.14.8 with optimized assertions disabled and warnings treated as errors. The six repository replay-selection tests passed. Separate internal proof/source review also passed the optimized replay, integrity checks and exact source comparisons; no independent human review is claimed.
+
+The general theorem is the written lifetime proof. The tests are finite implementation evidence, including arbitrary Boolean origins on small cubes. They do not execute the enormous selected GL64 domain or prove the inherited native/compiler semantics. ValueError cleanup is checked for contiguous tapes without internal BLANK holes. Arbitrary exception cleanup and numerical scratch cleanup on malformed inputs are not claimed.
+
+## Verification design and deviations
+
+Build the Lever led to a retained-source replay and literal write counter instead of a hand-counted receipt. Prove It Works led to exact permutation/origin checks and an independent peak census on the actual route. No production code is changed.
+
+Power of Ten inspection covers the new verifier, tracker and integrity command. There is no recursion. New fixture execution is fixed at eight contexts with at most 625 high matrices, 3 prefixes and 5 fibre symbols. The receipt comparator stops after 20,000 nodes; integrity subprocesses have 90-second timeouts; registered commands have finite 120-second timeouts. New functions remain below 60 physical lines. Executable contracts remain enabled under -O. Syntax validation and warning-as-error replays are run; no separate static type checker or linter is installed.
+
+Rule 3, memory allocation: Python and the retained tape interpreter allocate during execution. Scope is this finite offline verifier. The fixed fixture list bounds all tapes, keys and origin dictionaries; the tracker retains cleared tapes for the independent census, so its own memory must never be used as the theorem's storage measure. Each successful fixture closes its arena and clears source/result. Follow-up if extending the domains is to calculate a new allocation cap before changing the fixed fixtures.
+
+Rules 8/9, instrumentation: the inherited factory interface and one temporary routes.Tape replacement provide two explicit measuring-constructor targets. The context manager restores the original target on every exit. This is checker-only instrumentation, with bounded targets and no dynamic code evaluation. Follow-up for production use would be an explicit upstream observer interface, outside this component's scope.
+
+Frozen predecessor code retains tape-terminated loops, dynamic Python allocation and methods exceeding one page. Rewriting them would destroy the byte-exact subject of this audit. Their execution is bounded here by the finite complete cubes, fixed word lengths and registered timeouts; no repository-wide Power of Ten compliance is asserted.
+
+## Open next questions
+
+1. What explicit reserve covers the residual and primitive interiors alongside this caller phase bound? Start with one PR2697 residual ENTER/RETURN, retaining its input, output and the 661 role buffers. Missing lifetime bounds for its directories, counts, coefficient pages and leaf work still block total reserve admission.
+2. Can early bucket disposal or avoiding a local cube reduce this routine's peak without changing its complete-fibre semantics? First propose a changed literal ownership schedule and check it against the same origin and peak tests. This is an optimization opportunity, not needed to retain the present audit. A new route requires its own proof and source pin.
+
+## Credit and scope history
+
+Nick Petalas prepared this component audit. Jose Manuel/jmbarrancoml supplied PR2697's first-node caller and PR2569's source packets, routes and selected lineage. ywz65 supplied PR2590's cubic setup correction and PR2688's separate directory-storage component. The retained NOTICE.md credits the stream and tape framework, Douglas Colkitt, the selected hosting/word contributors and the source527/compiler lineage. Their construction and code are not claimed as new here. New work follows the repository's Apache-2.0 license.
+
+This follows the live total-live-volume handoff rather than the task picker's initial complex-mechanism suggestions. TASK.json declares a changed scope from the selected-stock-envelope card's complete stage recurrence to one actual pending caller component. PR2688 handles a different component. No family expansion, formal-kernel or independent human verification, full supplier replay, selected cold replay or new exponent is claimed.

research/selected-route-live-volume/RESULT.json

@@ -0,0 +1,103 @@
+{
+  "cases": [
+    {
+      "depth": 1,
+      "dimension": 1,
+      "fibre": 1,
+      "high_count": 1,
+      "key_symbols": 4,
+      "output_sha256": "4bf5122f344554c53bde2ebb8cd2b7e3d1600ad631c385a5d7cce23c7785459a",
+      "peak": 8,
+      "prefixes": 1,
+      "q": 3,
+      "volume": 1
+    },
+    {
+      "depth": 1,
+      "dimension": 2,
+      "fibre": 2,
+      "high_count": 1,
+      "key_symbols": 16,
+      "output_sha256": "cd0bae01d09803811b7a14b69461d4b28f8d6e0f0b779ac030adfe1cdc0dee6a",
+      "peak": 32,
+      "prefixes": 3,
+      "q": 3,
+      "volume": 6
+    },
+    {
+      "depth": 2,
+      "dimension": 1,
+      "fibre": 5,
+      "high_count": 3,
+      "key_symbols": 6,
+      "output_sha256": "81ea7c37a687bb9019f55d637dcdec36daf993e912dd794f4904ba3c3148be34",
+      "peak": 129,
+      "prefixes": 1,
+      "q": 3,
+      "volume": 15
+    },
+    {
+      "depth": 3,
+      "dimension": 1,
+      "fibre": 2,
+      "high_count": 9,
+      "key_symbols": 7,
+      "output_sha256": "da77e1503d5c44ad7dea69d72623f935ab1ee555c65ca37f8daa7c7f701bdc42",
+      "peak": 351,
+      "prefixes": 3,
+      "q": 3,
+      "volume": 54
+    },
+    {
+      "depth": 2,
+      "dimension": 1,
+      "fibre": 3,
+      "high_count": 5,
+      "key_symbols": 7,
+      "output_sha256": "678f17c55bd7d1cebc8ebc31d98086b327ea44dc0fe7bef9a965e95cb1ae33b7",
+      "peak": 210,
+      "prefixes": 2,
+      "q": 5,
+      "volume": 30
+    },
+    {
+      "depth": 2,
+      "dimension": 2,
+      "fibre": 1,
+      "high_count": 81,
+      "key_symbols": 24,
+      "output_sha256": "1b49ec19c3d85ef234dae5d2b72df5ada5bf86f1cdc5a9e56d592f035a56de84",
+      "peak": 6237,
+      "prefixes": 1,
+      "q": 3,
+      "volume": 81
+    },
+    {
+      "depth": 2,
+      "dimension": 2,
+      "fibre": 2,
+      "high_count": 81,
+      "key_symbols": 24,
+      "output_sha256": "da1f802b9e5512d1203ed31ea12c0f728707950b2942cea96f2a88a45fcfdf60",
+      "peak": 7290,
+      "prefixes": 3,
+      "q": 3,
+      "volume": 486
+    },
+    {
+      "depth": 2,
+      "dimension": 2,
+      "fibre": 1,
+      "high_count": 625,
+      "key_symbols": 28,
+      "output_sha256": "216a54a323d541e91219a06d495e3803a2157861120ed1c68393b92e9ef58654",
+      "peak": 55625,
+      "prefixes": 1,
+      "q": 5,
+      "volume": 625
+    }
+  ],
+  "controls": 17,
+  "scope": "Nonblank route payload/key symbols only; not total stock or host heap.",
+  "status": "component_certificate"
+}

research/selected-route-live-volume/SNAPSHOTS.json

@@ -0,0 +1,103 @@
+{
+  "repository": "https://github.com/CrocSwap/integer-mult-bounds",
+  "pr": 2697,
+  "commit": "a53fdf4bcbe33c6732f0bec1badc8c023380f9d1",
+  "files": [
+    {
+      "path": "vendor/directory.py",
+      "source_path": "research/selected-bit-node/vendor/directory.py",
+      "sha256": "4270e370b2bfe38ef73aadcd97d1b3496b56bd582115d74331eb9e5ceb90bec7",
+      "git_blob": "c74cacf5ce809c0561d374f137a52df0992b4226"
+    },
+    {
+      "path": "vendor/cardinality.py",
+      "source_path": "research/selected-bit-node/vendor/cardinality.py",
+      "sha256": "505d5e560c5a507e6184edcc19a87cf1fed243eb34a5cb21fbe1e4fe017e7f22",
+      "git_blob": "b8ba857e32c5903408e1e61ff916300848b4a208"
+    },
+    {
+      "path": "vendor/counts.py",
+      "source_path": "research/selected-bit-node/vendor/counts.py",
+      "sha256": "00b476dbda0e8cc99886bf794439e1cb9e775f435f599a3557e99321fe084069",
+      "git_blob": "81b48940ce222290a40d4fb349ce827f4788469d"
+    },
+    {
+      "path": "vendor/low_codes.py",
+      "source_path": "research/selected-bit-node/vendor/low_codes.py",
+      "sha256": "f657e17f6088c840e3f7783e662257630f6d2c1e71c217721ffbca4d6ac93e87",
+      "git_blob": "737edfc4a10f4b7b3b97a7cef4b40864efd806e6"
+    },
+    {
+      "path": "vendor/records.py",
+      "source_path": "research/selected-bit-node/vendor/records.py",
+      "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372",
+      "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3"
+    },
+    {
+      "path": "vendor/routes.py",
+      "source_path": "research/selected-bit-node/vendor/routes.py",
+      "sha256": "ed7dc3679451696ab1dd841146b215c9515a3eec5e4ff3763f33c315f1696ada",
+      "git_blob": "35531201dc349a811dfabc6f1f6e64697d665194"
+    },
+    {
+      "path": "vendor/bitstream.py",
+      "source_path": "research/selected-bit-node/vendor/bitstream.py",
+      "sha256": "f78bac9641007dbd8824984edcac057274fe016ce78bd9cb512d0c0913274783",
+      "git_blob": "4d1fd4abb0f2aabe833e5cbc9efb51039739e7ca"
+    },
+    {
+      "path": "vendor/matrices.py",
+      "source_path": "research/selected-bit-node/vendor/matrices.py",
+      "sha256": "00b687434039b54529ee092e34f9435cfcd66e0816eb3bd2a6688c73f4e01459",
+      "git_blob": "5d497353efbb9eeaaf4facd96ab40ffb0f3aa20d"
+    },
+    {
+      "path": "vendor/oracle.py",
+      "source_path": "research/selected-bit-node/vendor/oracle.py",
+      "sha256": "7bd18089e32ce48085b5e3a75159f6a82cdb2649ec682c53db05e399d97aef67",
+      "git_blob": "244f131466698a3ace10b657242fe1f65c07fd1f"
+    },
+    {
+      "path": "vendor/selection.py",
+      "source_path": "research/selected-bit-node/vendor/selection.py",
+      "sha256": "bc8e371fb1fa0b41fb05ef0b34d0f4c317b2396f9833d91f44f95c2b54b4052b",
+      "git_blob": "2c28f1aaec104a75c4e6c170b3e6a60300ee6700"
+    },
+    {
+      "path": "vendor/stream.py",
+      "source_path": "research/selected-bit-node/vendor/stream.py",
+      "sha256": "c7dc7da5b00f27016982ada4c0416f8328568b00df16d97012f33d4b372d79b5",
+      "git_blob": "5e5a4bb0f98971447043e25d4dd6991bfc070389"
+    },
+    {
+      "path": "vendor/words.py",
+      "source_path": "research/selected-bit-node/vendor/words.py",
+      "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9",
+      "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50"
+    },
+    {
+      "path": "vendor/PROOF.md",
+      "source_path": "research/selected-bit-node/PROOF.md",
+      "sha256": "88754d57bae35a2089d9de221ff32ba802b7a56b810f96271f3ea36985edfb14",
+      "git_blob": "a4746d1786f41e45a36fdedf37966b80fbab3562"
+    },
+    {
+      "path": "vendor/NOTICE.md",
+      "source_path": "research/selected-bit-node/NOTICE.md",
+      "sha256": "c446b32b8a621844fb2fbe654810c8122035bdd43fed2132f1137d98cb6f9943",
+      "git_blob": "ef9f81510db86eaf2f0a7191d85e92a6db30ddc0"
+    },
+    {
+      "path": "vendor/driver.py",
+      "source_path": "research/selected-bit-node/driver.py",
+      "sha256": "ee9e42fe95ab28fdd5e927c2d46fd480305aaad610eb2ca7ae514a5d22d9f0ac",
+      "git_blob": "0bdee4c9e348259b470a636a98e7657770f97fae"
+    },
+    {
+      "path": "vendor/node.py",
+      "source_path": "research/selected-bit-node/node.py",
+      "sha256": "b88fc9ac0b22d939311ff4f7aff788e8c87a64fd5e866498e59bd27940ee3f28",
+      "git_blob": "13badda6f059da2132cbe325c071307e5191baa3"
+    }
+  ]
+}