Price CRT switch layers by occupied color.

research/crt-occupied-color-macros/PROOF.md

@@ -0,0 +1,114 @@
+# Occupied colors, not all K residues, are the macros
+
+## Statement
+
+CRT.md §4 colors targets by current position modulo `K` and charges one
+switch layer as `O(K)` colors. The macros that the same paragraph prices
+are the occupied colors. On every batch cut by the pinned #4174 layout,
+
+```text
+c ≤ r ≤ r_max,
+```
+
+where `r` is the number of active targets, `c` is the number of distinct
+residues modulo `K`, and `r_max` is that layout's batch cap. Empty residues
+are not macros. A same-color pair is one macro.
+
+At the recomputed production point `d = 65536`, `ell = 24`, alternating
+widths `24/23`, this cap is `r_max = 5` and `K = 196608`. The color factor
+in the §4 layer sentence may be `5` rather than `196608`. The ratio is the
+exact rational `196608/5`. No new κ is claimed. #4100 is not accepted.
+
+## Definitions
+
+A batch is a finite set of active target positions. Its target count is `r`.
+For an integer `K ≥ 1`, the occupied-color count is
+
+```text
+c = |{ position mod K : position is an active target }|.
+```
+
+The pinned layout, transcribed from
+`research/pr4100-guard-coloring/vendor/pr4174_allocator.py`
+(`Layout.__init__`), sets
+
+```text
+logarithm = ceil(log2(p + 2)),
+G = 64 (ell + logarithm),
+K = 64 G,
+r_max = L // (100 G),
+H = r_max G,
+```
+
+with `L` the total width and `p` the precision parameter passed to the
+constructor. The constructor cuts each right-child stream into consecutive
+groups of at most `r_max` axes, so every batch it emits has `r ≤ r_max`.
+
+## Lemma 1
+
+For any batch and any `K ≥ 1`, `0 ≤ c ≤ min(r, K)`. Also `c = r` if and
+only if the `r` residues are pairwise distinct.
+
+Proof. The residue map sends the `r` targets onto a set of size `c`, so
+`c ≤ r`. The codomain has `K` residues, so `c ≤ K`. The map is bijective
+onto its image exactly when no two targets share a residue, which is
+`c = r`.
+
+## Lemma 2
+
+Every batch emitted by the pinned layout satisfies `c ≤ r_max`.
+
+Proof. The layout's own cut gives `r ≤ r_max`. Lemma 1 gives `c ≤ r`.
+
+A collision does not increase the macro count. If two targets differ by a
+nonzero multiple of `K`, then `c < r`, so the occupied-color bill is
+strictly smaller than one macro per target. The `(K−1)`-bit guard
+separation that lets those two targets share one macro is the lemma in
+`research/pr4100-guard-coloring`; it is cited, not replayed.
+
+## Substitution into the §4 cost line
+
+CRT.md §4 says the coloring "uses `O(K)=O(ell+log p)` colors", that one
+color costs `O(V H^(1-a)+V)`, and that with `K` colors and `H≤L=O(p)` one
+switch layer costs `O(V p^(1-a) (ell+log p))`. The factor `ell+log p` is
+the `O(K)` color count. Replacing that count by the occupied-color count
+replaces the layer bound by
+
+```text
+O(c (V H^(1-a) + V)),    c ≤ r_max.
+```
+
+On a layout whose `r_max` and `H` are fixed integers, the color factor is
+the integer `r_max`, not the integer `K`, whenever `r_max < K`.
+
+## Production corollary
+
+Take `d = 65536`, `ell = 24`, and `p = 6L`, which is the constructor call
+in `research/pr4100-guard-coloring/verify.py`. Alternating widths `24, 23,
+24, 23, ...` give
+
+```text
+L = 1540096,  logarithm = 24,  G = 3072,
+K = 196608,   r_max = 5,       H = 15360,
+y-bit count = 1494016.
+```
+
+These are the production row of that package's table. Lemma 2 gives
+`c ≤ 5` on every batch, while the written sentence multiplies by
+`K = 196608`. The color factors are in the exact ratio
+
+```text
+K / r_max = 196608/5.
+```
+
+The same constructor with every width `23` (nominal `ell = 24`) gives
+`L = 1507328`, the same `K = 196608`, and `r_max = 4`. That is the table's
+uniform-`23` row. Its color ratio is the integer `196608/4 = 49152`.
+
+## What this does not say
+
+The §5 product `O(V p^(1-a) ell^2 polylog p)` still hides `K` inside the
+polylogarithmic factor. This note does not rewrite that line and does not
+rerun the 104,864-plan census. It does not build the literal many-target
+tape macro, does not change a selected supplier, and does not accept #4100.
+The selected conditional exponent stays `605457647/200000000000`.

