Add a typed one-round actual-width H and rounded return.

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

@@ -0,0 +1,136 @@
+# Typed actual-width H and one rounded return
+
+This is a finite, exact interface lemma for the first open question in
+[discussion 1166, comment 19016699](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19016699).
+It does not prove the multi-round stock bound, execute a production-size cube,
+or change the selected exponent.
+
+## Statement
+
+Let `p >= 1` and `g >= 1`. A Gaussian numerator is a pair of integers `(re, im)`
+in the closed unit disk, meaning `re^2 + im^2 <= 2^{2p}`. The represented value
+is that pair divided by `2^p`. On a block of `N = 2^m` such gaussians, `m >= g`,
+fix `g` distinct address bits. Write `H0 = [[1, 1], [1, -1]] / 2`, and let
+`H` be `H0` tensored on those bits and the identity on every other coordinate.
+
+Evaluate `H` exactly, then apply one truncation `Q_p` toward zero onto the
+`p`-grid. Store the input and the returned words as two's-complement integers
+of width `w = p + 2`, least-significant bit first. Bridge each returned
+component to a most-significant-bit-first scan of the same width.
+
+Then:
+
+1. The exact numerator, in units of `2^{-(p+g)}`, is an integer of absolute
+   value at most `2^{p+g}`. Signed width `p + g + 2` holds every such
+   numerator, and width `p + g + 1` does not: the constant input `2^p` attains
+   `2^{p+g}` on the aligned character.
+2. `Q_p` returns integers in `[-2^p, 2^p]`, still on the disk, in width `w`.
+   Each real or imaginary component is wrong by strictly less than `2^{-p}`,
+   so the Euclidean error is strictly less than `sqrt(2) 2^{-p}`.
+3. `Q_p` commutes with a signed permutation of the coefficients. Truncation by
+   floor division does not, because `(-1) // 2 = -1` while toward-zero sends
+   `-1` at denominator `2` to `0`.
+4. The bit bridge preserves each integer. Reading the least-significant-bit-first
+   encoding as if it were most-significant-bit-first changes any
+   non-palindromic word.
+5. One call, with no layout permutation, performs `2 g N` real additions or
+   subtractions, `2 N` truncations, and `6 N (p + 2)` bit reads together with
+   the same number of bit writes. Two word tapes are rewound to their first
+   bit. A record permutation, when used, adds four word transfers per Gaussian
+   (read and write of both components).
+
+The old outer constructor admits a root only when
+`plan.dimension_exponent == (1, 40)`. The frozen active-width planner computes
+`K = floor(selected^{1/500})` and does not assign `dimension_exponent`. The
+typed plan check uses the matched floor and the cardinality
+
+```text
+gaussians = outer_rows * 2^{left + selected * K + right} * coefficients
+```
+
+instead of that guard.
+
+## Why the width and the error are exact
+
+The unnormalized Walsh sum on `g` bits is `sum_x chi(x, y) A_x`. Each `|A_x|`
+is at most `2^p`, and there are `2^g` characters, so the sum is at most
+`2^{p+g}`. Equality holds for the constant input `A_x = 2^p` at the trivial
+character. A signed word of width `t` represents `[-2^{t-1}, 2^{t-1} - 1]`.
+Width `p + g + 1` stops at `2^{p+g} - 1`. Width `p + g + 2` reaches
+`2^{p+g+1} - 1`, which contains both `2^{p+g}` and `-2^{p+g}`.
+
+Dividing by `2^g` toward zero leaves a remainder of absolute value at most
+`2^g - 1` in units of `2^{-(p+g)}`. That is strictly less than one `p`-grid
+step. The same bound on both components gives Euclidean error strictly less
+than `sqrt(2) 2^{-p}`. Toward-zero moves each component toward the origin, and
+`H0` has `L1` row norm one, so a disk input returns a disk output. This is the
+same endpoint shape as Jose Manuel's normalized `H0` statement; the new content
+is the typed width, the single truncation, and the bit-scan invoice.
+
+## Matched bits, not another arithmetic oracle
+
+Nick Petalas's frozen `OuterLayer.__init__` requires
+`dimension_exponent == (1, 40)`. Jose Manuel's frozen `ActiveWidthPlan.compute`
+sets `d` from the selected count and `K` from `floor_power(d, 1, 500)`. Those
+two source texts do not join: the planner never writes the exponent the
+constructor demands.
+
+On every common round of the ten small layouts below, the matched root bits
+
+```text
+right + rho + t K,  0 <= t < g,
+rho = (h - b) mod K,  b = (ell - 1) mod K
+```
+
+are exactly the bits of height `h` in the `K`-layout. For three short axes,
+`ell = 3` and `K = 1`, height `0` occupies bits `{0, 1, 2}`. The same names in
+the pre-layout order occupy `{0, 2, 4}`.
+
+The degree-`2` calibration `d = 4`, `g = 3` has `floor(d^{1/2}) = 2` and
+`floor((d - 1)^{1/2}) = 1`. It is a stand-in for the production identity
+`floor(k^{500}^{1/500}) = k` and `floor((k^{500} - 1)^{1/500}) = k - 1`, not a
+legal outer cube. On 32 addresses with the single nonzero numerator `(8, 0)` at
+address `0` and `p = 3`:
+
+- bits `{0, 1, 2}` return `(1, 0)` at address `2`;
+- bits `{0, 2, 4}` return `(0, 0)` there.
+
+The matched layout of the 64-address three-short cube fixes this origin
+impulse, and the height-`0` root bits are `{0, 1, 2}`, so the same return
+survives that permutation. The layout is nevertheless nontrivial: a
+nonconstant disk pattern is moved, at `256` word transfers.
+
+For `k = 2` and `k = 3` the production floors and both `p`-thresholds are
+checked as exact integers, including the caller's multiples of six. At `k = 2`
+those admitted precisions are `2^{20000} + 2` and `(2^{500} + 1)^{40} + 5`.
+The address-extent ratio between `K = k` and `K = k - 1` is `2^{k^{500} - 1}`.
+No tape of that size is allocated. A feasible plan with selected width `3`,
+`K = 1`, left `2`, right `1` and four coefficients has `256` gaussians. The
+typed check admits it. The `(1, 40)` guard rejects it, and `K = 2` fails the
+matched floor.
+
+## Invoice boundary
+
+The counts above are one typed round. They do not include descriptor updates,
+previous-output reset, borrowed restoration, private erasure, or a fixed
+cube buffer carried across rounds. Clear1nsight's sufficient multi-round
+allowance `Q <= C M R (r w + A + p^3) + poly(p)` is still a criterion, not a
+supplied contract. This package stops at that point.
+
+The ten layouts are the geometries already used by the matched-layer checker:
+`(ell, long flags, K)` equal to `(2, (F,), 1)`, `(2, (T,), 1)`,
+`(3, (F, F), 1)`, `(3, (T, F), 1)`, `(3, (T, T), 1)`, `(3, (F, F, F), 1)`,
+`(3, (T, F, T), 1)`, `(3, (F, F, F, F), 2)`, `(3, (T, F, F, F), 2)`, and
+`(4, (T, F), 2)`. Eighteen common-round bit identities are checked there.
+
+The `g = 1`, `p = 3` disk is exhaustive: `197` numerators and `38,809` ordered
+pairs, each compared with the explicit two-point matrix. The constant and
+negative-constant inputs check the sharp numerator. A separate `g = 3`, `p = 4`
+constant block checks the same bound one tensor higher.
+
+## What was not run
+
+No production T74 root, no PR3617 diagonal, no all-round lifecycle, no selected
+cold replay, and no execution at `ell >= 45,812,984,491`. The frozen planner
+and outer constructor are hashed and read as text. They are not imported:
+their modules are not on this branch.

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

