Audit the compact-switch coefficient and guard contract.

research/compact-switch-contract/README.md

@@ -0,0 +1,149 @@
+# Compact-switch contract
+
+**Scoped contract audit. No new κ.** The selected conditional result stays
+0.001672660197076918. This does not accept PR #4100 and it does not formalize
+the lemma in a proof assistant.
+
+## Scope and evidence
+
+Card `formal-interface-lemma`, scope **refined**. The catalogue's first
+experiment for #4100 is to audit the compact-switch statement and its
+hypotheses before a formalization campaign. That audit is the result here.
+Gate-operand parity (#3807) and certified endpoint arithmetic (#3857) are
+left untouched.
+
+The object is the one-target cancellation and the two-call macro in
+`research/unconditional-batched-crt/CRT.md`, section 4, at base
+`12fa8c5c844be21bfefb38a19503fbd867a11244`. The displayed gadget is
+
+```text
+y += sum_i 2 z_i t_i 2^j_i;
+t += sum_i y[j_i] B^i;
+y += sum_i z_i (1-2t_i) 2^j_i;
+t -= sum_i (y[j_i] XOR z_i) B^i.
+```
+
+The same section then says that the two `y` additions have total `z(1-2b)`.
+Those two readings disagree. `t_i` is introduced as the digit before `F`.
+Reusing that same integer in the third line is a frozen coefficient. The
+total `z(1-2b)` is the live digit after `t <- t+b`. The published
+`primitive_f` in `check_batched_crt.py` implements the live digit.
+
+## Lemma
+
+Let `B >= 2`, let `τ` be an integer in `0, ..., B-2`, and let `b, z` be bits.
+Place the target at bit 0 and let the `m` bits above it hold an integer
+window `W` with
+
+```text
+0 <= W <= 2^m - B + 1.
+```
+
+Set `L = b + 2W`. The post-increment step
+
+```text
+L1 = L + 2 z τ
+τ' = τ + b
+L2 = L1 + z (1 - 2 τ')
+```
+
+returns `L2 = L + z(1-2b)`. The target bit flips exactly when `z = 1`, the
+window returns to `W`, and neither `L1` nor `L2` uses a bit at position
+`m+1` or higher. The updated digit `τ'` is at most `B-1`, so a packed
+base-`B` increment does not carry into the next digit. Subtracting the final
+bit `b XOR z`, XOR `z`, removes exactly `b` from the digit `τ+b` and restores
+`τ` without borrowing from the next digit.
+
+The published margin `2B <= W < 2^m - 2B` implies the bound above for every
+`B >= 2`. It is sufficient for this isolated step. It is stricter than the
+step requires: `W = 0` satisfies the identity, and the first overflowing
+window is `W = 2^m - (B-2)` when `B > 2`, at `τ = B-2` and `z = 1`.
+
+Execute that step, add a Boolean `f` into the control digit, and execute the
+step again. If `f` does not read the target bit, the two live parities are
+`z` and `z XOR f`, the target ends as `b XOR f`, and both the control digit
+and the window return to their starting values. The same holds for several
+targets whose `K`-bit guards are pairwise disjoint, with `K = m+1`, when
+every source omits every active target and every control digit is at most
+`B-2`.
+
+## Witnesses
+
+All of the following use `B = 4` and the published good predicate
+(`guard = 6`, so `m = 5` and `8 <= W < 24`).
+
+| Reading | Start `(u, t, y)` | Endpoint |
+| --- | --- | --- |
+| One post-increment step | `(1, 0, 17)` | `y = 16` |
+| One frozen step | `(1, 0, 17)` | `y = 18` |
+| Macro, live digit, `f = 0` | `(1, 0, 17)` | `(1, 0, 17)` |
+| Macro, frozen digit, `f = 0` | `(1, 0, 17)` | `(1, 0, 19)` |
+| Published `primitive_f` | `(1, 0, 17)` | `(1, 0, 16)` |
+| Published `compact`, `f = 0` | `(1, 0, 17)` | `(1, 0, 17)` |
+
+`y = 17` is bit 0 set and window `W = 8`. The frozen step adds `+1` at a set
+bit and changes the window. The published checker follows the live digit.
+
+Targets at bits 0 and 1 both meet the per-target margin on
+`(u, t, y) = (0, 1, 80)`, with sources `(bit 4, bit 5) = (1, 0)`. The ideal
+restoration is `(0, 1, 81)`. The live macro returns `(0, 5, 81)`: the data
+bit flips and the control word does not return. Disjoint guards are a
+hypothesis of the simultaneous claim. The published finite sweep uses
+positions `(0,)` and `(0, 6)`, which are disjoint at `guard = 6`; it does
+not see this pair.
+
+A source that reads bit 0 on the same start `(1, 0, 17)` ends at `(0, 0, 17)`.
+The load and the unload disagree, so omitting every active target is required.
+
+Finite corroboration, all checked by this package:
+
+- 25,592 isolated windows across `B in {2,4,8,16}` and `m = 8`, including
+  windows below the published lower margin, with 3 sharp overflows.
+- 656 published-margin windows, every one inside the sharp range, and 90
+  sharp windows outside the published margin.
+- 36,864 single-target macros on every published-good address in
+  `u, t < 16`, `y < 256`, for both constant sources.
+- 331,776 disjoint two-target macros, positions `(0, 8)`, on every
+  published-good address in `u, t < 16`, `y < 2^14`.
+
+## What this does not establish
+
+The twelve paid `H`-bit exchanges, the reservoir shuttle, the bad-key sort,
+the `O(V)` guard scan, and the all-size CRT/multiplication assembly are not
+replayed. A passing isolated identity does not discharge those obligations.
+No Lean proof is supplied. The published `2B` margin remains a valid
+sufficient condition for the density estimate in CRT.md; this package does
+not replace that estimate.
+
+## Reproduce
+
+From the repository root, Python 3.12, standard library only:
+
+```sh
+python3.12 -B research/compact-switch-contract/verify.py
+python3.12 -B scripts/research_package.py --package research/compact-switch-contract
+```
+
+The direct command prints `PASS_COMPACT_SWITCH_CONTRACT` and the counts
+above. Local runtime is a few seconds.
+
+## Open next questions
+
+1. Formalize the live-digit lemma, with disjoint `K`-bit guards and
+   target-omitting Boolean sources as hypotheses. The statement above is the
+   one to formalize; freezing `t_i` at its pre-step value is a different
+   operation. A proof-assistant build is a separate budget. Nothing in the
+   arithmetic is still unresolved for that lemma.
+2. Recompute the section-4 bad-density estimate from the sharp window
+   `0 <= W <= 2^m - B + 1` and check whether the existing `O(V)` room still
+   holds. The first step is to replace only the `8B/2^K` term and compare it
+   with the printed `2^-G E(p, ell)` bound. The blocker is the rest of that
+   amortization, which this package does not audit.
+
+## Credit
+
+The compact-switch writeup and `check_batched_crt.py` are Cinna Davis's
+PR #4100 (`research/unconditional-batched-crt`, head retained on this base
+as `337d04939571a637aeab54a0f58f54fde811663a` in the family record). This
+package does not rerun that construction. Prepared by unpaidmoon with
+substantial Cursor Grok assistance. Apache-2.0.

