Join the one-target CRT hole mask with reverse-word repair keys

research/crt-joined-hole-repair/PROOF.md

@@ -0,0 +1,142 @@
+# Joined one-target hole mask, reverse-word keys, and repair
+
+This is one caller-bound step of Cinna Davis's PR #4100, `CRT.md` §4. It does
+not accept that construction and it does not change κ.
+
+The three pieces already audited apart are:
+
+- the one-target stencil and its scanner, ToikY's #4208 and #4201;
+- the reverse compact word, Hiroki KUMAZAKI's #4169;
+- the sparse-repair tariff, Ryanson Jonathan's #4328.
+
+#4328's first open question asks for those pieces to be run as one program,
+because each audit feeds the next a host-built table. The full Beneš evaluator
+priced in #4377 is a different procedure from these reverse shears. It removes
+a cost blocker for control generation. It does not by itself erase the mask or
+supply these keys.
+
+## Statement
+
+An integer geometry `(G, H, K, Y, J, B)` is admitted when
+
+```text
+G >= 1, H >= G, K >= G + 4, J >= 0, B >= 0, Y >= J + K.
+```
+
+The address length is `L = 2H + Y + B` and `M = 2^L`. Write an address
+`x ∈ {0, ..., M − 1}` as
+
+```text
+u = x >> (B + Y + H),   t = (x >> (B + Y)) mod 2^H,
+y = (x >> B) mod 2^Y,   back = x mod 2^B.
+```
+
+Let `f` be a function from `Y`-bit strings to one bit such that
+`f(y) = f(y xor 2^J)`. Let `S` be the compact macro of
+`check_batched_crt.compact` on `(u, t, y)`, with radix width `G`, control
+width `H`, target `J` and guard `K`, extended by leaving `back` fixed. Let
+`T` be the ideal switch that replaces `y` by `y xor f(y)·2^J` and leaves
+`u`, `t` and `back` fixed. Let `Holes` be the set of addresses that fail
+`check_batched_crt.good` on `(u, t, y)`.
+
+Run, on the fixed tape roles of the three predecessors:
+
+1. the unary producer on the six words of lengths `(G, H, K, Y, J, B)`;
+2. the three-tape scanner on that stencil;
+3. the repair whose hole bit at address `x` is the scanner mask, and whose
+   key at a hole is the #4169 reverse word on `(u, t, y)` followed by the
+   ideal map, packed with the same `back`.
+
+Then every payload that entered at `q` is written at `T(q)`. The producer's
+eight private tapes and the scanner counter are blank. The mask and the
+repair scratch are erased. The six geometry inputs are unchanged.
+
+## Stencil shape, for every admitted geometry
+
+The producer writes stencil cells from most significant address bit to least.
+Counting the cells it emits:
+
+| Block | Cells | Contents |
+| --- | ---: | --- |
+| High bits of `u` | `H − G` | skip |
+| Low bits of `u` | `G` | one digit interval |
+| High bits of `t` | `H − G` | skip |
+| Low bits of `t` | `G` | one digit interval |
+| `y` bits above the guard | `Y − J − K` | skip |
+| Guard above bit `J` | `K − 1` | one guard interval |
+| Bit `J` and the bits below it | `J + 1` | skip |
+| Spectator | `B` | skip |
+
+The guard block has length `(K − G − 3) + 1 + (G + 1) = K − 1`. Its threshold
+bits, most significant first, are the width-`(K − 1)` binary expansions of
+
+```text
+low  = 2^{G+1},    high = 2^{K−1} − 2^{G+1}.
+```
+
+Those are the constants in `good`: the low `G` bits of `u` and of `t` are not
+all ones, and the `K − 1` bits of `y` immediately above bit `J` lie in
+`[low, high)`. Skipped bits are not tested. The total is `2H + Y + B`.
+
+The scanner of #4201 implements those interval tests. This package does not
+reprove that flag machine. On every geometry below, the produced atoms equal
+this table and every mask bit equals membership of `Holes`.
+
+## Keys
+
+On a hole `x = (u, t, y, back)`, the key program reads only the mask bit. It
+executes the ten reverse shears of #4169 on `(u, t, y)` and then the ideal
+map, and packs `back` unchanged. It does not invert a stored table of `S`.
+
+#4169 shows that those shears invert the forward macro, and that `S` agrees
+with `T` on the good set whenever `f` omits bit `J`. Both facts are rechecked
+on every `(u, t, y)` of the geometries below. `T` preserves `Holes` because it
+changes only bit `J`, which is outside the tested digits and outside the guard.
+Therefore `S` preserves `Holes` as well: on the complement it equals `T`.
+
+## Repair
+
+After the macro, the record of origin `q` sits at `S(q)`. At a hole `x` the
+key is `T(S^{-1}(x))`. The map `T ∘ S^{-1}` sends `Holes` onto `Holes`, because
+both factors do. Sorting the hole records by this key and writing the record
+whose key equals the current hole address therefore places the record of `q`
+at `T(q)`:
+
+- the record of `q` is stored at `S(q)` and receives key `T(q)`;
+- the keys are exactly the hole addresses, so the sorted key stream is the
+  increasing enumeration of `Holes`;
+- the record written at address `T(q)` is the record of `q`.
+
+The same identity is why a key stream of `S^{-1}(x)` without `T` still passes
+the test "key equals current hole" and still misplaces the payload. The joined
+program keeps the ideal map. A mask with the hole bits flipped does not
+present that key permutation, and the address test rejects it.
+
+The repair's head schedule is the one priced in #4328: one mask-driven split,
+`L` stable two-bucket passes over the holes, one reinsertion, then erasure of
+the good stream, the hole stream and the mask. No key is computed on a good
+address. The cell bounds of that tariff therefore apply to this schedule with
+the same `M`, `L`, hole count and record width. They are checked on each
+fixture. They are not a new tariff.
+
+## What remains cited
+
+The universal shear inversion and the universal scanner-flag proof stay in
+#4169 and #4201. Outside the executed geometries, this note uses those
+theorems rather than repeating them. Many-target stencils, the last-`K`
+branch, and a bit-step price for these shears under the #4377 evaluator are
+outside the statement.
+
+## Executed geometries
+
+The verifier exhausts every address of
+
+```text
+(G, H, K, Y, J, B) =
+  (1, 1, 5, 5, 0, 0), (1, 1, 5, 5, 0, 1), (1, 2, 6, 7, 1, 0),
+  (1, 3, 5, 6, 0, 2), (2, 2, 6, 8, 2, 0).
+```
+
+The source on all five is bit `J + 1`. The first geometry is also run with
+bit `2`. Address counts are `128 + 256 + 2048 + 16384 + 4096`, and `128` again
+for the second source.

