Construct one stock for changing-width physical-H rounds (no κ)

research/variable-g-cube-stock/PROOF.md

@@ -0,0 +1,136 @@
+# A fixed stock for changing selected-bit counts
+
+This is a scoped tape-model construction with exact finite evidence. It extends
+Open next question 1 of unpaidmoon's [PR6342](https://github.com/CrocSwap/integer-mult-bounds/pull/6342).
+The one-round program and arithmetic return in unpaidmoon's PR4127 are premises.
+Neither predecessor's scientific suite is replayed or audited here.
+
+## Contract
+
+Fix a matched layout, precision `p`, record count `M`, and coefficient count `r`.
+Each invocation uses the cited program's physical source order and a permitted
+height. Its selected-bit count `g` may change between invocations. Set
+
+```text
+w = p + 2
+g_max = maximum selected-bit count over the layout's permitted heights
+W_max = p + g_max + 2
+C = 2 M r w
+S = 2 M r W_max
+```
+
+The source packet is a new external presentation at each invocation, just as in
+the one-round API. It is borrowed unchanged during that invocation. The previous
+root and consumer packets may be discarded before the next presentation.
+No diagonal or output-to-input transition is supplied. Retained host snapshots
+in the verifier are observations, not additional tapes used by the construction.
+
+The construction allocates seven physical bit arrays once:
+
+| Tape | Capacity |
+|---|---:|
+| source | C |
+| scratch | S |
+| root | C |
+| consumer | C |
+| low | S/2 |
+| high | S/2 |
+| paired | S |
+
+Thus its simultaneous allocated tape stock is exactly
+
+`3C + 3S = 6 M r (w + W_max)`.
+
+This is an upper bound achieved by this allocation, not a minimum over different
+tape programs. Python objects, receipts, diagnostic scans and scalar control
+storage are outside this bit-tape model. A complete machine lowering would have
+to price its own control representation.
+
+## Prefix simulation
+
+In a round with count `g`, use `W_g = p + g + 2`. The source, root and consumer
+retain length `C`. The other four arrays expose only the same prefixes requested
+by the one-round program: `2Mr W_g` for scratch/paired and `Mr W_g` for low/high.
+Prefix indexing rejects positions beyond that logical length. No cell is moved
+when the logical length changes.
+
+Maintain these invariants at a round boundary:
+
+1. All seven physical heads are zero.
+2. Scratch, low, high and paired are blank across their entire physical capacity.
+3. Root and consumer contain only the most recent output, and source contains
+   the current or previous borrowed presentation.
+
+They hold initially. Before a later round, blank the two output tapes. Present
+the new borrowed source in its unchanged packet width. All active prefixes then
+have the same starting bits and heads as the one-round program. Every tape read,
+write and seek has the same address, value and charged distance. No instruction
+uses an inactive cell. The existing one-round return therefore yields the same
+output packets and charged operation ledger.
+
+The one-round program creates low, high and paired inside each selected-bit
+iteration, and blanks and homes all three before returning from that iteration.
+Consequently the same physical arrays can serve its next selected bit. Their
+diagnostic counters restart at each allocation request, as fresh objects' counters
+would, before the original program folds their charges into scratch. Restarting
+these counters changes no physical bit and removes no operation from the ledger.
+
+Each returned work prefix is blank, and its inactive suffix was blank and was
+never accessed. Thus the entire physical work array is blank. Heads return to
+zero, proving all boundary invariants and completing induction over any finite
+schedule in the stated contract. This simulation is the proof; the finite
+comparisons corroborate it rather than prove it for every layout.
+
+## Reset charge and first witness
+
+Blanking one length-`C` output at head zero writes `C` bits, reads none, and
+travels `2(C-1)` cells. Resetting root and consumer therefore adds exactly
+`2C` writes and `4(C-1)` moves between rounds. These charges are separate from
+each unchanged one-round ledger. Presentation and source preservation use the
+same convention as the cited one-round API.
+
+For `ell=3`, flags `(True, False)`, `k=1`, `p=4`, there are `M=32` records,
+`r=8` coefficients and selected counts one and two. Hence `w=6`, `W_max=8`,
+`C=3072`, `S=4096`, and the stock is **21,504 cells**. The exact first witness is:
+
+| Round | g | Reads | Writes | Moves | Gates |
+|---|---:|---:|---:|---:|---:|
+| h=2 | 1 | 24576 | 38400 | 125876 | 19776 |
+| h=1 | 2 | 48128 | 71680 | 239476 | 28288 |
+
+The intervening reset adds 6,144 writes and 12,284 moves. Both round outputs,
+their actual root/consumer bit packets, borrowed source and complete one-round
+ledgers match fresh calls. No κ or selected-frontier change follows.
+
+## Executable bounds and remaining obligations
+
+The executable accepts at most sixteen rounds, `2 <= ell <= 4`, one to three
+Boolean axis flags, `1 <= p <= 16`, valid `k < ell`, at most nine address bits,
+and at most `2^20` total tape cells. Its geometric count gives at most three
+selected bits. These bounds constrain all new schedule and prefix loops.
+
+Finite verification uses five schedules comprising fourteen rounds, including
+both directions of the width change, repeated width changes, two chunk widths,
+precision one and a one-to-three selected-bit change. Eleven rejection controls
+cover prefix bounds, inactive dirt, invalid allocation state, invalid schedule
+and layout, input bounds and restoration of the module binding after failure.
+
+The adapter temporarily replaces `Tape` only in its privately loaded engine
+module. Execution must be serial, and a `finally` block restores that binding.
+No global import or shared repository module is patched. Python still allocates
+control objects and verifier snapshots dynamically; only the seven bit arrays
+are fixed. Explicit source-byte compilation is limited to the two named modules,
+with the external engine checked against its SHA256 before execution. These are
+the scoped managed-runtime and dynamic-loading deviations from Power of Ten.
+All new functions are under sixty lines; invariants use checks that survive `-O`.
+
+General physical lowering, retained-output storage, the framed diagonal,
+production-size execution, the five selected framework assumptions and a
+complete multiplication theorem remain unresolved. No Lean or Docker replay
+or selected cold replay is included.
+
+This construction, proof and verifier were produced by Nick Petalas. Credit
+unpaidmoon for PR6342's stock question and scheduler and PR4127's one-round tape
+program; Chris R / Clear1nsight for PR3623's matched layout and tensor; Sagar
+Thakrar for PR3617's diagonal contract; and the PR3493, PR3593, PR3599 and PR3611
+lineage retained in the one-round source. Apache-2.0.

