Research: pool PR #2269's 76 private T74 cleanup buffers into a 48-field bank

research/t74-cleanup-buffer-pooling/INPUTS.json

@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "files": [
+    {
+      "path": "source/BORROW-WORD-43base.json.gz",
+      "source_path": "research/gmx-t74-borrow43/new/borrow/words/BORROW-WORD-43base.json.gz",
+      "source_commit": "b479fc5567bc09ab9185bffe89b62594f36d74e5",
+      "git_blob": "448dd795adba29392a90b34aa3f1b1b796c7e0bd",
+      "sha256": "9492a5537fb87d9ca98dffcd0230f7625b3789744fa94e2f18acf23d91d998b5"
+    },
+    {
+      "path": "source/BORROW-WORD-43extra.json.gz",
+      "source_path": "research/gmx-t74-borrow43/new/borrow/words/BORROW-WORD-43extra.json.gz",
+      "source_commit": "b479fc5567bc09ab9185bffe89b62594f36d74e5",
+      "git_blob": "2b51ba96256283bbc5578f99b694c50edd8a0e35",
+      "sha256": "87d51f5298101d5947f45c43ee02f0ec45d6acbddabb808d0d02db1eaf063734"
+    },
+    {
+      "path": "source/NOTICE",
+      "source_path": "research/gmx-t74-borrow43/NOTICE",
+      "source_commit": "b479fc5567bc09ab9185bffe89b62594f36d74e5",
+      "git_blob": "46411b80b277d7dcd653a6d1999eaf12975b1103",
+      "sha256": "a91b93a731f116ae55b3644c88232b4d996e58bb810e2559dec013f9788f5e4b"
+    },
+    {
+      "path": "source/NOTICE-PR2226.md",
+      "source_path": "research/gmx-t74-borrow43/new/code/borrow/NOTICE-PR2226.md",
+      "source_commit": "b479fc5567bc09ab9185bffe89b62594f36d74e5",
+      "git_blob": "05c74506185550dd47277d6d6aff8e1f4110c97d",
+      "sha256": "9bd600b2a7aa46da910548d619e362e0540772da5f271b74d8f58de5d153ee0e"
+    },
+    {
+      "path": "source/PR2226-NOTICE.md",
+      "source_path": "research/gmx-t74-borrow43/new/code/borrow/vendor/PR2226-NOTICE.md",
+      "source_commit": "b479fc5567bc09ab9185bffe89b62594f36d74e5",
+      "git_blob": "5ea70357a04d083dba066fbc5c809a5736d8edd6",
+      "sha256": "f1d45d886926915531e3a59968abf0a4c974d7038f869848e71bd3a21b834422"
+    }
+  ]
+}

research/t74-cleanup-buffer-pooling/README.md

