From 45bb71aed0dc03323338d6d648585c1a424d072d Mon Sep 17 00:00:00 2001 From: Ryanson Jonathan Date: Wed, 21 Oct 2026 16:17:16 +0700 Subject: [PATCH 1/3] Audit #4100 CRT.md's sparse exception repair tariff Per-step accounting of extraction from the hole mask, TS^-1 keys at holes, two-bucket radix passes, keyed reinsertion and erasure at Theta(p)-bit records, where PR2250's tariff does not transfer; exact absorption at #4100's G, B, K; literal tape run around #4100's own compact/good fixture with failing controls (full-input sort, keys without T, no repair). No new kappa. Co-Authored-By: Claude Opus 5.5 --- research/pr4100-crt-repair-tariff/README.md | 169 +++++++++ .../pr4100-crt-repair-tariff/SOURCES.json | 36 ++ research/pr4100-crt-repair-tariff/TASK.json | 80 ++++ research/pr4100-crt-repair-tariff/VERIFY.json | 22 ++ research/pr4100-crt-repair-tariff/verify.py | 351 ++++++++++++++++++ 5 files changed, 658 insertions(+) create mode 100644 research/pr4100-crt-repair-tariff/README.md create mode 100644 research/pr4100-crt-repair-tariff/SOURCES.json create mode 100644 research/pr4100-crt-repair-tariff/TASK.json create mode 100644 research/pr4100-crt-repair-tariff/VERIFY.json create mode 100644 research/pr4100-crt-repair-tariff/verify.py diff --git a/research/pr4100-crt-repair-tariff/README.md b/research/pr4100-crt-repair-tariff/README.md new file mode 100644 index 0000000000..f08dd8e5b9 --- /dev/null +++ b/research/pr4100-crt-repair-tariff/README.md @@ -0,0 +1,169 @@ +# The sparse exception repair tariff of #4100's CRT.md §4 + +**Claim type: a scoped proof audit (per-step accounting with explicit +constants and exact absorption at #4100's parameters), checked against a +literal tape run of the repair around #4100's own compact fixture. No new +κ.** This does not accept #4100 and changes nothing in it. + +## Object and gap + +The object is the repair step of Cinna Davis's +[CRT.md](../unconditional-batched-crt/CRT.md) §4, #4100 head +`337d04939571a637aeab54a0f58f54fde811663a`. It reads: "On the bad holes, +apply the correction key `T(S^-1(x))`, sort those holes by this full key on +fixed tapes, and merge them back … It does not sort the full input." It then +says that "bad-key evaluation, O(p)-bit keys, radix passes, counters and +clearing all fit O(V)". + +**Every existing CRT audit leaves this tariff out:** +- #4169 lists "sequential head movement/sorting costs"; +- #4174 lists the "sorting tariff"; +- #4187 lists the repair integration; +- #4201 and #4208 list "exception extraction, inverse keys, sorting, payload + routing, reinsertion"; +- #4321 lists "bad-key repair". + +**Why PR2250's tariff does not carry over.** The mechanism comes from +jmbarrancoml's merged PR2250 +([PROOF §3–4](../selected-complex-compact-adapters/PROOF.md)): extraction, +inverse destination keys, two-bucket stable binary radix passes, keyed +reinsertion and erasure. Its cost is `O(V + M A³ + δ M A(R+A))`, absorbed +only because PR2250's records are superpolynomial (`A^C/R → 0`). In CRT.md, +`R` and `A = L` are both `Θ(p)`, so `M A³ = Θ(p²)·V`. CRT.md itself says not +to import that tariff unchanged. Its replacements are: +- the linear `O(ML)` guard scan (#4201) for the hole mask; +- `E(p,ell)`-cost keys evaluated only at holes; +- key comparisons only at holes. + +Nobody had checked that combination. + +**Outcome: the tariff holds.** Per color, the repair costs `O(V)` dense work +plus a sparse part that is `o(V)` with an enormous margin at every `p`. + +## Results + +Write `M = 2^L` records of `R` cells, `N` holes, and `δ = N/M`. + +**1. Dense part: `≤ 9MR + 5M` cells.** +- Read the guard scan's hole mask once. +- Split good records onto a good stream. +- Reinsertion overwrites the data region from cell 0 and consumes the good + stream and the mask in order. +- Erase both. +- No key, inverse or arithmetic work touches a good record. + +**2. Sparse part: `≤ N(L+R)(9L+6)` cells, plus `N` key evaluations.** +- At each hole, copy the `L`-bit address, evaluate `T(S^-1(x))` (cost + `E(p,ell)`, CRT.md's premise), and append key and record. +- Run `L` stable two-bucket LSD passes, each nine sweeps of the keyed holes: + read, bucket write, two rewinds, bucket read, concatenation write, a + two-sweep erase, and the next rewind. +- Reinsertion reads one sorted keyed hole per hole bit, then erases. + +**3. Counter: `≤ 8M + 4LN + 4L`.** This is two amortized binary-counter +scans plus address reads at holes only. + +**4. Correctness.** `T∘S^-1` permutes the bad set, because both maps +preserve it. So the `k`-th smallest key is the `k`-th hole address, and +reinsertion sends the record at `x` to `T(S^-1(x))`. This is PR2250's +argument, and it holds unchanged at these record widths. + +**Caution.** The reinsertion check "key equals current address" only proves +that the keys *permute the holes*. Keys `S^-1(x)` without `T` also permute +them and pass the check, while misplacing every hole record (control below). +Correct keys therefore rest on the inverse evaluator: #4169's literal reverse +word, composed with `T`. + +**5. Absorption at #4100's parameters.** CRT.md sets +`G = 64(ell + ⌈log₂(p+2)⌉)`, `B = 2^G`, `K = 64G` and `r ≤ L/(100G)`. +The bad density is `δ ≤ r(2/B + 8B/2^K)`, which the fixtures check exactly +at `r = 1`. + +- **Sparse moves:** `δ(1+L/R)(9L+6) + δ·4L/R`. Since + `2^-G ≤ 2^-64ell (p+2)^-64`, this is below `p³(p+2)^-64` for `L ≤ p` and + `R ≥ p/8`. So it is absorbed at **every** `p`, not just eventually. The + exact values range from `2^-640` (`p = 16`) to `2^-37,326` (`p = 2^64`). +- **Key evaluations:** `δ·E/R`, where `2^-G·2^(4ell)(p+2)^16 ≤ + 2^(-60ell)(p+2)^(-48)` holds exactly. This is CRT.md's displayed line; the + constant `C` in `E ≤ C·2^(4ell)(p+2)^16` remains CRT.md §2's. + +## Evidence + +`verify.py` uses only the standard library and takes about 6 seconds. + +- **Fixtures.** The macro `S` and the ideal switch `T` come from #4100's + pinned `check_batched_crt.py` (`compact`, `good`). There are five fixtures, + with `B ∈ {4, 8, 16}`, guard 6 or 8, three source functions and + `M = 1,024` to `65,536`. +- **Correctness.** Each fixture checks that `S` and `T` are bijections, that + both preserve the good set, and that `S = T` on good addresses. The repair + then realizes `T` on every record. +- **Density.** The measured density never exceeds `2/B + 8B/2^K`. + +| `B`, guard, `M` | Holes | Dense / `MR` | Sorted / (holes·`L(L+R)`) | +| --- | --- | --- | --- | +| 4, 6, 1,024 | 736 | 5.91 | 9.50 | +| 4, 6, 16,384 | 11,776 | 5.76 | 9.36 | +| 8, 8, 16,384 | 6,976 | 7.23 | 9.36 | +| 8, 8, 65,536 | 27,904 | 7.18 | 9.31 | +| 16, 8, 65,536 | 36,736 | 6.51 | 9.31 | + +Toy `B` makes holes dense here. At #4100's `G`, `δ ≈ 2^-G` (item 5). + +**Controls,** each of which must fail: +- **Full-input sort.** It evaluates 16,384 keys, not 11,776, and moves + 262·`MR`, which is `Θ(L)·V`. This is why CRT.md avoids it. +- **Keys `S^-1(x)`.** 5,888 records are misplaced, undetected by the + reinsertion check. +- **No repair.** 2,048 records are wrong. + +**Source binding:** SHA256 pins of CRT.md, `check_batched_crt.py` and +PR2250's PROOF.md, with 9 exact phrases. + +## Not covered + +- The cost of the `E(p,ell)` evaluator itself; #4192 covers its Beneš part. +- The guard scan that produces the hole mask (#4201, #4208). +- The macro `S`'s ordinary interchanges, the last-`K` branch (#4187), and + reservoir placement (#4174). +- The fixtures have one target. CRT.md's `r`-target density is the union + bound, checked here only at `r = 1`. +- There is no proof-kernel check. + +## Reproduce + +```sh +python3 scripts/research_package.py --package research/pr4100-crt-repair-tariff --check-only +python3.12 scripts/research_package.py --package research/pr4100-crt-repair-tariff +python3.12 -B research/pr4100-crt-repair-tariff/verify.py +``` + +The verifier prints `PASS_PR4100_CRT_REPAIR_TARIFF_FINITE`. + +## Open next questions + +1. **Compose the hole mask, key evaluator and repair into one fixed-tape + program.** + - *Why it matters:* the three pieces (#4201/#4208, #4192/#4169, this + package) are each audited with separate inputs and outputs. Their + ownership and erasure contracts have not been joined. + - *First step:* feed #4208's produced mask and #4169's reverse-word keys + into this repair on one shared fixture. + - *Blocked by:* the full `E(p,ell)` evaluator from CRT data (#4192's + follow-up). +2. **Check multi-target density exactly.** + - *Why it matters:* the `r`-target bound is a union bound over targets + with disjoint guards. + - *First step:* enumerate a two-target fixture (`positions=(0,6)`, 12 `y` + bits) through the same repair. + - *Blocked by:* nothing; it costs `2^20` records. + +## Credit + +The construction and audited claims are Cinna Davis's #4100 (OpenAI Codex +assistance). The repair mechanism (extraction, keys, two-bucket radix passes, +keyed reinsertion) is jmbarrancoml's PR2250, building on Douglas Colkitt's +compact-control construction. kumagi's #4169 supplies the reverse-word keys, +and ToikY's #4201/#4208 the hole mask. This independent tariff audit was +prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) +assistance. Apache-2.0. diff --git a/research/pr4100-crt-repair-tariff/SOURCES.json b/research/pr4100-crt-repair-tariff/SOURCES.json new file mode 100644 index 0000000000..4832983b91 --- /dev/null +++ b/research/pr4100-crt-repair-tariff/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/selected-complex-compact-adapters/PROOF.md", + "usage": "input", + "git_blob": "685efc529493e4b841c1ce8799d28968b4991d7e", + "sha256": "804446e22304540eb02a5f4da3f71464a217be830a33b11420ea31eea878782c" + }, + { + "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" + } + ] +} diff --git a/research/pr4100-crt-repair-tariff/TASK.json b/research/pr4100-crt-repair-tariff/TASK.json new file mode 100644 index 0000000000..38479b6436 --- /dev/null +++ b/research/pr4100-crt-repair-tariff/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": "Audit the fixed-tape tariff of #4100 CRT.md section 4's sparse exception repair (extraction from the hole mask, TS^-1 keys at holes, two-bucket radix sort, keyed reinsertion, erasure) at Theta(p)-bit records, with exact absorption at #4100's G, B, K.", + "scope_change_reason": "The card asks for one quantified implication at its caller; this is the repair-cost implication CRT.md states, which every open CRT audit excludes and whose PR2250 predecessor tariff does not transfer to Theta(p)-bit records.", + "bottleneck_link": "If the repair cost per color were not O(V), the batched CRT row (power 1-a2+2(1-epsilon)) and hence #4100's proposed exponent would fail.", + "budget_minutes": 75, + "stop_rule": "Stop once dense and sparse repair costs are bounded with explicit constants, absorbed at #4100's parameters, and matched by literal tape counts with failing controls.", + "outcome": "completed", + "evidence": "README accounting: dense <= 9MR+5M, sorted holes <= N(L+R)(9L+6), counter <= 8M+4LN+4L; exact absorption 2^-640 (p=16) to 2^-37326 (p=2^64) of V; verify.py on #4100's compact/good fixture (5 fixtures, M up to 65,536): repair realizes T on every record, keys only at holes, dense <= 7.23 MR, sorted ~9.3-9.5 L(L+R) per hole; controls: full sort 262 MR, keys S^-1 misplace 5,888 records undetected by the key check, no repair leaves 2,048 wrong.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, accounting proof, simulator implementation and writing; no independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Compose the guard-scan hole mask, the TS^-1 key evaluator and this repair as one fixed-tape program.", + "why_it_matters": "#4201/#4208, #4192/#4169 and this package are audited with separate input/output contracts; ownership and erasure across them are not joined.", + "first_step": "Feed #4208's produced mask and #4169's reverse-word keys into this repair on one shared fixture.", + "blocked_by": "The full E(p,ell) evaluator from CRT data (#4192 follow-up)." + }, + { + "question": "Check the r-target bad density exactly on a multi-target fixture.", + "why_it_matters": "CRT.md's r-target density is a union bound over targets with disjoint guards; only r=1 is enumerated here.", + "first_step": "Enumerate the two-target fixture (positions (0,6), 12 y bits) through the same repair.", + "blocked_by": "None; 2^20 records." + } + ] +} diff --git a/research/pr4100-crt-repair-tariff/VERIFY.json b/research/pr4100-crt-repair-tariff/VERIFY.json new file mode 100644 index 0000000000..958d7aaeac --- /dev/null +++ b/research/pr4100-crt-repair-tariff/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/selected-complex-compact-adapters/PROOF.md", + "research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/check_batched_crt.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Source pins and 9 phrases (CRT.md, PR2250 PROOF.md); repair on tapes around #4100's compact/good fixture against the ideal switch; dense/sparse/counter moves against the written bounds; exact density and absorption at #4100's parameters; controls for a full-input sort, keys without T, and no repair." + } + ] +} diff --git a/research/pr4100-crt-repair-tariff/verify.py b/research/pr4100-crt-repair-tariff/verify.py new file mode 100644 index 0000000000..bb34cfb116 --- /dev/null +++ b/research/pr4100-crt-repair-tariff/verify.py @@ -0,0 +1,351 @@ +#!/usr/bin/env python3 +"""Fixed-tape tariff of #4100 CRT.md section 4's sparse exception repair. + +Standard library only. The actual macro S and the ideal switch T come from +#4100's own pinned check_batched_crt.py (compact, good). The repair runs on +explicit tapes, and every head move is counted, split into dense and sparse +parts: + +- one split scan driven by the guard scan's hole mask; +- keys T(S^-1(x)) only at holes; +- two-bucket stable LSD radix passes over the keyed holes; +- one reinsertion scan comparing keys only at holes, then erasure. + +Key evaluations are counted separately; their E(p,ell) cost is CRT.md's +premise. Finite corroboration of the written accounting in README.md, not an +all-size proof. Ryanson Jonathan with Claude Code (Claude Opus 5.5) +assistance. Apache-2.0. +""" +from fractions import Fraction +import hashlib +import importlib.util +import json +import math +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parents[2] +SOURCE = ROOT / "research/unconditional-batched-crt" + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +PHRASES = [ + "from both ends of each K-bit guard. Its bad density is at most", + " r [2/B + 8B/2^K] <= C p 2^-G.", + "T(S^-1(x)), sort those holes by this full key on fixed tapes, and merge them", + "cost explicitly increased to E(p,ell). It does not sort the full input.", + " 2^-G E(p,ell) <= C 2^(-60 ell) (p+2)^(-48),", + "bad-key evaluation, O(p)-bit keys, radix passes, counters and clearing all", + "the E(p,ell) computation. Reinsertion reads the one-bit hole stream and", + " G=64(ell+ceil(log2(p+2))), B=2^G, K=64G,", +] +PR2250_PHRASE = " O(V + M A^3 + delta M A(R+A))." + + +def check_sources(): + pins = {row["path"]: row["sha256"] + for row in json.loads((Path(__file__).parent / "SOURCES.json").read_text())["files"]} + for rel in ("research/unconditional-batched-crt/CRT.md", + "research/unconditional-batched-crt/check_batched_crt.py", + "research/selected-complex-compact-adapters/PROOF.md"): + need(hashlib.sha256((ROOT / rel).read_bytes()).hexdigest() == pins[rel], f"pin {rel}") + text = (SOURCE / "CRT.md").read_text() + for phrase in PHRASES: + need(phrase in text, f"CRT.md phrase missing: {phrase}") + need(PR2250_PHRASE in (ROOT / "research/selected-complex-compact-adapters/PROOF.md").read_text(), + "PR2250 repair tariff phrase") + spec = importlib.util.spec_from_file_location("pr4100_crt", SOURCE / "check_batched_crt.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module, len(PHRASES) + 1 + + +class Tape: + def __init__(self, width=1): + self.cells, self.pos, self.moves, self.end, self.w = [], 0, 0, 0, width + + def goto(self, i): + self.moves += abs(i - self.pos) * self.w + self.pos = i + + def read(self): + need(self.pos < self.end, "read past the end marker") + v = self.cells[self.pos] + self.pos += 1 + self.moves += self.w + return v + + def write(self, v): + if self.pos < len(self.cells): + self.cells[self.pos] = v + else: + self.cells.append(v) + self.pos += 1 + self.moves += self.w + self.end = max(self.end, self.pos) + + def truncate(self): + self.end = self.pos + + def erase(self): + """Blank the written region (one sweep) and return to its origin.""" + self.goto(self.end) + self.goto(0) + self.moves += self.end * self.w + self.end = 0 + + +class Counter: + """L-bit binary address counter; head rests on the low end.""" + + def __init__(self, L): + self.bits, self.moves, self.L = [0] * L, 0, L + + def increment(self): + i = 0 + while i < self.L and self.bits[i]: + self.bits[i] = 0 + i += 1 + if i < self.L: + self.bits[i] = 1 + self.moves += 2 * (i + 1) + + def value(self): + self.moves += 2 * self.L # read every bit and return + return sum(b << i for i, b in enumerate(self.bits)) + + def reset(self): + self.bits = [0] * self.L + self.moves += 2 * self.L + + +def fixture(crt, bits, cb, yb, guard, fn): + L = 2 * cb + yb + M = 1 << L + + def split(q): + return q >> (cb + yb), (q >> yb) & ((1 << cb) - 1), q & ((1 << yb) - 1) + + def join(u, t, y): + return (u << (cb + yb)) | (t << yb) | y + + S, T, good = [0] * M, [0] * M, [False] * M + for q in range(M): + u, t, y = split(q) + S[q] = join(*crt.compact(u, t, y, fn, bits=bits, positions=(0,), ybits=yb, control_bits=cb)) + T[q] = join(u, t, y ^ fn(y)[0]) + good[q] = crt.good(u, t, y, bits=bits, positions=(0,), guard=guard) + need(sorted(S) == list(range(M)) and sorted(T) == list(range(M)), "S and T are bijections") + for q in range(M): + need(good[S[q]] == good[q] and good[T[q]] == good[q], "S and T preserve the good set") + if good[q]: + need(S[q] == T[q], "S agrees with T on good addresses") + inv_S = [0] * M + for q in range(M): + inv_S[S[q]] = q + return L, M, S, T, good, inv_S + + +def repair(L, M, R, S, T, good, inv_S, *, key_mode="TS^-1", full_sort=False): + """After the macro, the record from q sits at S(q). Return the final layout and the meters.""" + DATA, GOOD, BAD, B = Tape(R), Tape(R), Tape(L + R), [Tape(L + R), Tape(L + R)] + MASK = Tape(1) + ctr = Counter(L) + for x in range(M): + DATA.write(inv_S[x]) # record id = original address + MASK.write(0 if good[x] else 1) # the guard scan's owned hole mask (#4201) + DATA.truncate(); MASK.truncate(); DATA.goto(0); MASK.goto(0) + DATA.moves = MASK.moves = 0 + evaluations = 0 + + def key_of(x): + if key_mode == "TS^-1": + return T[inv_S[x]] + if key_mode == "S^-1": # control: forget the ideal map + return inv_S[x] + raise ValueError(key_mode) + + # Split scan: good records to GOOD; holes get their address, key and record on BAD. + for x in range(M): + hole = MASK.read() + rec = DATA.read() + sorted_here = full_sort or hole + if sorted_here: + addr = ctr.value() + need(addr == x, "counter tracks the current address") + evaluations += 1 + BAD.write((key_of(x), rec)) + else: + GOOD.write(rec) + ctr.increment() + BAD.truncate(); GOOD.truncate() + n_sorted = BAD.end + # Two-bucket stable LSD radix passes on the L-bit keys. + for j in range(L): + BAD.goto(0) + for _ in range(n_sorted): + key, rec = BAD.read() + B[(key >> j) & 1].write((key, rec)) + for b in B: + b.truncate() + BAD.goto(0) + for b in B: + b.goto(0) + for _ in range(b.end): + BAD.write(b.read()) + b.erase() + BAD.truncate() + BAD.goto(0) + # Reinsertion: output overwrites DATA from cell 0; keys compared only at holes. + MASK.goto(0); GOOD.goto(0); DATA.goto(0) + ctr.reset() + for x in range(M): + hole = MASK.read() + if full_sort: + key, rec = BAD.read() + elif hole: + key, rec = BAD.read() + addr = ctr.value() + need(key == addr, "sorted key equals the current hole address") + else: + rec = GOOD.read() + DATA.write(rec) + ctr.increment() + for tape in (GOOD, BAD, MASK): + tape.erase() + DATA.goto(0) + layout = DATA.cells[:M] + dense = DATA.moves + GOOD.moves + MASK.moves + sparse = BAD.moves + B[0].moves + B[1].moves + return layout, dict(dense=dense, sparse=sparse, counter=ctr.moves, evaluations=evaluations, + n_sorted=n_sorted) + + +def written_bounds(L, M, R, nbad): + """README accounting, in cells. + + Dense: DATA read, rewind, write, rewind (4MR); GOOD write, rewind, read and + two-sweep erase (5MR at most); MASK read, rewind, read and erase (5M). + Sorted holes: one keyed write, then per radix pass nine sweeps (read, + bucket write, two rewinds, bucket read, concatenation write, two-sweep + erase, next rewind), plus reinsertion read and erase: (L+R)(9L+6) per hole. + Counter: two amortized scans (8M), address reads at holes in both scans + (4L each), and a reset.""" + dense = 9 * M * R + 5 * M + sparse = nbad * (L + R) * (9 * L + 6) + counter = 8 * M + 4 * L * nbad + 4 * L + return dense, sparse, counter + + +FN = { + "bit2": lambda y: ((y >> 2) & 1,), + "parity": lambda y: ((y >> 1).bit_count() & 1,), + "and14": lambda y: (((y >> 1) & 1) & ((y >> 4) & 1),), +} +FIXTURES = [ # bits, control bits, y bits, guard, source function + (2, 2, 6, 6, "bit2"), + (2, 4, 6, 6, "parity"), + (3, 3, 8, 8, "and14"), + (3, 4, 8, 8, "parity"), + (4, 4, 8, 8, "bit2"), +] + + +def check_repairs(crt): + rows = [] + for bits, cb, yb, guard, name in FIXTURES: + L, M, S, T, good, inv_S = fixture(crt, bits, cb, yb, guard, FN[name]) + R = L # records and keys both Theta(p) + nbad = M - sum(good) + B = 1 << bits + need(Fraction(nbad, M) <= Fraction(2, B) + Fraction(8 * B, 1 << guard), "density <= 2/B + 8B/2^K") + layout, meter = repair(L, M, R, S, T, good, inv_S) + need(all(layout[T[q]] == q for q in range(M)), "repair realizes T on every record") + need(meter["evaluations"] == nbad, "keys evaluated only at holes") + dense_b, sparse_b, counter_b = written_bounds(L, M, R, nbad) + need(meter["dense"] <= dense_b, f"dense within bound {bits},{cb},{yb}") + need(meter["sparse"] <= sparse_b, f"sorted part within bound {bits},{cb},{yb}: {meter['sparse']} > {sparse_b}") + need(meter["counter"] <= counter_b, "counter within bound") + rows.append(dict(bits=bits, control_bits=cb, ybits=yb, guard=guard, source=name, L=L, M=M, + holes=nbad, density=round(nbad / M, 4), + density_bound=round(2 / B + 8 * B / 2 ** guard, 4), + dense_per_MR=round(meter["dense"] / (M * R), 3), + sparse_per_hole_LR=round(meter["sparse"] / max(1, nbad * L * (L + R)), 3), + sparse_per_MR=round(meter["sparse"] / (M * R), 3))) + return rows + + +def check_controls(crt): + bits, cb, yb, guard, name = FIXTURES[1] + L, M, S, T, good, inv_S = fixture(crt, bits, cb, yb, guard, FN[name]) + R = L + nbad = M - sum(good) + out = {} + # Keys S^-1(x) still permute the bad set (S preserves it), so the reinsertion + # key check passes; the layout is wrong because the holes skip T. + wrong_layout, _ = repair(L, M, R, S, T, good, inv_S, key_mode="S^-1") + out["key_without_T_wrong_records"] = sum(wrong_layout[T[q]] != q for q in range(M)) + need(out["key_without_T_wrong_records"] > 0, "control: keys S^-1(x) misplace hole records") + layout = [inv_S[x] for x in range(M)] # no repair at all + out["no_repair_wrong_records"] = sum(layout[T[q]] != q for q in range(M)) + need(out["no_repair_wrong_records"] > 0, "control: skipping repair leaves holes wrong") + full_layout, full = repair(L, M, R, S, T, good, inv_S, full_sort=True) + need(all(full_layout[T[q]] == q for q in range(M)), "full sort is also correct") + _, sparse_meter = repair(L, M, R, S, T, good, inv_S) + out["full_sort_evaluations"] = full["evaluations"] + out["sparse_evaluations"] = sparse_meter["evaluations"] + out["full_sort_per_MR"] = round(full["sparse"] / (M * R), 2) + # The full-input sort moves Theta(L) records' worth per record: not O(V). + need(full["sparse"] / (M * R) > 8 * L * 0.9, "control: sorting the full input costs Theta(L) V") + return out + + +def check_absorption(): + """At #4100's parameters, with L <= p and R >= p/8 (Theta(p) records and addresses): + sorted/V <= delta(1+L/R)(9L+6) and hole counter reads/V <= delta 4L/R, delta <= r(2/B+8B/2^K), r <= L/(100G).""" + rows = [] + for k in (4, 8, 16, 32, 64): + p = 1 << k + lg = (p + 1).bit_length() # exact ceil(log2(p+2)); floats round 2^64+2 down + for ell in (lg, 2 * lg, 8 * lg): # eventually ell >= ceil(log2(p+2)) + G = 64 * (ell + lg) + B, K = 1 << G, 64 * G + L, R = p, Fraction(p, 8) + r = Fraction(L, 100 * G) + delta = r * (Fraction(2, B) + Fraction(8 * B, 1 << K)) + sorted_over_V = delta * (1 + L / R) * (9 * L + 6) + counter_over_V = delta * 4 * L / R + need(sorted_over_V + counter_over_V < Fraction(1, 2 ** 64), "sparse repair is o(V) with huge margin") + # CRT.md's E line: 2^-G * 2^(4 ell) (p+2)^16 <= 2^(-60 ell) (p+2)^(-48). + lhs = Fraction(1 << (4 * ell), 1 << G) * (p + 2) ** 16 + rhs = Fraction(1, 1 << (60 * ell)) / (p + 2) ** 48 + need(lhs <= rhs, "2^-G E-envelope inequality") + total = sorted_over_V + counter_over_V + rows.append(dict(p=p, ell=ell, log2_sparse_over_V=round(math.log2(total.numerator) - math.log2(total.denominator), 1))) + return rows + + +def main(): + crt, phrases = check_sources() + rows = check_repairs(crt) + controls = check_controls(crt) + absorption = check_absorption() + print(json.dumps({ + "status": "PASS_PR4100_CRT_REPAIR_TARIFF_FINITE", + "source_phrases": phrases, + "fixtures": rows, + "controls": controls, + "absorption": absorption, + "max_dense_per_MR": max(r["dense_per_MR"] for r in rows), + "max_sparse_per_hole_LR": max(r["sparse_per_hole_LR"] for r in rows), + "all_size_theorem_claimed": False, + "new_kappa_claimed": False, + }, indent=1)) + + +if __name__ == "__main__": + sys.exit(main()) From 6cb983cc1832fac344a6627cc22d78363a33b82d Mon Sep 17 00:00:00 2001 From: Ryanson Jonathan Date: Wed, 21 Oct 2026 16:24:49 +0700 Subject: [PATCH 2/3] Check the CRT repair exactly on all 2^20 two-target addresses Exact r-target bad density 1-[(1-1/B)^2(1-8B/2^K)]^r from disjoint fields (implies CRT.md's union bound), verified exactly on every one-target fixture and on all 2^20 addresses of #4100's two-target layout for two sources. The repair, run by a sweep-level implementation cross-checked against the per-cell one, realizes the two-target switch on every record within the written bounds. A source reading the other active target breaks S = T on 55,296 good addresses (premise control). Co-Authored-By: Claude Opus 5.5 --- research/pr4100-crt-repair-tariff/README.md | 63 +++++-- research/pr4100-crt-repair-tariff/TASK.json | 10 +- research/pr4100-crt-repair-tariff/VERIFY.json | 4 +- research/pr4100-crt-repair-tariff/verify.py | 174 +++++++++++++++++- 4 files changed, 224 insertions(+), 27 deletions(-) diff --git a/research/pr4100-crt-repair-tariff/README.md b/research/pr4100-crt-repair-tariff/README.md index f08dd8e5b9..0de038db96 100644 --- a/research/pr4100-crt-repair-tariff/README.md +++ b/research/pr4100-crt-repair-tariff/README.md @@ -76,8 +76,17 @@ word, composed with `T`. **5. Absorption at #4100's parameters.** CRT.md sets `G = 64(ell + ⌈log₂(p+2)⌉)`, `B = 2^G`, `K = 64G` and `r ≤ L/(100G)`. -The bad density is `δ ≤ r(2/B + 8B/2^K)`, which the fixtures check exactly -at `r = 1`. +The bad density is `δ ≤ r(2/B + 8B/2^K)`. + +**Exact `r`-target density.** The `r` active targets use distinct `u` and `t` +digits and pairwise disjoint guard windows. On a complete enumeration these +fields are independent, so the good events are independent and + +`δ_r = 1 − [(1−1/B)²(1 − 8B/2^K)]^r` + +holds *exactly*. CRT.md's bound follows from `1 − Π(1−x_i) ≤ Σ x_i`. The +fixtures check the identity exactly at `r = 1` (all five) and at `r = 2` +(all `2^20` addresses, below). - **Sparse moves:** `δ(1+L/R)(9L+6) + δ·4L/R`. Since `2^-G ≤ 2^-64ell (p+2)^-64`, this is below `p³(p+2)^-64` for `L ≤ p` and @@ -89,7 +98,7 @@ at `r = 1`. ## Evidence -`verify.py` uses only the standard library and takes about 6 seconds. +`verify.py` uses only the standard library and takes about 45 seconds. - **Fixtures.** The macro `S` and the ideal switch `T` come from #4100's pinned `check_batched_crt.py` (`compact`, `good`). There are five fixtures, @@ -98,7 +107,11 @@ at `r = 1`. - **Correctness.** Each fixture checks that `S` and `T` are bijections, that both preserve the good set, and that `S = T` on good addresses. The repair then realizes `T` on every record. -- **Density.** The measured density never exceeds `2/B + 8B/2^K`. +- **Density.** Every measured density equals the product formula exactly, + and therefore never exceeds `2/B + 8B/2^K`. +- **Sweep-level repair.** A second implementation charges whole sweeps instead + of single cells. It matches the per-cell repair exactly (meters and layout) + on all five fixtures, and it runs the `2^20` case. | `B`, guard, `M` | Holes | Dense / `MR` | Sorted / (holes·`L(L+R)`) | | --- | --- | --- | --- | @@ -110,6 +123,28 @@ at `r = 1`. Toy `B` makes holes dense here. At #4100's `G`, `δ ≈ 2^-G` (item 5). +**Two targets, every address.** The layout is #4100's own two-target layout: +`positions=(0,6)`, `B = 4`, guard 6, 4-bit control fields, 12 `y` bits, so +`M = 2^20`. Two sources were run: #4100's own `source_pair`, and a second pair +that reads guard bits of both targets. Each omits both active targets. + +| Source | Holes | Density | Union bound | Dense / `MR` | Sorted / (holes·`L(L+R)`) | Keys without `T`: wrong records | +| --- | --- | --- | --- | --- | --- | --- | +| `source_pair` | 965,632 | 943/1024 (exact) | 2 | 4.65 | 9.25 | 724,224 | +| `mixed_pair` | 965,632 | 943/1024 (exact) | 2 | 4.65 | 9.25 | 603,520 | + +In both cases `S` and `T` are bijections, both preserve the good set, +`S = T` on good addresses, and the repair realizes the two-target switch on +all 1,048,576 records. At toy `B` the union bound exceeds 1, so the exact +identity is what is checked here. + +**Two-target premise control.** Take a source that reads the *other* active +target: `f_0` reads bit 6. Then `S ≠ T` on 55,296 good addresses, and `S` no +longer preserves the good set. The repair's premise, that both maps preserve +the bad set, fails, and a sparse repair cannot correct good-address errors. +CRT.md requires "all f_i omit the target set"; this is the two-target +counterpart of #4169's counterexample. + **Controls,** each of which must fail: - **Full-input sort.** It evaluates 16,384 keys, not 11,776, and moves 262·`MR`, which is `Θ(L)·V`. This is why CRT.md avoids it. @@ -126,8 +161,9 @@ PR2250's PROOF.md, with 9 exact phrases. - The guard scan that produces the hole mask (#4201, #4208). - The macro `S`'s ordinary interchanges, the last-`K` branch (#4187), and reservoir placement (#4174). -- The fixtures have one target. CRT.md's `r`-target density is the union - bound, checked here only at `r = 1`. +- `r ≥ 3` is not enumerated: `r` targets need `2^(8r+4)` addresses at + `B = 4`. The exact `r`-target formula rests on the field-disjointness + argument above. - There is no proof-kernel check. ## Reproduce @@ -151,12 +187,15 @@ The verifier prints `PASS_PR4100_CRT_REPAIR_TARIFF_FINITE`. into this repair on one shared fixture. - *Blocked by:* the full `E(p,ell)` evaluator from CRT data (#4192's follow-up). -2. **Check multi-target density exactly.** - - *Why it matters:* the `r`-target bound is a union bound over targets - with disjoint guards. - - *First step:* enumerate a two-target fixture (`positions=(0,6)`, 12 `y` - bits) through the same repair. - - *Blocked by:* nothing; it costs `2^20` records. +2. **Bind disjoint guard windows at the actual coloring.** (Done for + `r = 2`; the earlier question 2 is closed above.) + - *Why it matters:* the exact formula needs every active target's `K-1` + guard window to be disjoint from every other window and from every + active target. CRT.md colors targets by position mod `K` for this. + - *First step:* check that coloring mod `K` with `(K−1)`-bit windows gives + disjointness for the actual mixed `ell`/`ell−1` axis offsets of #4174's + descriptors. + - *Blocked by:* nothing. ## Credit diff --git a/research/pr4100-crt-repair-tariff/TASK.json b/research/pr4100-crt-repair-tariff/TASK.json index 38479b6436..abca18f92c 100644 --- a/research/pr4100-crt-repair-tariff/TASK.json +++ b/research/pr4100-crt-repair-tariff/TASK.json @@ -60,7 +60,7 @@ "budget_minutes": 75, "stop_rule": "Stop once dense and sparse repair costs are bounded with explicit constants, absorbed at #4100's parameters, and matched by literal tape counts with failing controls.", "outcome": "completed", - "evidence": "README accounting: dense <= 9MR+5M, sorted holes <= N(L+R)(9L+6), counter <= 8M+4LN+4L; exact absorption 2^-640 (p=16) to 2^-37326 (p=2^64) of V; verify.py on #4100's compact/good fixture (5 fixtures, M up to 65,536): repair realizes T on every record, keys only at holes, dense <= 7.23 MR, sorted ~9.3-9.5 L(L+R) per hole; controls: full sort 262 MR, keys S^-1 misplace 5,888 records undetected by the key check, no repair leaves 2,048 wrong.", + "evidence": "README accounting: dense <= 9MR+5M, sorted holes <= N(L+R)(9L+6), counter <= 8M+4LN+4L; exact r-target density 1-[(1-1/B)^2(1-8B/2^K)]^r; exact absorption 2^-640 (p=16) to 2^-37326 (p=2^64) of V. verify.py on #4100's compact/good: 5 one-target fixtures (M up to 65,536) plus every one of 2^20 two-target addresses for two sources; densities equal the product formula exactly (943/1024 at r=2); repair realizes T on every record; sweep-level repair matches per-cell repair exactly; controls: full sort 262 MR, keys without T misplace records (5,888; 724,224; 603,520) undetected by the key check, no repair leaves 2,048 wrong, a source reading the other active target breaks S=T on 55,296 good addresses.", "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, accounting proof, simulator implementation and writing; no independent human or proof-kernel review.", "open_questions": [ @@ -71,10 +71,10 @@ "blocked_by": "The full E(p,ell) evaluator from CRT data (#4192 follow-up)." }, { - "question": "Check the r-target bad density exactly on a multi-target fixture.", - "why_it_matters": "CRT.md's r-target density is a union bound over targets with disjoint guards; only r=1 is enumerated here.", - "first_step": "Enumerate the two-target fixture (positions (0,6), 12 y bits) through the same repair.", - "blocked_by": "None; 2^20 records." + "question": "Bind disjoint guard windows at the actual position-mod-K coloring and mixed ell/ell-1 axis offsets.", + "why_it_matters": "The exact r-target density (and the union bound) needs every active guard window disjoint from the others and from active targets.", + "first_step": "Check coloring mod K with (K-1)-bit windows against #4174's actual split-axis descriptors.", + "blocked_by": "None." } ] } diff --git a/research/pr4100-crt-repair-tariff/VERIFY.json b/research/pr4100-crt-repair-tariff/VERIFY.json index 958d7aaeac..4e6e639937 100644 --- a/research/pr4100-crt-repair-tariff/VERIFY.json +++ b/research/pr4100-crt-repair-tariff/VERIFY.json @@ -15,8 +15,8 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 300, - "checks": "Source pins and 9 phrases (CRT.md, PR2250 PROOF.md); repair on tapes around #4100's compact/good fixture against the ideal switch; dense/sparse/counter moves against the written bounds; exact density and absorption at #4100's parameters; controls for a full-input sort, keys without T, and no repair." + "timeout_seconds": 600, + "checks": "Source pins and 9 phrases (CRT.md, PR2250 PROOF.md); repair on tapes around #4100's compact/good fixture against the ideal switch; dense/sparse/counter moves against the written bounds; exact density and absorption at #4100's parameters; controls for a full-input sort, keys without T, and no repair; exact r-target density formula on one-target fixtures and on all 2^20 two-target addresses; sweep-level repair cross-checked against the per-cell repair; two-target premise control." } ] } diff --git a/research/pr4100-crt-repair-tariff/verify.py b/research/pr4100-crt-repair-tariff/verify.py index bb34cfb116..83485db97c 100644 --- a/research/pr4100-crt-repair-tariff/verify.py +++ b/research/pr4100-crt-repair-tariff/verify.py @@ -123,7 +123,9 @@ def reset(self): self.moves += 2 * self.L -def fixture(crt, bits, cb, yb, guard, fn): +def fixture(crt, bits, cb, yb, guard, fn, positions=(0,), strict=True): + """Enumerate every address (u, t, y). With strict=False, return the number of good + addresses where the macro disagrees with the ideal switch instead of failing.""" L = 2 * cb + yb M = 1 << L @@ -136,18 +138,34 @@ def join(u, t, y): S, T, good = [0] * M, [0] * M, [False] * M for q in range(M): u, t, y = split(q) - S[q] = join(*crt.compact(u, t, y, fn, bits=bits, positions=(0,), ybits=yb, control_bits=cb)) - T[q] = join(u, t, y ^ fn(y)[0]) - good[q] = crt.good(u, t, y, bits=bits, positions=(0,), guard=guard) + S[q] = join(*crt.compact(u, t, y, fn, bits=bits, positions=positions, ybits=yb, control_bits=cb)) + flips = sum(f << pos for f, pos in zip(fn(y), positions)) + T[q] = join(u, t, y ^ flips) + good[q] = crt.good(u, t, y, bits=bits, positions=positions, guard=guard) need(sorted(S) == list(range(M)) and sorted(T) == list(range(M)), "S and T are bijections") + disagreements = 0 for q in range(M): - need(good[S[q]] == good[q] and good[T[q]] == good[q], "S and T preserve the good set") - if good[q]: - need(S[q] == T[q], "S agrees with T on good addresses") + need(good[T[q]] == good[q], "T preserves the good set") + if strict: + need(good[S[q]] == good[q], "S preserves the good set") + if good[q] and S[q] != T[q]: + disagreements += 1 + if strict: + need(disagreements == 0, "S agrees with T on good addresses") inv_S = [0] * M for q in range(M): inv_S[S[q]] = q - return L, M, S, T, good, inv_S + if strict: + return L, M, S, T, good, inv_S + return L, M, S, T, good, inv_S, disagreements + + +def exact_bad_fraction(bits, guard, r): + """Complete enumeration, r targets on disjoint digits and disjoint guard windows: + the good events are independent, so delta_r = 1 - [(1-1/B)^2 (1-8B/2^K)]^r exactly.""" + B = 1 << bits + per_target_good = (1 - Fraction(1, B)) ** 2 * (1 - Fraction(8 * B, 1 << guard)) + return 1 - per_target_good ** r def repair(L, M, R, S, T, good, inv_S, *, key_mode="TS^-1", full_sort=False): @@ -225,6 +243,91 @@ def key_of(x): n_sorted=n_sorted) +class SweepTape: + """The Tape above, charged per sweep instead of per cell (same head semantics).""" + + def __init__(self, width=1): + self.pos, self.moves, self.end, self.w = 0, 0, 0, width + + def goto(self, i): + self.moves += abs(i - self.pos) * self.w + self.pos = i + + def sweep(self, n, writing=False): + if not writing: + need(self.pos + n <= self.end, "read past the end marker") + self.pos += n + self.moves += n * self.w + if writing: + self.end = max(self.end, self.pos) + + def truncate(self): + self.end = self.pos + + def erase(self): + self.goto(self.end) + self.goto(0) + self.moves += self.end * self.w + self.end = 0 + + +def counter_scan_cost(L, M): + """Head moves of M increments of the L-bit counter from zero: 2(trailing ones + 1) each.""" + return sum(2 * (min(L, (x ^ (x + 1)).bit_length() - 1) + 1) for x in range(M)) + + +def repair_bulk(L, M, R, S, T, good, inv_S, *, key_mode="TS^-1"): + """repair() with sweep-level charging, for M = 2^20; data moves as Python lists.""" + DATA, GOOD, BAD = SweepTape(R), SweepTape(R), SweepTape(L + R) + BK, MASK = [SweepTape(L + R), SweepTape(L + R)], SweepTape(1) + DATA.end, MASK.end = M, M + holes = [not g for g in good] + nbad = sum(holes) + key_of = (lambda x: T[inv_S[x]]) if key_mode == "TS^-1" else (lambda x: inv_S[x]) + inc = counter_scan_cost(L, M) + counter = 0 + # Split scan. + MASK.sweep(M); DATA.sweep(M) + good_list = [inv_S[x] for x in range(M) if not holes[x]] + bad_list = [(key_of(x), inv_S[x]) for x in range(M) if holes[x]] + GOOD.sweep(len(good_list), writing=True); BAD.sweep(nbad, writing=True) + counter += inc + 2 * L * nbad + BAD.truncate(); GOOD.truncate() + # Radix passes. + for j in range(L): + BAD.goto(0); BAD.sweep(nbad) + zeros = [kr for kr in bad_list if not (kr[0] >> j) & 1] + ones = [kr for kr in bad_list if (kr[0] >> j) & 1] + BK[0].sweep(len(zeros), writing=True); BK[1].sweep(len(ones), writing=True) + for b in BK: + b.truncate() + BAD.goto(0) + for b, part in zip(BK, (zeros, ones)): + b.goto(0); b.sweep(len(part)); BAD.sweep(len(part), writing=True); b.erase() + BAD.truncate() + bad_list = zeros + ones + BAD.goto(0) + # Reinsertion. + MASK.goto(0); GOOD.goto(0); DATA.goto(0) + counter += 2 * L + layout, gi, bi = [], iter(good_list), iter(bad_list) + for x in range(M): + if holes[x]: + key, rec = next(bi) + need(key == x, "sorted key equals the current hole address") + else: + rec = next(gi) + layout.append(rec) + MASK.sweep(M); BAD.sweep(nbad); GOOD.sweep(M - nbad); DATA.sweep(M, writing=True) + counter += inc + 2 * L * nbad + for tape in (GOOD, BAD, MASK): + tape.erase() + DATA.goto(0) + dense = DATA.moves + GOOD.moves + MASK.moves + sparse = BAD.moves + BK[0].moves + BK[1].moves + return layout, dict(dense=dense, sparse=sparse, counter=counter, evaluations=nbad, n_sorted=nbad) + + def written_bounds(L, M, R, nbad): """README accounting, in cells. @@ -262,8 +365,11 @@ def check_repairs(crt): R = L # records and keys both Theta(p) nbad = M - sum(good) B = 1 << bits + need(Fraction(nbad, M) == exact_bad_fraction(bits, guard, 1), "density equals the exact product formula") need(Fraction(nbad, M) <= Fraction(2, B) + Fraction(8 * B, 1 << guard), "density <= 2/B + 8B/2^K") layout, meter = repair(L, M, R, S, T, good, inv_S) + bulk_layout, bulk_meter = repair_bulk(L, M, R, S, T, good, inv_S) + need(bulk_layout == layout and bulk_meter == meter, "sweep-level repair matches the per-cell repair exactly") need(all(layout[T[q]] == q for q in range(M)), "repair realizes T on every record") need(meter["evaluations"] == nbad, "keys evaluated only at holes") dense_b, sparse_b, counter_b = written_bounds(L, M, R, nbad) @@ -329,17 +435,69 @@ def check_absorption(): return rows +TWO_TARGET_FN = { + "source_pair": lambda y: ((y >> 3) & 1, (y & ~65).bit_count() & 1), # #4100's own two-target source + "mixed_pair": lambda y: (((y >> 1) & 1) ^ ((y >> 11) & 1), ((y >> 5) & 1) & ((y >> 8) & 1)), +} + + +def check_two_target(crt): + """Every one of the 2^20 addresses of #4100's two-target layout: positions (0, 6), B = 4, + guard K = 6, 4-bit control fields, 12 y bits. Each source omits both active targets.""" + bits, cb, yb, guard, positions = 2, 4, 12, 6, (0, 6) + B = 1 << bits + rows = [] + for name, fn in TWO_TARGET_FN.items(): + L, M, S, T, good, inv_S = fixture(crt, bits, cb, yb, guard, fn, positions=positions) + R = L + nbad = M - sum(good) + exact = exact_bad_fraction(bits, guard, 2) + need(Fraction(nbad, M) == exact, "two-target density equals the exact product formula") + union = 2 * (Fraction(2, B) + Fraction(8 * B, 1 << guard)) + need(exact <= union, "product formula implies the union bound") + layout, meter = repair_bulk(L, M, R, S, T, good, inv_S) + need(all(layout[T[q]] == q for q in range(M)), "repair realizes the two-target switch on every record") + dense_b, sparse_b, counter_b = written_bounds(L, M, R, nbad) + need(meter["dense"] <= dense_b and meter["sparse"] <= sparse_b and meter["counter"] <= counter_b, + "two-target meters within the written bounds") + wrong_layout, _ = repair_bulk(L, M, R, S, T, good, inv_S, key_mode="S^-1") + rows.append(dict(source=name, L=L, M=M, holes=nbad, density=str(Fraction(nbad, M)), + union_bound=str(union), + dense_per_MR=round(meter["dense"] / (M * R), 3), + sparse_per_hole_LR=round(meter["sparse"] / (nbad * L * (L + R)), 3), + key_without_T_wrong_records=sum(wrong_layout[T[q]] != q for q in range(M)))) + need(rows[-1]["key_without_T_wrong_records"] > 0, "control: keys without T misplace hole records") + # Premise control: a source that reads the other active target breaks agreement on good + # addresses, which the sparse repair never touches. + reads_other = lambda y: ((y >> 6) & 1, (y >> 1) & 1) + L, M, S, T, good, inv_S, disagreements = fixture(crt, bits, cb, yb, guard, reads_other, + positions=positions, strict=False) + need(disagreements > 0, "control: reading another active target breaks S = T on good addresses") + preserved = all(good[S[q]] == good[q] for q in range(M)) + control = dict(source_reads_other_target=True, good_addresses_where_S_differs_from_T=disagreements, + S_preserves_good_set=preserved) + if preserved: + layout, _ = repair_bulk(L, M, L, S, T, good, inv_S) + control["records_wrong_after_repair"] = sum(layout[T[q]] != q for q in range(M)) + need(control["records_wrong_after_repair"] > 0, "control: the repair cannot fix good-set disagreement") + return rows, control + + def main(): crt, phrases = check_sources() rows = check_repairs(crt) controls = check_controls(crt) absorption = check_absorption() + two_target, premise_control = check_two_target(crt) print(json.dumps({ "status": "PASS_PR4100_CRT_REPAIR_TARIFF_FINITE", "source_phrases": phrases, "fixtures": rows, "controls": controls, "absorption": absorption, + "two_target": two_target, + "two_target_premise_control": premise_control, + "sweep_repair_matches_per_cell": True, "max_dense_per_MR": max(r["dense_per_MR"] for r in rows), "max_sparse_per_hole_LR": max(r["sparse_per_hole_LR"] for r in rows), "all_size_theorem_claimed": False, From b3ea5ee525b131273d190747b892e5f3667d286f Mon Sep 17 00:00:00 2001 From: Ryanson Jonathan Date: Wed, 21 Oct 2026 16:25:48 +0700 Subject: [PATCH 3/3] Correct the r-target enumeration size in the CRT repair README Co-Authored-By: Claude Opus 5.5 --- research/pr4100-crt-repair-tariff/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/research/pr4100-crt-repair-tariff/README.md b/research/pr4100-crt-repair-tariff/README.md index 0de038db96..1eba912277 100644 --- a/research/pr4100-crt-repair-tariff/README.md +++ b/research/pr4100-crt-repair-tariff/README.md @@ -161,8 +161,8 @@ PR2250's PROOF.md, with 9 exact phrases. - The guard scan that produces the hole mask (#4201, #4208). - The macro `S`'s ordinary interchanges, the last-`K` branch (#4187), and reservoir placement (#4174). -- `r ≥ 3` is not enumerated: `r` targets need `2^(8r+4)` addresses at - `B = 4`. The exact `r`-target formula rests on the field-disjointness +- `r ≥ 3` is not enumerated: `r` targets need `2^(10r)` addresses at + `B = 4` (`4r` control bits and `6r` `y` bits). The exact `r`-target formula rests on the field-disjointness argument above. - There is no proof-kernel check.