research/variable-g-cube-stock/README.md

@@ -0,0 +1,76 @@
+# One physical-H inventory across changing selected-bit counts
+
+One fixed seven-tape inventory now serves rounds with different selected-bit
+counts. This answers Open next question 1 of unpaidmoon's [PR6342](https://github.com/CrocSwap/integer-mult-bounds/pull/6342).
+The new adapter uses checked active prefixes and reuses the butterfly arrays
+after every selected bit. Its achieved stock is
+
+`F = 6 M r (p + 2 + p + g_max + 2)`.
+
+Claim type: scoped tape-model construction and written simulation proof, with
+an exact finite certificate. No new kappa or selected-frontier change is claimed.
+The predecessor arithmetic and one-round return are cited premises.
+
+For `ell=3`, flags `(True, False)`, `k=1`, `p=4`, the first two heights have
+`g=1` then `g=2`. They run on **21,504 cells**. Both complete one-round ledgers
+and actual output packets equal fresh calls. The previous output reset adds
+6,144 writes and 12,284 moves. [PROOF.md](PROOF.md) gives the induction, exact
+buffer list and first witness invoice.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/variable-g-cube-stock/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/variable-g-cube-stock/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/variable-g-cube-stock
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/variable-g-cube-stock --check-source-history
+```
+
+Any CPython 3.12 executable may replace this installation path. Direct execution
+prints `PASS_VARIABLE_G_CUBE_STOCK` followed by a generated receipt with computed
+results and package file hashes. No handwritten receipt is supplied.
+
+The verifier checks five schedules comprising fourteen rounds, including both
+width-change directions, repeated changes, two chunk widths and a one-to-three
+selected-bit change. It compares every output bit and the full charged ledger
+with a fresh invocation. Eleven rejection controls cover prefix and capacity
+bounds, inactive dirt, invalid allocation state, input bounds and restoration
+on failure. Normal and optimized commands are registered in VERIFY.json.
+
+## Scope and remaining obligations
+
+The stock counts seven physical bit arrays. Python control objects, diagnostic
+scans and verification snapshots are outside that bit-tape model. The executable
+bounds layouts and schedules as stated in PROOF.md. Its privately loaded engine
+module is used serially; its temporary Tape binding is restored on every exit.
+
+Each round receives an external source presentation. Only the latest physical
+root/consumer output remains live. This is not an inter-round diagonal or an
+output-to-input transfer, nor a minimum stock theorem. Production widths,
+physical control lowering, retained-output banks and the five framework
+assumptions remain open. No selected cold replay, Lean, Docker, supplier
+admission or complete multiplication theorem is supplied.
+
+## Open next questions
+
+- Compose the retained output, a fully charged framed diagonal and the next
+  round on this stock. Start with the same ell=3 witness and specify the packet
+  framing; initial framing and input transfer remain unpriced.
+- Specify explicit banks when a caller needs both round outputs simultaneously.
+  The current bound depends on resetting the previous root and consumer.
+
+TASK.json records the corresponding first steps and blockers. Optimization
+stopped at the first verified changing-width construction.
+
+## Credit and sources
+
+This construction, proof and verifier were produced by Nick Petalas.
+Credit unpaidmoon for PR6342's question and stock scheduler and PR4127's
+one-round physical tape program; Chris R / Clear1nsight for PR3623's matched
+layout and tensor; Sagar Thakrar for PR3617's diagonal contract; and the
+PR3493, PR3593, PR3599 and PR3611 lineage retained in the one-round source.
+SOURCES.json binds the canonical base and cited source files without changing
+their credit lines. Independent human and formal proof-kernel review are
+unclaimed. Apache-2.0.

research/variable-g-cube-stock/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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"
+    },
+    {
+      "path": "research/typed-actual-width-physical-h/physical_h.py",
+      "usage": "input",
+      "git_blob": "1ff92d44bf2545a158c984442a387cf4f5eaf29d",
+      "sha256": "f032251b60c3d3a4eca84bb6697f5cf032980089b891e1dc8248c297e99ecd2a"
+    },
+    {
+      "path": "research/two-round-cube-stock/README.md",
+      "usage": "provenance",
+      "git_blob": "032227826a399b0cb500a60bd4827a18942073f4",
+      "sha256": "fededf92a0bff07d10fbb7604c3f122ee3d7a220cb59e4e014daa83f7bbf45c6"
+    },
+    {
+      "path": "research/two-round-cube-stock/TASK.json",
+      "usage": "provenance",
+      "git_blob": "54fc0fac787ec811d10aa555e9b53b6420f9447a",
+      "sha256": "4517cdec54b76833a7765ca3ac10f975d576005674bbfecf7a60ef5c8f589958"
+    },
+    {
+      "path": "research/two-round-cube-stock/stock.py",
+      "usage": "provenance",
+      "git_blob": "5ee594ebb67a11be24b32fcafe28d06ef3dde22c",
+      "sha256": "36b21f916c507121fb35918e681194bd77bc49e310b2b82dccd6ce908bc47687"
+    },
+    {
+      "path": "research/typed-actual-width-physical-h/README.md",
+      "usage": "provenance",
+      "git_blob": "bb713d755be6d281db545930a96aae8ace10774a",
+      "sha256": "3494198a6f635b7cf87005f51d348719ae1bcd69f7f1700d151c357df1d8a5a4"
+    }
+  ]
+}

research/variable-g-cube-stock/TASK.json

@@ -0,0 +1,96 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Construct a fixed seven-tape stock for changing selected-bit counts in the typed actual-width physical H, using checked active prefixes and per-butterfly buffer reuse.",
+  "scope_change_reason": "Takes Open next question 1 of unpaidmoon PR6342. This is a scoped precision/tape interface construction, not a proof of the selected all-size assumption. The chosen card follows the concrete stock handoff rather than the randomly suggested BIT cards.",
+  "bottleneck_link": "A varying-width return needs a simultaneous stock before a complete caller can use it. This supplies that tape-model stock and reset charges; the framed diagonal and selected outer ledger remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified changing-g inventory. Do not retain both physical outputs, integrate a diagonal, optimize buffer count, or change the selected frontier.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the stock and prefix simulation induction. verify.py checks five schedules comprising fourteen rounds, every output packet and exact fresh-call ledger, eleven rejection controls, and generated file-hash receipts.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a caller feed the retained output through the framed diagonal into the next round on this same stock?",
+      "why_it_matters": "Independent input presentations do not implement the complete inter-round arithmetic path.",
+      "first_step": "Specify the diagonal packet framing and compose one ell=3 two-round path, charging input transfer and all head movement.",
+      "blocked_by": "The diagonal and its initial framing are not implemented here."
+    },
+    {
+      "question": "Can the same stock retain every requested round output?",
+      "why_it_matters": "The present bound depends on resetting the previous root and consumer.",
+      "first_step": "Add explicit output banks and account for their simultaneous lifetimes before changing the reset policy.",
+      "blocked_by": "Only one root/consumer pair is allocated."
+    }
+  ],
+  "question_source": {
+    "pr": 6342,
+    "author": "unpaidmoon",
+    "question": 1,
+    "head": "f744101c871914c767982484f06bf49cd5ef5d82"
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358894"
+}

research/variable-g-cube-stock/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/typed-actual-width-physical-h/physical_h.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Five changing-g schedules and fourteen fresh-call output/ledger comparisons; bounded prefix access, blank inactive tails, charged output resets, per-bit buffer reuse, exception restoration and eleven rejecting controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same finite evidence with assertions disabled; generated receipt binds all package file hashes."
+    }
+  ]
+}