Price one typed actual-width physical H and its toward-zero return

research/typed-actual-width-physical-h/PROOF.md

@@ -0,0 +1,121 @@
+# Typed actual-width H and toward-zero return
+
+This note prices one matched-layout normalized butterfly and its rounded
+return. It does not apply the diagonal, reuse tapes across rounds, or change
+a multiplication exponent.
+
+## Typed object
+
+Fix a layout parameter `K >= 1`, axis flags, length `ell >= 2`, and precision
+`p >= 1`. Let the original and physical named-slot orders be the two orders in
+PR #3623's `slots_for`. Write `M` for the number of records and `r = 2^ell`
+for the coefficients in each record. A round `h` in that layout's round list
+has selected address bits `beta_1, ..., beta_g` from the matched-extent rule:
+
+- on a common round, `g` equals the axis count and the bits are
+  `right + rho + t K`;
+- on a prefix round, the bits are exactly the physical slots of height `h`.
+
+The packet width is `w = p + 2`. The work width is `W = p + g + 2`. Every
+borrowed numerator is an integer in `[-2^p, 2^p]`, encoded as an MSB-first
+two's-complement word of width `w`. The call reads those words in either the
+original or the physical slot order and writes the rounded tensor in the
+physical order. The root copy is LSB-first. The consumer copy is MSB-first.
+Both copies, and the blanked work tape, finish with their heads at cell 0.
+The borrowed source bytes are unchanged. The object rejects a second call.
+
+An old descriptor is not coerced. On the three short axes with `ell = 3` and
+`K = 1`, round `h = 1` has selected bits `(3, 4, 5)`. The concealed bits
+`(0, 1, 2)` raise `selected-bit descriptor`.
+
+## Butterfly and rounding
+
+Sign-extend each admitted word into width `W`. For each selected bit `beta`,
+split the work image by that address bit, interleave the two halves so that
+partners are adjacent, replace each adjacent pair `(a, b)` by `(a+b, a-b)`,
+and merge the sum back onto the clear bit and the difference onto the set bit.
+Component additions and subtractions are ripple circuits on width `W`.
+Subtraction is invert-and-add-one. A final carry that leaves the signed
+`W`-bit range aborts; the bound below says a successful admitted call does
+not hit that abort.
+
+After `t` selected bits, every work numerator is a sum of `2^t` input
+numerators with coefficients in `{±1}`. Its absolute value is therefore at
+most `2^{p+t}`. At `t = g` this is at most `2^{p+g}`. Width `W = p+g+2`
+represents every integer from `-2^{p+g+1}` through `2^{p+g+1}-1`, so the
+whole work vector fits.
+
+`Q_p` then acts componentwise. Let `s` be the sign bit. Form the magnitude by
+xoring every bit with `s` and adding `s`, drop the `g` low bits by keeping the
+high `w` bits, then xor with `s` and add `s` again. For a nonnegative
+magnitude this wiring is division by `2^g` rounded down. Restoring the sign
+makes the result truncating division: nonnegative inputs use `floor(n/2^g)`,
+and negative inputs use `-floor(|n|/2^g)`. That is not an arithmetic right
+shift. In particular `-1` divided by `2` is `0` here and `-1` under an
+arithmetic shift. The same witness appears in the two-record call below:
+records `(0, 0)` and `(1, 0)` on the single selected bit become `(0, 0)` and
+`(0, 0)` after rounding, whereas an arithmetic shift of the difference `-1`
+would have left `-1`.
+
+The consumer word is that signed `w`-bit vector, MSB first. The root word is
+its reversal. Decoding the reversal as an MSB word changes the integer `1`.
+Reversing again recovers it. After rounding, every returned numerator still
+lies in `[-2^p, 2^p]`, which fits in a `w = p+2` two's-complement word
+because `2^p <= 2^{p+1}-1` and `-2^p >= -2^{p+1}`.
+
+The integer shadow of this schedule is exactly the unnormalized Hadamard on
+the selected bits, followed by truncating division by `2^g`. Hadamard factors
+on distinct bits commute, so the selected-bit order does not change the
+integer result. PR #3623's explicit tensor `h_direct`, followed by its
+toward-zero `truncate`, is the same map. The finite cubes compare those two
+executables; they are controls for the wiring, not the only inputs covered
+by the schedule.
+
+## Exact bill
+
+Write `C = 2 M r` for the number of real and imaginary components, and
+`L = C W` for the work-tape length. A successful call performs exactly
+
+```text
+reads  = C w + 5 g L + L
+writes = 2 L + 7 g L + 2 C w
+gates  = C (W - w) + C + 2 g M + (3/2) g C W + C (2 W + 2 w)
+```
+
+The summands are the layout read and sign-extended write, five sequential
+work-length passes per selected bit (split, interleave, adjacent butterfly,
+deinterleave, merge), the final `Q_p` read, the root and consumer writes, and
+the final work-tape blank. The two extra writes per selected bit blank the
+half tapes and the paired tape. Gates are one disk test and `W-w` sign-fanout
+gates per component, two address tests per record per selected bit, `3W`
+adder/inverter gates per butterfly component pair, and `2W+2w` magnitude and
+resign gates per component. Head travel is data-independent and equals the
+itinerary in `itinerary_moves`: every scan starts and ends at cell 0, and the
+adjacent butterfly is the only pass that seeks backward inside a pair.
+
+For two records of one bit each, that adjacent pair costs 4 moves: step from
+cell 0 to cell 1, return to cell 0, step to cell 1, and home. The whole
+linear level on that shape costs 14 moves, because each of the five length-2
+scans costs 2 and the adjacent pair costs 4, while every one-cell half tape
+costs 0. Both integers are checked.
+
+The two-record witness with `ell = 2`, one short axis, `K = 1`, `p = 4` and
+one selected bit has `M = 2`, `r = 4`, `g = 1`, `W = 7`, `w = 6`, `C = 16`
+and `L = 112`. The formulas give 768 reads, 1200 writes and 620 gates, and
+the executed ledger matches those three integers. Its head travel is the
+separate itinerary value 3890.
+
+## What this does not prove
+
+The diagonal factors `J_h` stay with PR #3617. This return is `Q_p H` in
+physical slot order, not `J Q_p H` and not `Q_p H J`. Auxiliary tapes are
+allocated per selected bit and blanked before the next bit; that is not a
+fixed all-round stock. The initial framing of a production cube, descriptor
+updates, previous-output reset, and a simultaneous buffer bound are still
+open. No call uses the production band `ell >= 45812984491`. No selected
+exponent changes.
+
+The checked `Q_p` range is every integer from `-2^{p+g}` through `2^{p+g}`
+for `p = 4` and `0 <= g <= 6`, which covers every selected-bit width in the
+cube suite. The wiring argument is not limited to those widths; the exhaustive
+loop is.

