Compare the sharp compact-switch window with CRT.md's repair room.

research/compact-switch-sharp-density/PROOF.md

@@ -0,0 +1,143 @@
+# Sharp-window density against the printed CRT repair room
+
+Scoped proof. No new κ. The selected conditional exponent is unchanged.
+This does not accept PR #4100, and it does not extend the simultaneous
+carry argument from the published `2B` margin to the sharp window.
+
+## Parameters
+
+CRT.md §3, for integers `ell ≥ 1` and `p ≥ 2`, sets
+
+```text
+G = 64 (ell + ceil(log2(p+2))),    B = 2^G,    K = 64 G.
+```
+
+A batch has `r` targets with `r ≤ floor(L / (100 G))`. The absorption
+hypothesis used below is the same one as PR #4328: `L ≤ p`. It is not
+proved here that every address layout satisfies `L ≤ p`. On this domain
+`G ≥ 192`.
+
+## Two window predicates
+
+A `K`-bit guard stores the target in its least bit and the window `W` in
+the other `m = K − 1` bits, so `W` is an integer in `0, …, 2^m − 1`.
+This is the layout in `check_batched_crt.py`: the published predicate is
+
+```text
+2B ≤ W < 2^m − 2B.
+```
+
+Whenever `4B ≤ 2^m`, exactly `4B` windows fail, and the fraction is
+
+```text
+4B / 2^m = 8B / 2^K.
+```
+
+That is the window summand in CRT.md §4.
+
+The isolated post-increment step, with digit `τ ≤ B − 2`, is the map
+
+```text
+y1 = y + 2 z τ,    τ' = τ + (y1 mod 2),    y2 = y1 + z (1 − 2 τ').
+```
+
+For `z = 1`, `τ = B − 2` and a zero target bit, direct expansion shows
+that `y1` first leaves the `m`-bit window at
+
+```text
+W = 2^m − (B − 2) = 2^m − B + 2.
+```
+
+Every smaller window, `0 ≤ W ≤ 2^m − B + 1`, returns `y2 = y + z(1−2b)`
+with the window restored and with no bit at position `m+1` or above.
+Thus the sharp bad set has size exactly `B − 2` (and size `0` when
+`B = 2`). Its fraction is
+
+```text
+β = (B − 2) / 2^m = 2(B − 2) / 2^K.
+```
+
+For `B > 2` and `4B ≤ 2^m`,
+
+```text
+β = ((B − 2) / (4B)) · (8B / 2^K) < (1/4) · (8B / 2^K).
+```
+
+Every published-good window is sharp-good: `2B ≤ W ≤ 2^m − 2B − 1`
+implies `W ≤ 2^m − B + 1` because `B ≥ 2`. The inclusion is proper
+whenever a window below `2B` exists.
+
+## What the substitution does not prove
+
+CRT.md uses the `2B` margin to keep simultaneous carries inside disjoint
+guards. The count above is for one isolated target. Replacing `8B/2^K`
+by `β` in the density line is valid for that isolated predicate. It does
+not by itself certify the simultaneous macro on the extra windows
+`W < 2B` or `2^m − 2B ≤ W ≤ 2^m − B + 1`.
+
+## Union bound
+
+Charge a target as bad when either control digit equals `B − 1` or its
+window is sharp-bad. The two digit failures contribute `2/B = 2^{1−G}`.
+For `r` targets,
+
+```text
+δ ≤ r (2/B + β) = r (2^{1−G} + 2(2^G − 2) 2^{−64G}).
+```
+
+Factor `2^{−G}`:
+
+```text
+2/B + β = 2^{−G} (2 + 2(1 − 2^{1−G}) 2^{−62G})
+        < 2^{−G} (2 + 2^{1−62G}).
+```
+
+The published window summand `8B/2^K` produces the same identity with
+`2^{1−62G}` replaced by `2^{3−62G}`. Either window term is smaller than
+`2^{−60}` times the digit term `2/B` once `G ≥ 1`.
+
+## The printed room does not contain the window term
+
+CRT.md §2 allows `E(p, ell) ≤ C_E 2^{4 ell} (p+2)^{16}`. With the §3
+formula for `G`,
+
+```text
+2^{−G} 2^{4 ell} (p+2)^{16}
+    = 2^{−60 ell} (p+2)^{16} / 2^{64 ceil(log2(p+2))}
+    ≤ 2^{−60 ell} (p+2)^{−48},
+```
+
+because `2^{ceil(log2(p+2))} ≥ p+2`. The factor `8B/2^K` does not occur.
+Substituting `β` leaves this line unchanged, including the constant
+`C_E` in front of `E`.
+
+## Absorption
+
+Assume `L ≤ p` and `r ≤ floor(L/(100G))`. Then `r ≤ p/(100G) ≤ p/19200`,
+and
+
+```text
+r (2/B + β) < r (2 + 2^{1−62G}) 2^{−G} ≤ p 2^{−G} / 6400.
+```
+
+The same bound holds with `8B/2^K` in place of `β`, because that only
+increases the tiny summand from `2^{1−62G}` to `2^{3−62G}`, and
+`2 + 2^{3−62G} < 3` still gives a factor below `1/6400`. Therefore both
+
+```text
+r (2/B + β) ≤ C p 2^{−G},    r (2/B + 8B/2^K) ≤ C p 2^{−G}
+```
+
+hold for every `C ≥ 1/6400`, and in particular for every `C ≥ 1`.
+Multiplying by the room line,
+
+```text
+r (2/B + β) E ≤ (C_E p / 6400) 2^{−60 ell} (p+2)^{−48}.
+```
+
+The scalar prefactor that CRT.md compares with `2^{−G}` gets smaller
+when `8B/2^K` is replaced by `β`, and the displayed `2^{−G} E` factor
+is unchanged. The `O(V)` comparison does not lose room.
+
+This is a comparison of those two displayed scalars. It is not a
+fixed-tape replay of bad-key evaluation, sorting, or reinsertion.