research/compact-switch-contract/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/compact-switch-contract/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "Audit the PR #4100 compact-switch cancellation before formalization: the live post-increment digit, the sharp window, and disjoint guards.",
+  "scope_change_reason": "The card asks for one uncovered interface formalization. Its first experiment says to audit the #4100 compact-switch contract before a proof-assistant build. This package is that audit and the corrected lemma. It does not repeat the gate-operand parity lemma or the certified endpoint arithmetic, and it does not start a Lean build.",
+  "bottleneck_link": "PR #4100's proposed all-size exponent depends on this switch. A formalization that freezes the displayed coefficient, or that drops disjoint guards, would certify a different operation. Fixing the statement is a prerequisite for any later interface proof; this package does not change kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the isolated live-digit identity, the frozen and overlap witnesses, and the disjoint finite sweep. Do not replay the CRT amortization, tape program, or Lean baseline.",
+  "outcome": "partial",
+  "evidence": "Written post-increment lemma. Independent enumeration of 25592 safe windows, 36864 single-target macros and 331776 disjoint pair macros. Frozen witness y=17 to y=18; overlap witness (0,1,80) returns control 5. Published primitive_f matches the live digit on that witness. Receipt PASS_COMPACT_SWITCH_CONTRACT.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "Formalize the live-digit compact-switch lemma with disjoint K-bit guards and target-omitting Boolean sources.",
+      "why_it_matters": "Freezing t_i at its pre-step value is a different gadget, and overlapping targets that meet the per-target margin fail restoration.",
+      "first_step": "Use the lemma in research/compact-switch-contract/README.md as the statement. Check it against the frozen witness (u,t,y)=(1,0,17) and the overlap witness (0,1,80).",
+      "blocked_by": "A separate proof-assistant budget. The arithmetic statement itself is not blocked."
+    },
+    {
+      "question": "Does the section-4 bad-density estimate still fit O(V) if the window hypothesis is relaxed to 0 <= W <= 2^m - B + 1?",
+      "why_it_matters": "The published 2B margin is sufficient for isolated cancellation and stricter than the sharp window. A smaller bad set can only help the estimate, but the printed 8B/2^K term was not recomputed here.",
+      "first_step": "Replace only that term in CRT.md section 4 and compare it with the printed 2^-G E(p, ell) bound.",
+      "blocked_by": "The rest of the section-4 amortization, which this audit does not replay."
+    }
+  ]
+}

research/compact-switch-contract/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": "Live-digit identity on every sharp window for B in {2,4,8,16}; published margin is a subset; single-target and disjoint two-target macros; frozen, overlap, and target-reading controls must fail the ideal endpoint; published primitive_f matches the live digit on (1,0,17)."
+    }
+  ]
+}