research/crt-joined-hole-repair/README.md

@@ -0,0 +1,85 @@
+# Joined one-target hole mask, reverse-word keys, and repair
+
+**Scoped proof with an exhaustive finite component. No new κ.** The selected
+conditional exponent is unchanged.
+
+## Scope and evidence
+
+Original card: `uniform-transfer-audit`, refined to one proposition. Cinna
+Davis's PR #4100 restores bad CRT addresses by the key `T(S^{-1}(x))` and a
+sparse repair (`CRT.md` §4). Three later audits each stop at their own output:
+
+- #4208/#4201 produce the one-target hole mask and erase the scanner's counter;
+- #4169's reverse word inverts the compact macro, including on dirty addresses;
+- #4328 prices the repair, but reads a host-built mask and a host-built table of `S`.
+
+#4328's first open question is to compose those pieces. Its stated blocker was
+the full `E(p, ell)` evaluator. That evaluator now has a constant in #4377, and
+it is a different machine from these reverse shears. The ownership join was
+still open.
+
+[PROOF.md](PROOF.md) counts the stencil for every admitted one-target geometry
+`(G, H, K, Y, J, B)`. The scanner mask is the hole set of the pinned `good`
+predicate. Keys at holes are the #4169 reverse shears followed by the ideal
+map; the program does not invert a stored table of `S`. Because `S` and `T`
+both permute the holes, sorting by `T(S^{-1}(x))` writes the record of `q` at
+`T(q)`. The producer's eight private tapes, the scanner counter, the mask and
+the repair scratch are erased.
+
+The universal shear inversion and the scanner's flag machine stay cited from
+#4169 and #4201. Both are rechecked on every address of the geometries below,
+not re-proved for every larger size. The repair cell counts obey the #4328
+bounds on this same schedule. They are not a new tariff.
+
+`verify.py` exhausts every address of
+
+```text
+(G, H, K, Y, J, B) =
+  (1, 1, 5, 5, 0, 0), (1, 1, 5, 5, 0, 1), (1, 2, 6, 7, 1, 0),
+  (1, 3, 5, 6, 0, 2), (2, 2, 6, 8, 2, 0)
+```
+
+with source bit `J + 1`, and repeats the first geometry with source bit `2`:
+**23,040** addresses and **19,392** holes. Three controls fail in the stated
+way. Origin keys still satisfy "key equals the hole address" and misplace the
+payload. A complemented mask does too, because `S = T` on the good set, and
+the ideal image fails. A source that reads bit `J` is rejected before repair.
+
+Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json).
+The selected record and catalogue are historical provenance.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 scripts/research_package.py --package research/crt-joined-hole-repair --check-only
+python3.12 -B research/crt-joined-hole-repair/verify.py
+```
+
+The verifier prints `PASS_CRT_JOINED_HOLE_REPAIR`.
+
+## Open next questions
+
+1. Does a two-target stencil, with disjoint guards, produce the product hole
+   set and restore payloads under the same reverse-word repair? CRT.md colors
+   several targets in one layer. The first step is one extra digit block and
+   one extra guard block at position `J + K`. It is blocked because the #4208
+   producer emits one target only.
+2. Is one reverse shear at most the #4377 budget
+   `E(p, ell) = 2^{4 ell}(p+2)^{16}` at the actual control width `H`? This
+   join does not identify the shears with that Beneš evaluator, so the `o(V)`
+   absorption is not yet a bit-step price for these keys. The first step is to
+   expand one `H`-bit modular addition in that bit-step model. It is blocked
+   because the shears are not expressed as those rotation tables.
+
+## Credit
+
+Cinna Davis supplies the CRT construction and the compact macro in PR #4100.
+ToikY's #4201 and #4208 supply the scanner and the unary producer. Hiroki
+KUMAZAKI's #4169 supplies the reverse word. Ryanson Jonathan's #4328 supplies
+the repair schedule, the cell bounds and the open composition question.
+Douglas Colkitt supplies the compact-control and sparse-repair ancestry those
+packages retain. Prepared by unpaidmoon with substantial Cursor Grok
+assistance. Apache-2.0. No independent human review or proof-assistant
+acceptance is claimed.

research/crt-joined-hole-repair/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/crt-arbitrary-source-repair/verify.py",
+      "usage": "input",
+      "git_blob": "813eafd24f031b046b2d4aaabdcb0950538980f1",
+      "sha256": "9a646116e430a242fc16c98d6e35c21290a00ccd9951145290b9a4bf5c007d48"
+    },
+    {
+      "path": "research/crt-dense-guard-scan/machine.py",
+      "usage": "input",
+      "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82",
+      "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7"
+    },
+    {
+      "path": "research/crt-unary-stencil-producer/producer.py",
+      "usage": "input",
+      "git_blob": "dd357a0679c244e5d95b2b782bd70ea9f2507795",
+      "sha256": "8586d019a0a35390d36b944a2b764ec96682040b1abc42e29d740faf5a830bd0"
+    },
+    {
+      "path": "research/pr4100-crt-repair-tariff/README.md",
+      "usage": "input",
+      "git_blob": "1eba9122777570041acbd5ddcfee22ceb0e60703",
+      "sha256": "5953ed2ae02a609744df2274810d7016cd766f2e43bdf8f79047084ae55a0513"
+    },
+    {
+      "path": "research/unconditional-batched-crt/check_batched_crt.py",
+      "usage": "input",
+      "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc",
+      "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e"
+    }
+  ]
+}

research/crt-joined-hole-repair/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.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 PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "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_status": "refined",
+  "actual_scope": "On an admitted one-target unary geometry, do the #4208/#4201 hole mask, the #4169 reverse-word keys and the #4328 repair form one program that restores every payload to the ideal switch and erases its private tapes?",
+  "scope_change_reason": "The card asks for one quantified implication of #4100 at its caller, prioritizing CRT total repair if that piece is still open. The mask, the reverse word, the repair tariff and the Beneš evaluator already have separate audits. The remaining named step is to run those repair pieces as one program. This package does that for one target. It does not reprice E(p, ell) or claim a new exponent.",
+  "bottleneck_link": "PR #4100's CRT route restores bad addresses by a keyed sparse repair. Separate audits of the mask, the keys and the tariff do not yet show that the mask tape is what the repair consumes. Closing that ownership join is one caller-bound obligation of the proposed transfer. It does not select a new exponent.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the one-target ownership join and its failure controls. Do not build a many-target stencil, a Beneš bit-step price for the shears, or a new kappa.",
+  "outcome": "completed",
+  "evidence": "PROOF.md counts the stencil and applies the permutation lemma to the reverse-word keys. verify.py exhausts 23,040 addresses over five geometries and two sources, checks both invoices, and rejects origin keys, a complemented mask and a target-dependent source. It prints PASS_CRT_JOINED_HOLE_REPAIR.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Cursor Grok, substantial assistance with the proof writeup and the verifier.",
+  "open_questions": [
+    {
+      "question": "Does a two-target stencil, with disjoint guards, produce the product hole set and restore payloads under the same reverse-word repair?",
+      "why_it_matters": "CRT.md colors several targets in one layer. A one-target join does not show that a second guard block preserves ownership or the permutation.",
+      "first_step": "Extend the unary producer by one more digit block and one more guard block at position J+K, and rerun this repair on every address of one small pair.",
+      "blocked_by": "The #4208 producer emits one target only. This package does not add a second block."
+    },
+    {
+      "question": "Is one reverse shear at most the #4377 bit-step budget E(p, ell) = 2^{4 ell}(p+2)^{16} when the control width is the actual H?",
+      "why_it_matters": "This join uses the ten #4169 shears as the key procedure. #4377 prices a different Beneš evaluator. The o(V) repair absorption still needs a bit-step price for these shears.",
+      "first_step": "Expand one modular addition on an H-bit control into head moves in the #4377 bit-step model and compare it with E at H = G = 64(ell + ceil(log2(p+2))).",
+      "blocked_by": "The reverse shears are not expressed as that evaluator's rotation tables, and this package does not translate them."
+    }
+  ]
+}

research/crt-joined-hole-repair/VERIFY.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/crt-arbitrary-source-repair/verify.py",
+    "research/crt-dense-guard-scan/machine.py",
+    "research/crt-unary-stencil-producer/producer.py",
+    "research/pr4100-crt-repair-tariff/README.md",
+    "research/unconditional-batched-crt/check_batched_crt.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Stencil atoms, mask bits, shear inverses and ideal restoration on 23040 addresses; producer and scanner invoices; repair cell bounds; rejection of origin keys, a complemented mask and a target-dependent source."
+    }
+  ]
+}