research/crt-occupied-color-macros/README.md

@@ -0,0 +1,122 @@
+# Price CRT switch layers by occupied color
+
+**Scoped tariff lemma. No new κ.** The selected conditional exponent stays
+`605457647/200000000000`. #4100 is not accepted.
+
+## Result
+
+CRT.md §4 colors active targets by position modulo `K` and charges a switch
+layer for `O(K)` colors. The macro that paragraph prices is one occupied
+color. For every batch cut by the pinned #4174 layout,
+
+```text
+c ≤ r ≤ r_max.
+```
+
+Here `r` is the number of active targets, `c` is the number of distinct
+residues modulo `K`, and `r_max` is the layout's batch cap. Empty residues
+are not macros. Two targets exactly `K` apart are one macro.
+
+At `d = 65536`, `ell = 24`, and alternating widths `24/23`, with the
+constructor call `p = 6L` used by `research/pr4100-guard-coloring`, the
+parameters recompute as `L = 1540096`, `K = 196608`, `r_max = 5`, and
+`H = 15360`. The §4 color factor may be `5` instead of `196608`. The ratio
+is exactly `196608/5`. The all-short width `23` row recomputes as
+`r_max = 4` and ratio `49152`.
+
+The proof is in [PROOF.md](PROOF.md). The singleton-color hypothesis in the
+predecessor's open question is sufficient but not necessary: the batch cap
+already forces `c ≤ r_max` when a color collides.
+
+## Scope
+
+Task card `uniform-transfer-audit`, priority revision 7, base
+`32890bc5de034ab8fc93ac88ead7279a6a416d04`. Scope status is **refined**.
+
+The card asks whether one quantified step of #4100 holds at its caller.
+This package prices the occupied-color factor in the CRT.md §4 layer
+sentence. It is item 12 of the ordered list below.
+
+Ordered eligible list for session r44, rebuilt on 2026-10-25 against
+`32890bc5de034ab8fc93ac88ead7279a6a416d04`. Open handoffs from the 19
+October index come first. Answered handoffs are dropped. Priority-table
+rows come next, and inside `uniform-transfer-audit` the still-open
+successors follow the order recorded in
+`research/pr4100-ledger-boundary-exponent`: the first still-open successor
+of an answered row, then the second. A row is dropped when a merged
+package, an open pull request, an excluded unpaidmoon delivery, or a fork
+`cursor/*` branch already answers it.
+
+1. A caller that accepts `(w, q, v_N)` without restoring the original source
+   slots (discussion comment 19030045).
+2. Whether the PR2809 continuation serializer parks the ancestor chain or
+   one root-sized stream per cut.
+3. Whether marker, template, and erased-backing cells sit inside the
+   `26041 V` budget.
+4. Whether the stored narrow band has at most `2p` off-diagonal entries and
+   the rounding meets `2^{-5p}`.
+5. Whether a byte-identical `outer/check_ledger.py` regenerates the
+   `tau_eff` point.
+6. Whether the word-level scalar inventory fits constant one at the two
+   excluded `p = 2` corners.
+7. Whether the full-batch allowance composes with reservoir placement and
+   the paid repair-key service.
+8. Whether the normalized 1-norm stays below the infinity norm on longer
+   Gaussian paths.
+9. An explicit `C` and `k` for `mu ≤ C (W/B) (log p)^k`.
+10. A physically costed producer for the 32-bit CRT source ROM.
+11. The control cost of the joined producer, scanner, and repair.
+12. **This package.** Macros per occupied color, bounded by `r_max`.
+
+Dropped before this cut: the fresh T385 wrapper, the six-tape head-move
+bill, the retiming handoff, the four-provider rebind, the matched
+park/restore comparison (open #4167 and #4172), the literal `evaluate_key`
+tape service, the separator-corner enclosure and its immediate Neumann
+readings, the stack `O_q(V)` claim, and the printed `tau_eff` choice.
+Catalogue cards already closed by this account, including the rank-8
+producer, the difference-basis census, the compact-switch audit, and the
+stock, replay, packing, and scalar-itinerary cards, stay off the list.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -B research/crt-occupied-color-macros/verify.py
+python3 -B scripts/research_package.py --package research/crt-occupied-color-macros
+```
+
+`verify.py` prints
+
+```text
+PASS_CRT_OCCUPIED_COLOR_MACROS K=196608 r_max=5 ratio=196608/5 uniform23_r_max=4 ratio=49152 same_color_pair_macros=1 no_new_kappa=true
+```
+
+It hashes CRT.md and the layout allocator, checks the §4 sentences, exhausts
+the `2^12` subsets of a 12-point universe at `K = 6`, and recomputes both
+production rows. Not run: the 104,864-plan census, Lean, Docker, and the
+selected cold replay.
+
+## Open next questions
+
+1. Can §5's `ell^2 polylog p` line be rewritten with `r_max` in place of the
+   hidden `K` factor, and does any later numerical budget use the looser
+   factor? The first step is to expand `O(log d)` levels times `O(ell)`
+   layers times `c ≤ r_max` colors. The blocker is that §5 does not display
+   `K` as a separate multiplier.
+2. Does one same-color macro's repair bill stay inside the one-color `O(V)`
+   when that color holds two targets? The first step is the bad-density line
+   at `r = 2` and this `K`. The literal many-target tape macro is still
+   unpinned, so this question does not ask for that program.
+
+## Credit
+
+The coloring, the `O(K)` layer sentence, and the one-color cost are Cinna
+Davis's #4100. The batch cap `r_max = L // (100 G)` is Hiroki KUMAZAKI's
+#4174 layout, as vendored by Ryanson Jonathan in
+`research/pr4100-guard-coloring`. That package leaves the occupied-color
+price open and proves the `(K−1)`-bit guard lemma cited here. #4321
+(unpaidmoon) stated the disjoint-guard hypothesis that package decided.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human review and no formal-kernel acceptance are claimed.

research/crt-occupied-color-macros/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/unconditional-batched-crt/CRT.md",
+      "usage": "input",
+      "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6",
+      "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b"
+    },
+    {
+      "path": "research/pr4100-guard-coloring/vendor/pr4174_allocator.py",
+      "usage": "input",
+      "git_blob": "4b3ad89652a28f7d142248d1b5747272e696493c",
+      "sha256": "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688"
+    }
+  ]
+}

