Certify a 624-cell two-round stock for the ell=2 typed-H witness

research/two-round-cube-stock/PROOF.md

@@ -0,0 +1,80 @@
+# Two-round stock for the typed actual-width return
+
+This note shows that one fixed tape collection carries two rounds of the
+typed actual-width physical `H` on the ell=2 layouts already checked by
+`research/typed-actual-width-physical-h`. It does not retain both outputs,
+attach the PR #3617 diagonal, or change a multiplication exponent.
+
+## Inventory
+
+Fix precision `p >= 1`, record count `M`, coefficient count `r = 2^ell`,
+packet width `w = p + 2` and work width `W = p + g + 2` for a round that
+selects `g` address bits. One round of the predecessor, while its butterfly
+is in progress, holds seven tapes:
+
+| Buffer | Cells |
+|---|---:|
+| source, root, consumer | `M r 2 w` each |
+| scratch, paired | `M r 2 W` each |
+| low, high | `(M/2) r 2 W` each |
+
+The total is
+
+```text
+F = 3(M r 2 w) + 2(M r 2 W) + 2((M/2) r 2 W) = 6 M r (w + W).
+```
+
+Those seven lengths are exactly the allocation order inside
+`TypedActualWidthH.run` and `_butterfly` when `g` is the work width used to
+size the inventory. A second retained copy of the same seven tapes would hold
+`2F` cells.
+
+## Schedule
+
+The schedule constructs those seven tapes once. Each round creates a fresh
+`TypedActualWidthH` object and runs the unchanged `run` method, with the
+module's `Tape` constructor redirected onto the inventory in the order
+above. The redirect refuses an eighth tape and refuses a length other than
+the inventory length. Between rounds, `_blank_tape` clears root and consumer
+and returns their heads to cell 0. That is the previous-output reset: the
+next round's output occupies the same cells. Scratch and the three
+auxiliaries are already blank at the end of `run`. Counters are zeroed after
+the reset is recorded, so each round's read, write, move and gate ledger is
+comparable to a fresh one-shot call.
+
+For a tape of length `n` whose head is already at cell 0, `_blank_tape`
+writes `n` zeros and moves `2(n - 1)` cells: one step forward across the
+tape and a return to cell 0. Root and consumer each have length
+`n = M r 2 w`.
+
+## The ell=2 witness
+
+The predecessor's two-record witness is `ell = 2`, `flags = (False,)`,
+`k = 1`, `p = 4`. It has one layout height, `h = 0`, with selected bit
+`(0,)`, so `g = 1`, `M = 2`, `r = 4`, `w = 6` and `W = 7`. Then
+`F = 6 · 2 · 4 · (6 + 7) = 624`. The two schedule rounds are two admissible
+presentations of that same height. Each presentation's tensor and ledger
+equal a fresh one-shot call. The common ledger is 768 reads, 1200 writes,
+3890 moves and 620 gates, the same closed bill as the one-round package.
+Each output tape's reset is 96 writes and 190 moves. The first consumer
+image is not blank, and it is blank after the reset, before the second
+presentation. A second `run` on one predecessor object still raises
+`one-shot physical H`.
+
+## Two heights at ell=2
+
+`flags = (True,)` is the next ell=2 row in the same cube list. Its heights
+are `h = 1` then `h = 0`, with selected bits `(1,)` and `(0,)`. Both have
+`g = 1`, and `M = 4`, so `F = 1248 = 2 · 624`. The same redirect carries
+both heights of one cube. The two tensors differ, and each matches its own
+one-shot call. This is still one footprint, not two.
+
+## What is not claimed
+
+The redirect asks for the exact length of each buffer. A later round whose
+`g` is smaller or larger than the inventory's `g` is rejected rather than
+packed into a wider scratch. `ell = 3`, `flags = (True, False)`, `k = 1`
+has a height of `g = 1` followed by heights of `g = 2`, so it is outside
+this certificate. Both outputs are not live together. No diagonal factor,
+descriptor update, production-width cube, selected cold replay, or change
+to κ is included. The five selected framework assumptions remain.

research/two-round-cube-stock/README.md