research/compact-switch-sharp-density/README.md

@@ -0,0 +1,94 @@
+# Sharp-window bad density for the compact switch
+
+**Scoped comparison. No new κ.** The selected conditional exponent is
+unchanged. This does not accept PR #4100.
+
+## Result
+
+CRT.md §4 bounds the bad density of one batch by
+
+```text
+r [2/B + 8B/2^K] ≤ C p 2^{-G}
+```
+
+and then uses the separate room
+
+```text
+2^{-G} E(p, ell) ≤ C 2^{-60 ell} (p+2)^{-48}.
+```
+
+The window summand `8B/2^K` is the fraction of `K−1`-bit windows outside
+the published margin `2B ≤ W < 2^m − 2B`. The isolated post-increment
+step admits the larger range `0 ≤ W ≤ 2^m − B + 1`. On that predicate the
+bad-window count is exactly `B − 2`, so the summand is
+
+```text
+β = 2(B − 2) / 2^K = ((B − 2) / (4B)) · (8B / 2^K).
+```
+
+For every `B > 2` this is strictly less than one quarter of the published
+window term. It is zero when `B = 2`.
+
+Under CRT.md's parameters `G = 64(ell + ceil(log2(p+2)))`, `B = 2^G`,
+`K = 64G`, with `ell ≥ 1`, `p ≥ 2`, `L ≤ p` and `r ≤ floor(L/(100G))`,
+
+```text
+r (2/B + β) < p 2^{-G} / 6400.
+```
+
+The same ceiling holds for the published window term. The displayed
+`2^{-G} E` line does not contain `8B/2^K`, so it is unchanged. Replacing
+the window term therefore does not shrink the scalar room CRT.md uses to
+put bad-key work in `O(V)`.
+
+The argument is in [PROOF.md](PROOF.md). The executable checks the window
+count by running the isolated step, the integer form of the ratio, the
+room identity, and the `C = 1/6400` comparison on a finite parameter grid.
+
+## Scope
+
+Card `formal-interface-lemma`, scope **refined**. The catalogue's first
+experiment for #4100 is to audit the compact-switch contract before a
+formalization campaign. That audit is PR #4321. Its open question 2 asks
+whether the section-4 density still fits `O(V)` if the window hypothesis
+is the sharp range. This package answers that question.
+
+The simultaneous carry argument in CRT.md still assumes the stricter `2B`
+margin. This count does not extend that argument to the extra windows.
+No tape repair, Lean proof, or multiplication theorem is claimed.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -B research/compact-switch-sharp-density/verify.py
+python3.12 -B scripts/research_package.py --package research/compact-switch-sharp-density
+```
+
+The direct command prints `PASS_COMPACT_SWITCH_SHARP_DENSITY`.
+
+## Open next questions
+
+1. Does one two-target macro with disjoint guards still restore both
+   controls on a window that is sharp-good but outside the published `2B`
+   margin? The density line can use `β` for the isolated predicate only.
+   First step: run the live two-target macro at `W = 0` and at
+   `W = 2^m − B + 1` with `K`-separated positions. Blocker: the twelve
+   paid `H`-bit exchanges are not replayed here.
+2. Is `L ≤ p` true for a real #4174 placement, or only a sufficient
+   hypothesis inherited from #4328? The constant `1/6400` uses that
+   hypothesis. First step: read one production plan's address length
+   against its `p`. Blocker: reservoir placement is not an input here.
+
+## Credit
+
+Cinna Davis, PR #4100, for CRT.md and `check_batched_crt.py`. The
+live-digit lemma and the sharp window are the compact-switch contract
+audit, PR #4321. The published density identity and the `L ≤ p`
+absorption hypothesis are PR #4328. The uniform evaluator constant is
+PR #4377 and is not reused. The guard-coloring decision is PR #4329.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance.
+Apache-2.0. No independent human review and no formal-kernel acceptance
+are claimed.

research/compact-switch-sharp-density/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/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/compact-switch-sharp-density/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Replace CRT.md section 4's window term 8B/2^K by the sharp-window fraction 2(B-2)/2^K and compare the union bound with the printed 2^{-G} E room.",
+  "scope_change_reason": "The card asks for one uncovered interface statement after the compact-switch contract is reviewed. PR #4321 is that review and leaves the section-4 density recomputation open. This package answers that question. It does not formalize the live-digit lemma in a proof assistant and does not repeat the gate-operand or certified-endpoint arithmetic.",
+  "bottleneck_link": "PR #4100's repair amortization charges bad records at the section-4 density. The sharp window shrinks that window term and leaves the printed 2^{-G} E line unchanged, so the scalar room does not shrink. This does not change kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the isolated window count, the ratio, and the scalar comparison under L <= p. Do not replay simultaneous carries, the tape repair, or Lean.",
+  "outcome": "completed",
+  "evidence": "PROOF.md. Verifier PASS_COMPACT_SWITCH_SHARP_DENSITY: sharp bad count B-2 on seven (B, m) pairs, room identity on seven (ell, p) pairs, C=1/6400 absorption on 15 parameter rows including 6 with r > 0, and two failure controls.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "Does one two-target macro with disjoint guards restore both controls on a window that is sharp-good but outside the published 2B margin?",
+      "why_it_matters": "The density substitution uses the isolated predicate. CRT.md's simultaneous carry argument still assumes the stricter margin.",
+      "first_step": "Run the live two-target macro at W=0 and at W=2^m-B+1 with K-separated positions.",
+      "blocked_by": "The twelve paid H-bit exchanges are not replayed here."
+    },
+    {
+      "question": "Is L <= p true for a real #4174 placement, or only a sufficient hypothesis inherited from #4328?",
+      "why_it_matters": "The constant 1/6400 uses L <= p. A larger address length needs its own constant.",
+      "first_step": "Read one production plan's address length against its p.",
+      "blocked_by": "Reservoir placement is not an input to this package."
+    }
+  ]
+}

research/compact-switch-sharp-density/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": 120,
+      "checks": "Sharp bad-window count equals B-2 by executing the isolated step; published count is 4B and strictly larger; ratio (B-2)/(4B); 2^{-G} E room identity; C=1/6400 absorption for L<=p on a parameter grid; failure controls reject a forged 4B count and a room line that drops E."
+    }
+  ]
+}