research/crt-occupied-color-macros/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "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": "Replace the CRT.md section-4 switch-layer factor O(K) by the occupied-color count, and prove that count is at most the pinned layout batch cap r_max.",
+  "scope_change_reason": "The card asks for one quantified #4100 implication at its caller. This is the unblocked occupied-color price left by research/pr4100-guard-coloring, the still-open many-target macro tariff. It does not build a tape macro, replay the production census, or accept #4100.",
+  "bottleneck_link": "Side result under the retained #4100 transfer audit. A tighter color factor does not change the selected exponent; unknown tape and repair costs stay unknown.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the occupied-color inequality and the recomputed production ratios are checked. Do not rerun the 104864-plan census or write a many-target tape program.",
+  "outcome": "completed",
+  "evidence": "PROOF.md lemmas and verify.py: CRT.md and allocator hashes, section-4 sentences, 4096-subset residue census, production rows K=196608 with r_max=5 and r_max=4.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance for the proof, verifier, and package text. No independent human or formal-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Can the section-5 ell^2 polylog p line be rewritten with r_max in place of the hidden K factor?",
+      "why_it_matters": "The layer sentence is tighter, but the aggregate still hides K, so a later numerical budget may keep the loose factor.",
+      "first_step": "Expand O(log d) levels times O(ell) layers times c <= r_max colors and compare with the written aggregate.",
+      "blocked_by": "Section 5 does not display K as a separate multiplier."
+    },
+    {
+      "question": "Does one same-color macro's repair bill stay inside the one-color O(V) when that color holds two targets?",
+      "why_it_matters": "Occupied-color pricing charges one macro for a collision; the repair term might still grow with the target count.",
+      "first_step": "Instantiate the bad-density line at r = 2 and K = 196608.",
+      "blocked_by": "The literal many-target tape macro is not pinned, and this question does not ask for it."
+    }
+  ]
+}

research/crt-occupied-color-macros/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/unconditional-batched-crt/CRT.md",
+    "research/pr4100-guard-coloring/vendor/pr4174_allocator.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "CRT.md and allocator hashes, the K-color sentence, the 4096-subset lemma, and both recomputed production rows."
+    }
+  ]
+}