Decide #4100 CRT.md's guard premise: mod-K coloring needs (K-1)-bit guards; vacuous on #4174's production plans (no new κ)

research/pr4100-guard-coloring/README.md

@@ -0,0 +1,179 @@
+# Guard windows under #4100's position-mod-K coloring
+
+**Claim type: a scoped proof audit with a counterexample to the literal text,
+plus a census of #4174's actual production descriptors. No new κ.** This
+does not accept #4100 and changes nothing in it.
+
+## Object
+
+Cinna Davis's [CRT.md](../unconditional-batched-crt/CRT.md) §4, at #4100 head
+`337d04939571a637aeab54a0f58f54fde811663a`, says three things:
+
+- the good predicate requires "a margin 2B from both ends of each K-bit
+  guard";
+- the bad density is at most `r[2/B + 8B/2^K]`;
+- "Color targets by current position modulo K, so guard intervals are
+  disjoint."
+
+Three open audits take this disjoint-guard premise as given:
+
+- #4321 (unpaidmoon) assumes "the `K`-bit guards are pairwise disjoint" and
+  notes that no audit decides that hypothesis.
+- #4328's exact `r`-target density needs disjoint windows.
+- #4174 (kumagi) supplies the actual placement descriptors; this package
+  checks them.
+
+## Results
+
+### 1. Lemma
+
+Let one macro's active targets all share a color, that is, a residue of their
+`y`-significance position mod `K`.
+
+- With `(K−1)`-bit guards (the `K−1` bits above each target), the guards are
+  pairwise disjoint and contain no active target, for every descriptor.
+  Distinct same-color targets differ by a nonzero multiple of `K`, hence by
+  at least `K`.
+- With `K`-bit guards, they are still pairwise disjoint, but a guard contains
+  another active target exactly when two same-color targets are `K` apart.
+
+This is checked exhaustively on 3,266 small position sets.
+
+### 2. The literal `K`-bit reading fails on #4100's own gadget
+
+In #4100's `check_batched_crt.py`, `good(…, guard=g)` reads `g−1` window bits.
+Its two-target fixture places the targets at positions 0 and 6, exactly
+`K = 6` apart. Running every one of the `2^20` addresses:
+
+| Source | Window bits | Good addresses | `S ≠ T` on good addresses | `T` leaves the good set |
+| --- | --- | --- | --- | --- |
+| #4100's `source_pair` | 5 (`K−1`) | 82,944 | 0 | 0 |
+| #4100's `source_pair` | 6 (`K`) | 186,624 | **3,888** | **31,104** |
+| second pair | 5 (`K−1`) | 82,944 | 0 | 0 |
+| second pair | 6 (`K`) | 186,624 | **2,388** | **15,552** |
+
+Example: `(u,t,y) = (0,1,1086)` goes to `(0,5,1087)` instead of
+`(0,1,1087)`. A carry inside target 0's 6-bit window flips target 1 before
+target 1 is read, so the control field is not restored.
+
+**Consequence.** The premise must read "**`(K−1)`-bit guards**, free of active
+targets". The equivalent alternative is `K`-bit guards with coloring mod
+`K+1`. This matches the code, and it matches the density term `8B/2^K`,
+which counts `4B` bad values in `K−1` bits. A `K`-bit window would give
+`4B/2^K`. This is a presentational correction to CRT.md's "K-bit guard" and
+to #4321's hypothesis wording. No bound changes.
+
+### 3. #4174's production descriptors
+
+The layout is #4174's own production census: `d = 65,536`, `ell = 24`,
+widths alternating 24/23, `p = 6L`. That gives:
+
+| `L` | `G` | `K` | `r_max` | `H` | `y` bits |
+| --- | --- | --- | --- | --- | --- |
+| 1,540,096 | 3,072 | 196,608 | 5 | 15,360 | 1,494,016 |
+
+The census covers all 104,864 plans, 524,288 active-axis visits and 524,314
+fragments:
+
+- **Every active axis lies in `y`** after the three exchanges.
+- **No two active axes of any plan can ever share a color, for any Beneš bit
+  schedule.** For every pair of fragments, the range of position differences
+  contains no nonzero multiple of `K`. This holds even though pairs reach
+  1,463,286 bits apart. The aligned schedule (bit `m` on every axis wider
+  than `m`) confirms it over 12,304,384 target visits: maximum color
+  multiplicity 1, and no exact-`K` pair.
+- **So at production parameters the disjoint-guard premise holds
+  vacuously,** and each compact macro handles one target. The multi-target
+  cancellation, and #4328's `r ≥ 2` density, are not exercised there. The
+  `O(K)`-colors-per-layer tariff covers this.
+- **The last-`K` branch carries a material share.** 16,225 plans (15.5%) have
+  active axes in the top `K−1` bits of `y`. Under the aligned schedule,
+  388,466 plan-layers contain exceptions, up to all 5 targets. At these sizes
+  `K/|y| ≈ 13%`. #4187 audits that branch at `O(VK)`.
+
+### 4. Other admitted width patterns
+
+The same census ran on eight more width patterns at `d = 65,536`, each
+accepted by #4174's `Layout`:
+
+| Pattern | Plans | Possible same-color pairs | Aligned: max multiplicity / exact-`K` pairs | Plans with last-`K` axes |
+| --- | --- | --- | --- | --- |
+| alternating 24/23 (production) | 104,864 | 0 | 1 / 0 | 16,225 |
+| blocked: 24 on axes 0..32767, then 23 | 104,864 | 0 | 1 / 0 | 16,534 |
+| blocked: 23 on axes 0..32767, then 24 | 104,864 | 0 | 1 / 0 | 15,925 |
+| uniform 24 | 104,864 | 0 | 1 / 0 | 15,899 |
+| uniform 23 (all `ell−1`, `r_max = 4`) | 131,072 | 0 | 1 / 0 | 20,654 |
+| random, half short, seed 4100 | 104,864 | 0 | 1 / 0 | 16,227 |
+| random, half short, seed 4174 | 104,864 | 0 | 1 / 0 | 16,232 |
+| random, 1/8 short, seed 4329 | 104,864 | 0 | 1 / 0 | 15,986 |
+| alternating 32/31 (`ell = 32`, `K = 229,376`) | 104,864 | 0 | 1 / 0 | 14,078 |
+| **uniform 24, one `ell−1` axis at 20000** | 104,864 | **1** (exact `K`) | 1 / 0 | 15,899 |
+| **uniform 24, `ell−1` axes 16384..16407** | 104,864 | **1** (exact `K`) | **2 / 24** | 15,899 |
+
+In every pattern, every active axis lies in `y`, and wherever a color holds
+two targets, the `(K−1)`-bit windows are checked directly to be target-free.
+
+**The vacuity is pattern-specific, and the `K−1` correction is needed on
+admitted layouts.** Uniform 24 comes within one bit of a collision. At level
+14, batch 1638 pairs axes 16383 and 24576. A batch can straddle a skipped
+left half, and here the 8,193 axes between them span `196,632 = K + 24` bits.
+Shortening 24 of the axes in between gives an admitted pattern (the last row)
+where the aligned Beneš schedule puts two active targets of one color
+**exactly `K` apart** at 24 layers. Under literal `K`-bit guards each such
+target sits inside the other's window, which is the gadget failure of §2.
+With `(K−1)`-bit guards those windows are target-free. Shortening a single
+axis instead reaches exact `K` for some bit schedule, but not the aligned one.
+
+## Evidence
+
+`verify.py` uses only the standard library and takes about 2 minutes (11 censuses). It
+also checks the source bindings: SHA256 pins of CRT.md and
+`check_batched_crt.py`, 3 exact CRT.md phrases, `good()`'s `guard−1` window
+expression, and the byte hash of the vendored allocator.
+
+## Not covered
+
+- Other values of `d` and `ell`. Eleven patterns are censused at
+  `d = 65,536`, with `ell ∈ {24, 32}`. The lemma covers every descriptor with
+  `(K−1)`-bit guards.
+- The elementary last-`K` branch's correctness (#4187).
+- The control-function supports (#4169, #4174).
+- There is no proof-kernel check.
+
+## Reproduce
+
+```sh
+python3 scripts/research_package.py --package research/pr4100-guard-coloring --check-only
+python3.12 scripts/research_package.py --package research/pr4100-guard-coloring
+python3.12 -B research/pr4100-guard-coloring/verify.py
+```
+
+The verifier prints `PASS_PR4100_GUARD_COLORING_FINITE`.
+
+## Open next questions
+
+1. **Price macros per occupied color, not per residue.**
+   - *Why it matters:* in every regular pattern each color is a singleton, so
+     a layer uses at most `r_max` macros per batch rather than `K`. The tariff could
+     be stated per occupied color.
+   - *First step:* bound occupied colors per batch by `r_max` in the CRT §4
+     cost line.
+   - *Blocked by:* nothing.
+2. **Fix the window convention in the written construction.** (The earlier
+   question 2, other width patterns, is answered in §4.)
+   - *Why it matters:* an admitted layout puts same-color targets exactly `K`
+     apart, so the text's "K-bit guard" must become `(K−1)` bits, or the
+     coloring must be mod `K+1`. That change also changes #4321's hypothesis
+     wording.
+   - *First step:* restate CRT.md §4's predicate with `(K−1)`-bit windows and
+     re-derive `8B/2^K`.
+   - *Blocked by:* author or maintainer action on #4100's text.
+
+## Credit
+
+The construction and audited text are Cinna Davis's #4100 (OpenAI Codex
+assistance). The placement descriptors are Hiroki KUMAZAKI's (@kumagi) #4174,
+vendored unmodified; see [vendor/NOTICE.md](vendor/NOTICE.md). #4321
+(unpaidmoon) states the guard hypothesis this package decides. Prepared by
+Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/pr4100-guard-coloring/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/unconditional-batched-crt/CRT.md",
+      "usage": "input",
+      "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6",
+      "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b"
+    },
+    {
+      "path": "research/unconditional-batched-crt/check_batched_crt.py",
+      "usage": "input",
+      "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc",
+      "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e"
+    }
+  ]
+}