research/typed-actual-width-physical-h/README.md

@@ -0,0 +1,95 @@
+# Typed actual-width physical H
+
+**A one-round rounded return for the matched twiddle layout. No new κ.**
+
+PR #3623 proves a matched chunk width `K = floor((d-1)^(1/500))` and joins
+PR #3617's fixed diagonal to arithmetic-oracle butterflies. Its first open
+question is a typed physical `H` and toward-zero `Q_p` on that same array.
+This package supplies that call: MSB packet words in, physical-order rounded
+tensor out, with an exact read/write/gate bill and a data-independent head
+itinerary. It does not build the inter-round stock contract.
+
+## Result
+
+For each round of the ten small layouts used by PR #3623's cube checker, and
+for both original and physical source orders, the tape program equals PR
+#3623's explicit tensor followed by toward-zero division by `2^g`. The
+borrowed source is unchanged, scratch and per-bit auxiliary tapes are
+blanked, heads return to cell 0, and a second call is rejected. The old
+descriptor `(0, 1, 2)` is rejected on the matched round whose bits are
+`(3, 4, 5)`. A numerator `17` at `p = 4` is rejected before the butterfly.
+
+The bill depends only on the record count, coefficient count, selected-bit
+count and precision. On the two-record witness it is 768 reads, 1200 writes
+and 620 gates. Across the 50 calls the totals are 18,871,808 reads,
+27,630,304 writes, 94,213,460 moves and 9,636,792 gates. [PROOF.md](PROOF.md)
+derives the closed form. The cube comparisons are wiring controls for that
+schedule, not a production-width execution.
+
+Arithmetic right shift is a different return: `-1` shifted by one bit stays
+`-1`, while this `Q_p` returns `0`. Skipping the LSB-to-MSB bridge changes
+the integer `1`.
+
+## Evidence
+
+The frozen tensor is byte-identical to `check_join.py` at PR #3623 head
+`c5ab698bba8b35323e40ae3b132e78f26179d393` and at the handoff head
+`328c40966b650f60b1d62cfb0b1d67b2b755eb62` (git blob
+`421ae05f081ec37e4c5fa0b1b7e200a1578ab16d`). The current PR head only adds a
+workflow commit after that scientific file. `Q_p` was also checked on every
+integer in `[-2^{p+g}, 2^{p+g}]` for `p = 4` and `g = 0..6`.
+
+From the repository root, with Python 3.12 and the standard library:
+
+```sh
+python3 -B research/typed-actual-width-physical-h/verify.py
+python3 -B -O research/typed-actual-width-physical-h/verify.py
+python3 -B scripts/research_package.py --package research/typed-actual-width-physical-h --check-only
+python3 -B scripts/research_package.py --package research/typed-actual-width-physical-h
+```
+
+Both direct runs print `PASS_TYPED_ACTUAL_WIDTH_PHYSICAL_H` and match
+[RECEIPT.json](RECEIPT.json). On this host each direct run took about 10
+seconds. The registered launcher was also run, as recorded in the PR.
+
+Not run: the selected cold replay, Lean, Docker, a production `ell`, the
+PR #3617 diagonal, and any all-round tape reuse.
+
+## Open next questions
+
+1. Can one fixed collection of full-cube tapes carry every round, with
+   previous-output reset and a proved simultaneous-stock bound? The diagonal
+   pass is one-shot and this `H` allocates its auxiliary tapes per selected
+   bit. A useful first step is one two-round schedule on the `ell = 2`
+   witness with an explicit buffer list. The blocker is that no such shared
+   inventory is constructed here.
+2. Can this return be placed under PR #3617's framed diagonal on one complete
+   cube without a fresh stage object per round? That would discharge the
+   fixed-`h` join, not the inter-round stock question. The blocker is the
+   one-shot full pass and the still-unpriced initial framing.
+3. Does any of this change the retained outer movement bottleneck? No faster
+   exponent is claimed. Reopen that only with a paid movement change. The
+   blocker is the unchanged `169711/2000000000000` ordinary term.
+
+## Credit
+
+The matched layout, tensor and toward-zero truncation are Clear1nsight's PR
+#3623, incorporating Sagar Thakrar's PR #3617 diagonal contract and the
+PR #3493 / #3593 / #3599 / #3611 sources credited there. The handoff is
+discussion #1166 comment 19016699. New tape schedule, bill and checks by
+unpaidmoon, with substantial assistance from Grok 4.7 in Cursor. No
+independent human or formal-kernel acceptance is claimed. Apache-2.0.
+
+## Relation to the parallel arithmetic invoice
+
+While this package was being checked, the same account posted a different
+one-round answer to comment 19016699: discussion comment 19056745 and
+upstream PR #4123 (`research/typed-actual-width-h`, head
+`499427578245cbd3d2b07680945a94f6e927d020`). That invoice counts normalized
+`H0` add/sub operations, truncations and bit touches, and proves a Euclidean
+error below `sqrt(2) 2^{-p}`. This package does not repeat that count. It
+prices the unnormalized butterfly as a one-shot tape program: sequential
+split, interleave, adjacent butterfly, deinterleave and merge, then
+toward-zero division by `2^g`, with a closed read/write/gate form and a
+data-independent head itinerary. The two artifacts can be reviewed
+separately. Neither prices inter-round stock or the PR #3617 diagonal.