@@ -0,0 +1,183 @@
+# A 48-field private pool for the borrowed T74 cleanup
+
+**The frozen PR2269 cleanup can use 48 private FULL-frame fields in place of
+76 dedicated buffers.** The forward orientation needs 44 slots in the certified
+interval schedule; the inverse-transpose orientation needs 48. A shared-capacity
+bank therefore saves **28 fields**. No scalar operation is added: 151 and 409
+proved zero operations, respectively, are omitted, and the remaining operations
+keep their original order. All 661 ordinary entry arrays are arbitrary.
+
+This is a finite allocation construction with a scoped proof, author-checked
+with an independently represented dense cross-check. It is not an admitted
+supplier, a new recursive profile, a new κ, or independent human review.
+
+## Exact source and result
+
+The claim is in [Discussion #2609](https://github.com/CrocSwap/integer-mult-bounds/discussions/2609).
+
+The two `BORROW-WORD-43base/extra.json.gz` files are byte-for-byte copies from
+Jeremy Kothe's [PR2269](https://github.com/CrocSwap/integer-mult-bounds/pull/2269),
+head `b479fc5567bc09ab9185bffe89b62594f36d74e5`. Their serialized cleanup lists
+are identical, although their enclosing words differ. We bind both files and
+check both orientations; this is one common cleanup stream, not four different
+constructions. [INPUTS.json](INPUTS.json) records original paths, commit, Git
+blob IDs and SHA256 hashes. Source notices are retained unchanged.
+
+[Sagar Thakrar's PR2315](https://github.com/CrocSwap/integer-mult-bounds/pull/2315),
+head `4a2f20ea339e30348448096ca789d0efe55df9bb`, reproduced the words and found
+that the 76 eagerly allocated buffers had not been charged. Later constructions
+charge dedicated banks. This package addresses the distinct storage-reuse
+question; it does not repair or endorse the rest of PR2269's record claim.
+
+| Per enclosing word | Forward | Inverse transpose |
+| --- | ---: | ---: |
+| Original private buffers | 76 | 76 |
+| Buffers ever formally nonzero | 76 | 58 |
+| Maximal nonzero intervals | 81 | 65 |
+| Optimal interval-pool slots | 44 | 48 |
+| First maximum, after cleanup event (one-based) | 82 | 2686 |
+| Zero ADDs omitted | 123 | 361 |
+| Zero SCALEs omitted | 28 | 48 |
+| WARP operations retained | 43 | 43 |
+| Original / retained total operations | 4500 / 4349 | 4500 / 4091 |
+
+[EXPECTED.json](EXPECTED.json) contains every nonzero interval, a **static
+per-logical-buffer** slot assignment over the hull of its intervals, the exact
+peak rows, the omitted event numbers, and the ordinary endpoint digest. The
+static hull coloring already attains the same peak as splitting lifetimes;
+no mid-lifetime copying, dynamic allocator, or value-dependent decision is
+required. `pooled_replay` in [verify.py](verify.py) executes that allocation.
+
+## Model and proof
+
+Let `A = Q[F_43]` be the group algebra of the free group on the 43 invertible
+warp symbols. Each of the 661 ordinary registers starts as a separate free
+module generator `x_r`; every private buffer starts at zero. A scalar gate
+adds a rational multiple of one row to another or scales one row. A warp
+left-multiplies every term by its symbol; only adjacent inverse symbols cancel.
+This is exact symbolic arithmetic, not numerical sampling. For the second
+orientation, ADDs reverse source/destination and negate their coefficient,
+SCALEs invert their coefficient, and symbol `j` denotes `K_j^(-T)`.
+Applying inverse transpose to each chronological gate preserves gate order.
+
+A reduced row is zero exactly when all its coefficients vanish. Trace each
+buffer's maximal nonzero intervals. A zero source makes an ADD the identity;
+a SCALE or WARP applied to a zero buffer is also the identity. Removing exactly
+these events is valid for arbitrary ordinary inputs and for **any** invertible
+substitution for the warp symbols. Both buffers and ordinary data are checked
+as part of the final boundary. No caller-specific reachable-state restriction
+is used: the proof checks all independent cleanup-entry arrays.
+
+For each logical buffer, take the hull from its first nonzero write through
+its last zero-return event. Color these inclusive integer intervals by the
+usual earliest-available-slot rule. Each assigned field is zero at allocation,
+contains the logical value while allocated, and is zero at release. An
+induction over events proves that renamed execution equals the original
+execution: skipped events are identities, and every retained source and target
+is allocated or ordinary. The verifier checks the zero boundary at each
+allocation/release and compares every ordinary endpoint coefficient. All pool
+fields return to zero.
+
+The 44 forward and 48 dual simultaneous-live intervals certify lower bounds
+for **interval allocation with distinct storage for overlapping lifetimes**;
+the displayed colorings attain them. This alone would not exclude equal-value
+coalescing. Indeed, at the first forward peak two pairs of buffers carry equal
+expressions, so we do not claim a forward minimum under that broader model.
+
+There is a stronger certificate for the **common 48-field bank**. At dual cut
+2686, all 48 private rows are distinct and nonzero, and every row is a plain
+rational linear form: all warp symbols have canceled. The receipt gives an
+explicit small input witness using SHA256-derived signed 16-bit integers
+(seed 0, maximum absolute input 32736). Its 48 outputs are distinct and nonzero;
+maximum absolute output is `707881/4`, and denominators divide 4. The witness
+therefore survives the actual invertible warp specialization. On this input,
+a field storing one literal buffer value cannot store another different
+buffer value at the same cut. Thus 48 is also a sharp common capacity for
+**direct literal storage**, even allowing equal-value coalescing, when ordinary
+registers and the declared event boundaries are retained.
+
+That lower bound does **not** allow encoding several values into a field,
+address packing, borrowing ordinary/cold storage, recomputation, spilling,
+changes to precision, or resynthesis/reordering of the cleanup. It is not an
+information-theoretic scratch lower bound for arbitrary circuits.
+
+## Cost and interface boundary
+
+All original cleanup gates carry the FULL frame; preserved cold helpers are
+never touched directly. The checker binds the private namespace to exactly
+`704 + cold_helper` and confirms that no earlier section touches those buffers.
+The new bank is used only in the same cleanup interval. Logical scalar work
+decreases by the zero operations above, and the retained warp count is unchanged.
+The construction adds no arithmetic, transport, copy, or recursive call.
+
+Under a convention that clears each physical private field once at allocation
+and once at release, the candidate uses 88 forward or 96 dual CLEARs instead of
+152, or 96 for a common 48-field bank. These are conditional invoice counts,
+not a checked native emitter patch. Static routing, array allocation, exact
+native phase bindings, precision/tape constants, full hosted admission, and
+integration with later 78-buffer words remain to be checked. A smaller private
+bank by itself does not establish any change in κ.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -I -B scripts/research_package.py --package research/t74-cleanup-buffer-pooling
+```
+
+Equivalent direct commands:
+
+```sh
+python3 -I -O -B research/t74-cleanup-buffer-pooling/verify.py
+python3 -I -B research/t74-cleanup-buffer-pooling/check_dense.py
+```
+
+Expected final markers are `PASS_T74_CLEANUP_BUFFER_POOLING` and
+`PASS_DENSE_POOL_ORACLE cases=8 columns_per_case=1322 primes=65537,1000003 noncommuting=PASS`.
+Replay is read-only. `verify.py --write FRESH_PATH` explicitly creates a fresh
+receipt and refuses to overwrite an existing path. Default replay recomputes
+and compares every stored certificate field, preserving JSON type distinctions.
+
+The primary has six semantic controls per word/orientation: overlapping
+allocation, release before zero, dirty pool entry, a wrong-sign closing ADD,
+a re-enabled unallocated zero read, and an inverse-warp sign change that alters
+the ordinary endpoint despite scratch cleanup. `check_dense.py` imports neither
+the primary nor predecessor code. It separately interprets literal gates using
+noncommuting determinant-one 2-by-2 matrices over each of two prime fields,
+checks all 1322 scalar basis inputs, every zero/nonzero lifetime, the peak-row
+certificate, the pooled boundary and scratch restoration. This finite-field
+cross-check supports implementation confidence; the group-algebra derivation
+and rational replay establish the exact identities.
+
+## Open next questions
+
+- **Native adoption on this pinned word.** Emit the static slot renaming and
+  skipped identities in the native cleanup, then price allocation and routing.
+  This would turn the logical pool into an admitted physical saving; the native
+  stream and whole-call accounting are the missing artifacts.
+- **Later borrowed words.** Apply the same independently derived lifetime test
+  to a named 78-buffer successor, checking its exact cleanup instead of carrying
+  forward the number 48. Changed kernels and source-partner lifetimes may change
+  the intervals and peak; no such transfer is established here.
+- **Forward equal-value coalescing.** At forward cut 82, `(1015,1202)` and
+  `(1031,1214)` coincide. Examine their next writes before trying a smaller
+  forward-only bank. Equal values at one cut do not authorize merging complete
+  lifetimes, and cannot defeat the dual 48-value witness in the direct-storage
+  model.
+
+Structured questions and the changed task scope are in [TASK.json](TASK.json).
+
+## Credit
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+
+Jeremy Kothe/PR2269 supplies the frozen T74 words. Sagar Thakrar/PR2315 supplies
+the independent accounting finding. Cinna Davis (@1337isnot1337)/PR2226 supplies
+the anticipatory dirty-borrowing mechanism, early restoration and private-zero
+cleanup. Dugongue/PR2309 supplies dedicated private-stock accounting in the
+successor line. Rohan Arun, Marius-Paul Dumitrean, icekylinx and the retained
+T74/provider/compiler lineage keep the attribution in `source/` notices.
+No predecessor code is imported, executed or copied into the new checkers.
+The copied words and notices retain their original Apache-2.0 context.
+No independent human review or hosted-CI success is claimed.

research/t74-cleanup-buffer-pooling/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    }
+  ]
+}

research/t74-cleanup-buffer-pooling/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 4,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?",
+    "starting_points": [
+      "research/complex-local-word-ceiling/README.md",
+      "research/heterogeneous-owner-assembly/README.md",
+      "certificates/selected-result.json",
+      "research/selected-k8-unrestricted-ends/README.md"
+    ],
+    "methods": [
+      "Propose a changed helper inventory and derive an optimistic exact moment.",
+      "Design a small completed instance and independently verify its endpoint and rank bill."
+    ],
+    "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.",
+    "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.",
+    "allowed_variations": [
+      "Narrow to one changed boundary or helper type with explicit counts.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Mixing only providers already inside the pinned catalogue.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013."
+    ],
+    "overlap_terms": [
+      "helper inventory",
+      "heterogeneous-owner",
+      "mutable leaver"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact zero-to-zero private-buffer allocation for the two frozen PR2269 cleanup words, with a 48-field common pool and scoped direct-storage lower bound.",
+  "scope_change_reason": "Take the central private-buffer accounting question identified by PR2315. This finite storage construction does not claim the catalogue construction/ceiling acceptance gate.",
+  "bottleneck_link": "Dirty borrowing introduces private FULL-frame cleanup fields. Safe interval reuse reduces the physical bank without altering the paid recursive profile; native integration remains open.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the two pinned cleanup words, both orientations, exact pooled boundary and lower-bound witness, with source and semantic controls. No record search or global admission.",
+  "outcome": "completed",
+  "evidence": "EXPECTED.json: 44 forward / 48 dual slots; all 661 ordinary entry columns; six controls in each of four bound cases. check_dense.py independently checks 1322 scalar columns in each of eight cases.",
+  "author": "commdata2338",
+  "ai_assistance": "OpenAI Codex (GPT-6 Astra) derived, implemented, checked and wrote the contribution; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Can the 48-field pool be emitted and admitted natively on these pinned words?",
+      "why_it_matters": "Turns a logical scratch reduction into a checked physical invoice.",
+      "first_step": "Translate the static slot map and zero-event omissions into the native cleanup and verify allocation, routing and exact boundary.",
+      "blocked_by": "No native emitter patch or whole-call accounting replay is supplied."
+    },
+    {
+      "question": "What pool is valid for a named later 78-buffer successor?",
+      "why_it_matters": "New source partners and kernels may change the actual private-storage peak.",
+      "first_step": "Pin that successor and recompute its complete cleanup lifetimes before making a capacity claim.",
+      "blocked_by": "Later cleanup words are outside this certificate."
+    },
+    {
+      "question": "Can forward-only equal-value coalescing improve on its 44-slot interval schedule?",
+      "why_it_matters": "Two pairs agree at the first peak, but later writes may split them.",
+      "first_step": "Trace the next writes of pairs (1015,1202) and (1031,1214) with a charged split rule.",
+      "blocked_by": "Equal-value lifetime coalescing and modified circuits are not certified; the dual common-bank floor remains 48."
+    }
+  ],
+  "scope_key": "f3b0895a4f9f1cc62e75/PR2269-private-zero-pool",
+  "predecessors": [
+    {
+      "pr": 2269,
+      "head": "b479fc5567bc09ab9185bffe89b62594f36d74e5"
+    },
+    {
+      "pr": 2315,
+      "head": "4a2f20ea339e30348448096ca789d0efe55df9bb"
+    }
+  ],
+  "result_kind": "finite construction and scoped proof",
+  "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2609",
+  "refresh_checkpoint": {
+    "main_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+    "priority_revision": 4,
+    "checked_utc": "2026-10-15T16:24:54.125659+00:00",
+    "decision": "Main and contribution guidance unchanged. Retain PR2269 as the intentional frozen scientific input; no transfer to later cleanup words or selected frontier is claimed."
+  }
+}

research/t74-cleanup-buffer-pooling/VERIFY.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact source-bound free-group-algebra lifetime, pooled endpoint, scoped minimum witness, stored receipt and six semantic controls per case."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/check_dense.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Code-disjoint noncommuting dense finite-field all-column cross-check of lifetimes, peak rows and pooled endpoints."
+    }
+  ]
+}