research/pr4100-guard-coloring/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "Decide the disjoint-guard premise of #4100 CRT.md section 4 under position-mod-K coloring: a window lemma, a counterexample to the literal K-bit guard on #4100's own gadget, and a census of #4174's actual production placement descriptors, plus eight further admitted width patterns and two adversarial ones.",
+  "scope_change_reason": "The card asks for one quantified implication at its caller; this is the guard hypothesis that #4321 and #4328 assume and no audit decided, checked at the actual caller's descriptors (#4174).",
+  "bottleneck_link": "The compact switch's correctness and the bad-density term both rest on this premise; a wrong window convention breaks the gadget on good addresses.",
+  "budget_minutes": 75,
+  "stop_rule": "Stop once the premise is decided (lemma plus counterexample) and checked on #4174's production descriptors.",
+  "outcome": "completed",
+  "evidence": "verify.py: 3,266 exhaustive lemma cases; #4100's gadget on all 2^20 two-target addresses at spacing K: (K-1)-bit guards give S=T on all 82,944 good addresses, K-bit guards fail on 3,888/2,388 good addresses and T leaves the good set on 31,104/15,552; #4174 production census (104,864 plans, 524,288 axis visits): all axes in y, zero possible same-color pairs for any Benes schedule, aligned multiplicity 1, 16,225 plans with last-K exception axes; eight more admitted patterns (blocked both ways, uniform 24, uniform 23, three random, ell=32): zero possible same-color pairs; uniform 24 misses a multiple of K by one bit, and the admitted pattern with ell-1 axes 16384..16407 puts aligned same-color targets exactly K apart at 24 layers, where (K-1)-bit windows are checked target-free.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, the lemma, census implementation and writing; no independent human or proof-kernel review.",
+  "open_questions": [
+    {
+      "question": "Price compact macros per occupied color rather than per residue mod K.",
+      "why_it_matters": "At #4174's production descriptors every color is a singleton, so a layer needs at most r_max macros per batch, not K.",
+      "first_step": "Bound occupied colors per batch by r_max in the CRT section 4 cost line.",
+      "blocked_by": "None."
+    },
+    {
+      "question": "Restate CRT.md section 4's guard with (K-1)-bit windows (or coloring mod K+1).",
+      "why_it_matters": "An admitted layout puts same-color targets exactly K apart, so the literal K-bit guard fails there; #4321's hypothesis wording follows the text.",
+      "first_step": "Restate the predicate with (K-1)-bit windows and re-derive the 8B/2^K term.",
+      "blocked_by": "Author or maintainer action on #4100's text."
+    }
+  ]
+}