research/typed-actual-width-physical-h/RECEIPT.json

@@ -0,0 +1,41 @@
+{
+  "pass_token": "PASS_TYPED_ACTUAL_WIDTH_PHYSICAL_H",
+  "calls": 50,
+  "selected_bit_widths": [
+    1,
+    2,
+    3,
+    4
+  ],
+  "totals": {
+    "read": 18871808,
+    "write": 27630304,
+    "move": 94213460,
+    "gate": 9636792
+  },
+  "digest_sha256": "9de82d583fb882cdaa6f238d764ef8e6b72ff757aa856a4983ad9a889229d176",
+  "controls": {
+    "negative_output": [
+      [
+        0,
+        0
+      ],
+      [
+        0,
+        0
+      ]
+    ],
+    "negative_ledger": {
+      "read": 768,
+      "write": 1200,
+      "move": 3890,
+      "gate": 620
+    },
+    "arithmetic_shift_of_minus_one": -1,
+    "old_descriptor": "selected-bit descriptor",
+    "disk": "unit disk",
+    "adjacent_pair_moves": 4,
+    "linear_level_moves_m2_rw1": 14,
+    "q_range_failures": 0
+  }
+}

research/typed-actual-width-physical-h/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/typed-actual-width-physical-h/TASK.json

@@ -0,0 +1,72 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "docs/audit.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the selected review scope and choose one exact all-size or precision implication.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "Choose one tape, precision, hosting or restoration lemma."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Implement one typed actual-width physical H and toward-zero Q_p return on the PR3623 matched layout, and give its exact tape bill.",
+  "scope_change_reason": "The catalogue card asks for one quantified all-size, precision, hosting or restoration implication. This takes the released physical-H obligation from discussion 1166 comment 19016699, which is the first open question of PR 3623, rather than a new all-size compiler theorem. The schedule identity and closed bill are the implication; the finite cubes check the wiring.",
+  "bottleneck_link": "PR 3623 leaves H and Q_p unpriced, so the matched layer still cannot be charged as a caller. An exact one-round bill shows what that return costs and that an arithmetic shift or an old bit descriptor is a different return. It does not move the retained outer ordinary bottleneck.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after one round's typed return and its bill. Do not build inter-round stock, the diagonal, or a production-width root. Preserve the selected frontier.",
+  "outcome": "partial",
+  "evidence": "PROOF.md derives the work-width bound, the toward-zero wiring, and the read/write/gate formulas. verify.py matches PR3623 h_direct plus truncate on 50 calls, rejects the old descriptor, the out-of-disk numerator and a second call, and checks Q_p on the full p=4, g<=6 magnitude range. RECEIPT.json records the totals.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial assistance from Grok 4.7 in Cursor. No independent human or formal-kernel acceptance is claimed.",
+  "open_questions": [
+    {
+      "question": "Can one fixed collection of full-cube tapes carry every round of this H, with previous-output reset and a simultaneous-stock bound?",
+      "why_it_matters": "Per-bit auxiliary tapes and a one-shot diagonal do not give the all-round Q term in PR 3623.",
+      "first_step": "Write a two-round schedule on the ell=2 witness and list every live buffer.",
+      "blocked_by": "No shared inventory is constructed in this package."
+    },
+    {
+      "question": "Can this MSB return sit under PR 3617's framed diagonal on one cube without a fresh stage object per round?",
+      "why_it_matters": "That would discharge the fixed-h semantic join while leaving inter-round stock open.",
+      "first_step": "Feed one rounded packet from this return into the unchanged diagonal consumer and price the framing.",
+      "blocked_by": "The published full pass is one-shot, and initial framing is still unpriced."
+    },
+    {
+      "question": "Can a paid movement change improve the retained outer ordinary bottleneck while keeping this return?",
+      "why_it_matters": "The matched K and this local H bill do not change the narrower 169711/2000000000000 movement term.",
+      "first_step": "Price a different movement or consumer with the same endpoints and the full transfer invoice.",
+      "blocked_by": "No improved outer movement construction is claimed here."
+    }
+  ]
+}

research/typed-actual-width-physical-h/VERIFY.json

@@ -0,0 +1,28 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Fifty matched-layout calls equal the frozen tensor and the closed bill; old descriptor, disk, one-shot, bridge and toward-zero controls reject or disagree as stated."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same identity and failure controls with assertions disabled, so the result does not depend on assert statements."
+    }
+  ]
+}