@@ -0,0 +1,96 @@
+# Typed actual-width H and one rounded return
+
+**Partial result, no new κ.** One typed round of the normalized transform
+`H0 = [[1, 1], [1, -1]] / 2` on the matched actual-width bits, followed by one
+toward-zero return `Q_p` and an MSB-first component bridge. The selected
+frontier is unchanged.
+
+This takes the first open question of the handoff in
+[discussion 1166, comment 19016699](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19016699),
+left by [PR #3623](https://github.com/CrocSwap/integer-mult-bounds/pull/3623).
+The multi-round tape allowance in that handoff is still unspecified, so this
+package does not start that construction.
+
+## Result
+
+For `p >= 1` and `g` selected bits, an exact `H0` tensor sends a `p`-grid unit
+disk to integer numerators in units of `2^{-(p+g)}`. Those numerators fit in
+signed width `p + g + 2` and do not fit in width `p + g + 1`. One truncation
+toward zero returns the `p`-grid disk in width `p + 2`, with Euclidean error
+strictly below `sqrt(2) 2^{-p}`. The truncation commutes with signed
+permutations; floor division does not. The bit bridge preserves values and is
+exactly the conversion from the LSB-first root word to an MSB-first scan.
+
+On the matched layout, common-round root bits are the physical slots of that
+height. The degree-2 witness (`d = 4`, so `K_d = 2` and `K_g = 1`) puts a
+numerator `(8, 0)` at address 0 and `p = 3`:
+
+| Selected bits | Address 2 after `Q_p` |
+|---|---|
+| matched `{0, 1, 2}` | `(1, 0)` |
+| old stride `{0, 2, 4}` | `(0, 0)` |
+
+The 32-address witness invoice is 192 real add/sub operations, 64
+truncations, and 960 bit reads plus 960 bit writes. Those bit counts include
+the input load, the MSB-first bridge, and the read of the returned tape.
+Temporary width is 8 and final width is 5. The `g = 1`, `p = 3` disk is exhaustive (197 points, 38,809
+pairs). Production floors at `k = 2, 3` are exact integers, including the
+six-multiple offsets `+2` and `+5` at `k = 2`. The extent ratio between the two
+chunk widths has base-2 logarithm `k^{500} - 1`; that cube is not allocated.
+
+The argument, the finite domain, and the claims that are not made are in
+[PROOF.md](PROOF.md).
+
+## Evidence
+
+Canonical main for this package is `bb4bccbf42844d2801487450727c2f63e10d1d0f`,
+priority revision 6. The predecessor proof was written against
+`20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The two frozen sources have the same
+git blobs at PR #3623 heads `328c40966b650f60b1d62cfb0b1d67b2b755eb62` and
+`c5ab698bba8b35323e40ae3b132e78f26179d393`.
+
+```sh
+python3.12 -I -B research/typed-actual-width-h/verify.py
+python3.12 -B scripts/research_package.py --package research/typed-actual-width-h
+```
+
+Both the normal command and the same command under `-O` print
+`PASS_TYPED_ACTUAL_WIDTH_H` and the same receipt. The local run below used
+CPython 3.12.3 and finished in about two seconds. It does not import the frozen
+modules.
+
+## Credit
+
+The `(1, 40)` outer guard is Nick Petalas's PR #3493, as vendored by
+Clear1nsight in PR #3623. The selected-width `K` law and the normalized `H0`
+endpoint are Jose Manuel's PR #3599 (`jmbarrancoml`), retaining Hiroki
+Kumazaki's factory work. The matched layout, the address-2 witness, and the
+decision to stop when the multi-round allowance is unspecified are
+Clear1nsight's PR #3623, incorporating Sagar Thakrar's PR #3617 diagonal as an
+unexecuted predecessor. The transform lineage retained there includes Douglas
+Colkitt, Philipp, and the authors named in that proof.
+
+New work is the typed width, the single toward-zero return, the MSB/LSB bit
+invoice, and the independent checker. unpaidmoon, with substantial AI
+assistance. No independent human review or formal-kernel proof is claimed.
+Apache-2.0. The frozen files keep their original notices.
+
+## Open next questions
+
+1. **Can one fixed cube and packet inventory carry every round?** The
+   sufficient bound `Q <= C M R (r w + A + p^3) + poly(p)` still does not name
+   descriptor updates, previous-output reset, borrowed restoration, or the
+   constant number of cube buffers. First step: write those operations for one
+   common round and one prefix round on the 64-address three-short cube, with
+   an explicit simultaneous tape count. Blocked by: that contract is not in
+   PR #3623 or in this package, and the handoff says to stop while it is
+   unspecified.
+2. **Does this one-round invoice plug into PR #3617 without a second producer
+   charge?** PR #3617 already pays a fixed-h diagonal. First step: add this
+   bridge's `6 N (p + 2)` bit scans once per record and show which of its 38
+   roles, if any, already move those bits. Blocked by: PR #3617 is unmerged,
+   and its full-array pass was not replayed here.
+3. **Is the `k = 2` extent gap visible to any executable outer instance?** The
+   ratio is `2^{2^{500} - 1}` and the source band forces
+   `ell >= 45,812,984,491`. First step: none that allocates the cube. A
+   symbolic tape-count identity would still not be a physical execution.

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

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    }
+  ],
+  "related_work": [
+    {
+      "pr": 3623,
+      "heads": [
+        "328c40966b650f60b1d62cfb0b1d67b2b755eb62",
+        "c5ab698bba8b35323e40ae3b132e78f26179d393"
+      ],
+      "usage": "Frozen outer guard and active-width planner copied into this package. Not ancestors of this branch, so they are hashed by verify.py rather than pinned with head:.",
+      "blobs": {
+        "research/twiddle-matched-layer/pr3493-outer_layer.py": "2fc3370ea7e1b32be27faa4ec726ad7732af6769",
+        "research/twiddle-matched-layer/pr3599-active_plan.py": "c3a01cd8c4f52cab478aefacad60f64f60f1453a"
+      }
+    }
+  ]
+}

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

@@ -0,0 +1,80 @@
+{
+  "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": "Typed actual-width H0 tensor, one toward-zero Q_p return, and an MSB-first bit bridge on the matched twiddle array, with an exact one-round invoice.",
+  "scope_change_reason": "Handoff 1166#19016699 asks for a typed actual-width physical H and rounded return on the matched array from PR3623. The catalogue card is a general all-size or precision implication. This session takes only that one-round construction. The multi-round allowance is unspecified, so the lifecycle is not started.",
+  "bottleneck_link": "The matched K repair does not move the retained outer movement bottleneck. Pricing this previously unpriced one-round H and Q_p removes an oracle from that interface without a new exponent.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the typed one-round width, return, bridge and invoice. Do not build multi-round stock or a production-size cube while the caller allowance remains an uninstantiated criterion.",
+  "outcome": "partial",
+  "evidence": "PROOF.md and verify.py. Exhaustive g=1, p=3 disk (197 points, 38809 pairs); degree-2 address-2 witness (1,0) versus (0,0); 18 common-round bit identities; exact k=2,3 floors including six-multiple offsets +2 and +5 at k=2. Normal and -O runs both print PASS_TYPED_ACTUAL_WIDTH_H.",
+  "author": "unpaidmoon, with substantial AI assistance",
+  "ai_assistance": "Substantial AI assistance in the proof, the checker, and the write-up. No independent human review or formal-kernel proof is claimed.",
+  "open_questions": [
+    {
+      "question": "Can one fixed cube and packet inventory carry every round under an explicit simultaneous tape count?",
+      "why_it_matters": "The one-round invoice does not discharge the handoff's all-round reuse obligation, and an unknown multi-round charge is not zero.",
+      "first_step": "Write descriptor update, previous-output reset, borrowed restoration and the cube-buffer count for one common round and one prefix round on the 64-address three-short cube.",
+      "blocked_by": "PR3623 states Q<=C M R(rw+A+p^3)+poly(p) only as a sufficient criterion. The operations themselves are not specified."
+    },
+    {
+      "question": "Does this one-round bit invoice plug into PR3617 without charging the producer a second time?",
+      "why_it_matters": "The diagonal pass already has a 38-role tariff. Adding 6N(p+2) bit scans blindly could double-count work the pass already pays.",
+      "first_step": "Identify which PR3617 roles already move component bits, then add only the missing bridge scans once per record.",
+      "blocked_by": "PR3617 is unmerged and its full-array pass was not replayed here."
+    },
+    {
+      "question": "Is the k=2 extent gap visible to any executable outer instance?",
+      "why_it_matters": "The address-extent ratio is 2^(2^500-1), so every feasible cube has K_g=K_d=1 and cannot exhibit the production mismatch.",
+      "first_step": "Keep the exact integer thresholds already checked. Do not allocate the cube.",
+      "blocked_by": "The retained outer band forces ell>=45812984491, above the predecessor executable cap of 32."
+    }
+  ],
+  "handoff": {
+    "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19016699",
+    "predecessor_pr": 3623,
+    "predecessor_heads": [
+      "328c40966b650f60b1d62cfb0b1d67b2b755eb62",
+      "c5ab698bba8b35323e40ae3b132e78f26179d393"
+    ]
+  }
+}

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

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Typed width, exhaustive g=1 disk, matched-bit witness, production floors, bridge, and one-round invoice."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same checks with asserts disabled. Failures are raised explicitly, so the receipt must match the unoptimized run."
+    }
+  ]
+}