@@ -0,0 +1,84 @@
+# Two-round cube stock for the typed actual-width H
+
+**Scoped tape-stock certificate. No new κ.**
+
+One fixed collection of seven tapes carries two rounds of the typed
+actual-width physical `H` on the ell=2 layouts from
+`research/typed-actual-width-physical-h`. Previous-output reset blanks the
+root and consumer tapes between rounds. The live cell count stays one
+round's footprint, `F = 6Mr(w+W)`, which is half of two retained one-shot
+inventories.
+
+## Result
+
+The predecessor's two-record witness is `ell = 2`, one short axis
+`flags = (False,)`, `k = 1` and `p = 4`. It has a single layout height, so
+the two-round schedule is two admissible presentations of height `h = 0`.
+The shared inventory has 624 cells. Each presentation matches a fresh
+one-shot tensor and the one-round bill of 768 reads, 1200 writes, 3890 moves
+and 620 gates. Each reset of an output tape writes 96 bits and moves 190
+cells. The first consumer image is nonempty and is blank after the reset.
+The predecessor object still rejects a second `run` with `one-shot physical H`.
+
+The same contract on `flags = (True,)`, the smallest ell=2 layout with two
+heights, carries `h = 1` and then `h = 0` in 1248 cells. The selected bits
+are `(1,)` and `(0,)`. The tensors differ and each matches its one-shot call.
+
+[PROOF.md](PROOF.md) derives `F` and the reset bill. The checker compares
+both schedules with the unmodified `physical_h.py` machine.
+
+## Scope
+
+This is the first open question of `research/typed-actual-width-physical-h`,
+left by discussion #1166 comment 19016699 after the one-round return was
+supplied. It is not a proof of any of the five selected framework
+assumptions, not a PR #3617 diagonal join, and not a production-width cube.
+Rounds whose selected-bit counts differ do not fit this exact-length
+inventory. Both outputs are not retained at once. Selected κ stays
+`781451/250000000`.
+
+## Reproduce
+
+Python 3.12, standard library, from the repository root:
+
+```sh
+python3 -B research/two-round-cube-stock/verify.py
+python3 -B -O research/two-round-cube-stock/verify.py
+python3 -B scripts/research_package.py --package research/two-round-cube-stock --check-only
+python3 -B scripts/research_package.py --package research/two-round-cube-stock
+```
+
+Both direct runs print `PASS_TWO_ROUND_CUBE_STOCK`. On this host each took
+well under a second. The selected-record binding check
+`python3 -B scripts/research_selected_baseline.py` printed
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` and was not a scientific replay.
+
+Not run: `make frontier6030-verify`, Lean, Docker, a production `ell`, and
+the PR #3617 diagonal.
+
+## Open next questions
+
+1. Can one inventory carry a layout whose rounds have different `g`? The
+   ell=3 row `flags = (True, False)`, `k = 1` selects one bit and then two.
+   A wider scratch would have to accept the shorter round's exact allocation,
+   which this redirect rejects. First step: pad or window the `g = 2` tapes
+   so the `g = 1` round is a prefix, and check both tensors.
+2. What stock is required when the caller keeps both round outputs? Reset
+   is what keeps `F` from becoming `2F`. First step: add a second
+   root/consumer pair and price the retained pair against `F`.
+3. Can the reset output sit under PR #3617's framed diagonal without a new
+   stage object per round? That is still the predecessor's second question.
+   First step: feed one rounded packet into the unchanged diagonal consumer
+   and price the framing.
+
+## Credit
+
+The matched layout, one-round machine, tensor and toward-zero return are
+Clear1nsight's PR #3623, incorporating Sagar Thakrar's PR #3617 diagonal
+contract and the PR #3493 / #3593 / #3599 / #3611 sources credited there.
+The one-round tape bill is unpaidmoon's `research/typed-actual-width-physical-h`.
+The handoff is discussion #1166 comment 19016699. The two-round inventory,
+reset bill and checks are new.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. No
+independent human or formal-kernel acceptance is claimed. Apache-2.0.

research/two-round-cube-stock/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "626e936ce4d61f2584316914fc71baf96940c512",
+  "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"
+    }
+  ]
+}

research/two-round-cube-stock/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "626e936ce4d61f2584316914fc71baf96940c512",
+  "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": "Show that one seven-tape inventory carries two rounds of the typed actual-width physical H on the ell=2 witness, with previous-output reset and simultaneous stock F = 6Mr(w+W).",
+  "scope_change_reason": "The revision-8 card asks for one of the five selected assumptions at its caller. Discussion 1166 comment 19016699 is the first structured open handoff, and its typed actual-width return is already on main. This package takes that handoff's remaining stock question, which is open question 1 of research/typed-actual-width-physical-h, instead of a new all-size assumption proof.",
+  "bottleneck_link": "The one-round bill cannot be reused across rounds while auxiliary tapes are allocated per call. A fixed footprint F, rather than 2F, is the stock term a later caller would pay for two rounds of this return. It does not move the selected main_transform outer row.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the ell=2 short-axis two-presentation schedule and the ell=2 long-axis two-height schedule. Do not build a variable-g inventory, retain both outputs, attach the PR 3617 diagonal, or run the selected cold replay.",
+  "outcome": "partial",
+  "evidence": "PROOF.md derives F = 6Mr(w+W) and the blank bill n writes and 2(n-1) moves. verify.py matches fresh one-shot tensors and ledgers, checks 624 and 1248 live cells, the reset bill, the predecessor one-shot rejection and the unit-disk rejection.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial assistance from Cursor Grok 4.7. No independent human or formal-kernel acceptance is claimed.",
+  "open_questions": [
+    {
+      "question": "Can one inventory carry rounds whose selected-bit counts differ?",
+      "why_it_matters": "ell=3 with flags (True, False) and k=1 has g=1 followed by g=2, so the exact-length redirect rejects the shorter round.",
+      "first_step": "Pad the g=2 scratch, low, high and paired tapes so the g=1 round uses a checked prefix, then compare both tensors with one-shot calls.",
+      "blocked_by": "This allocator requires each requested length to equal the inventory length."
+    },
+    {
+      "question": "What is the stock if the caller keeps both round outputs?",
+      "why_it_matters": "Previous-output reset is what keeps the live count at F instead of 2F.",
+      "first_step": "Add a second root and consumer pair and compare the retained-pair cell count with F.",
+      "blocked_by": "No second output pair is allocated here."
+    },
+    {
+      "question": "Can one reset output sit under PR 3617's framed diagonal without a fresh stage object?",
+      "why_it_matters": "That is the predecessor's second open question and would price the fixed-h join separately from this stock bound.",
+      "first_step": "Feed one rounded consumer packet into the unchanged diagonal consumer and price the framing.",
+      "blocked_by": "The diagonal pass is not invoked, and initial framing remains unpriced."
+    }
+  ]
+}

research/two-round-cube-stock/VERIFY.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/typed-actual-width-physical-h/physical_h.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Two presentations of the ell=2 short-axis witness and both heights of the ell=2 long-axis layout match fresh one-shot tensors and ledgers on one seven-tape inventory; reset bills, the 624- and 1248-cell footprints, the one-shot second-call rejection and the unit-disk rejection all hold."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same identities with assertions disabled, so the result does not depend on assert statements."
+    }
+  ]
+}