research/pr4100-guard-coloring/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/unconditional-batched-crt/CRT.md",
+    "research/unconditional-batched-crt/check_batched_crt.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Source pins, CRT.md phrases, good()'s guard-1 window and the vendored #4174 allocator hash; exhaustive window lemma; #4100's two-target gadget with (K-1)-bit versus K-bit guards on all 2^20 addresses; census of all 104,864 #4174 production plans; eight further admitted width patterns and two adversarial ones with direct (K-1)-window checks."
+    }
+  ]
+}

research/pr4100-guard-coloring/vendor/NOTICE.md

@@ -0,0 +1,19 @@
+# Vendored file
+
+`pr4174_allocator.py` is a byte-identical copy of
+`research/crt-reservoir-placement/allocator.py` from
+[PR #4174](https://github.com/CrocSwap/integer-mult-bounds/pull/4174).
+
+| Field | Value |
+| --- | --- |
+| Head | `5fec853f0c048871de3b8098d1e30d4ee19cda23` |
+| Git blob | `4b3ad89652a28f7d142248d1b5747272e696493c` |
+| SHA256 | `b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688` |
+
+It is copied, not pinned, because that PR head is not reachable from canonical main, and
+package pins resolve only against reachable Git objects. `verify.py` checks the SHA256
+before importing the file.
+
+Author: Hiroki KUMAZAKI (@kumagi), with substantial OpenAI Codex assistance. It implements
+the CRT.md §3 placement of Cinna Davis's PR #4100. Apache-2.0, as stated in the file. It is
+unmodified.