Independently check #4377's CRT evaluator bound: arithmetic holds with ~500x slack; per-axis bill tight (0.977) at m = 1; one non-load-bearing wire-tariff slip at ell = 1 (no new κ)

research/crt-evaluator-independent-check/README.md

@@ -0,0 +1,75 @@
+# Independent check of #4377's CRT evaluator bound
+
+**Claim type:** an independent exact re-derivation plus an instrumented operand-size check. **No
+new κ.** It checks unpaidmoon's
+[#4377](https://github.com/CrocSwap/integer-mult-bounds/pull/4377) (`PROOF.md`), which proves
+`E(p, ℓ) ≤ 2^{4ℓ}(p+2)^{16}` with constant `C = 1` for #4100's sequential CRT and rotation-switch
+evaluator. Nothing is imported from #4377.
+
+## Results
+
+**Part A: the arithmetic holds.** All of these were re-derived with exact integers:
+
+- the schoolbook and restoring-division tariffs, `8ab`, for `a, b ≤ 64`;
+- the Euclid tariff `64b³`;
+- the six cost terms;
+- the bound `7·max ≤ B` and the sum bound `≤ B`, on `p = 2..200` and `ℓ = 1..40`;
+- the guard amortization `2^{−G}E ≤ 2^{−60ℓ}(p+2)^{−48}`.
+
+The largest ratio of the six terms' sum to `B` is `1.96·10⁻³`, at `p = 2, ℓ = 1`. The closing
+inequality has a factor of about 500 of slack.
+
+**Part B: the per-axis bill holds, tightly.** An instrumented copy of #4100's retained
+`decode_group` and `balanced` offset step charges every multiplication, division, inverse and
+addition at its **actual** operand bit lengths. It uses #4377's tariffs, with the quotient length
+of each division. The source is `check_batched_crt.py`, pinned, and its result is compared with
+the retained function's output. The check covers 653 axes:
+
+- groups with `W ≤ p` at `ℓ = 3..12`;
+- long-moduli cases at `ℓ = 14..32`, with `m ∈ {1, 2, 4}` and a full right-child prefix.
+
+Every axis is within #4377's per-axis bill `128mW² + 128mℓ³ + 16mW`. The bill is nearly tight,
+though. At `m = 1` the ratio rises steadily from 0.950 at `ℓ = 14` to 0.977 at `ℓ = 32`. The two
+modular inverses, one in `decode_group` and one for the target, use the whole `2m·64ℓ³` inverse
+budget. Any extra inverse in an implementation would exceed the per-axis bill. It would still
+pass the closing inequality, given the factor-500 slack.
+
+**Part C: one non-load-bearing slip.** `PROOF.md` prices one rotation-table wire at
+`9(ℓ+2)²`, as "one addition and one restoring division of integers of at most `ℓ + 2` bits". Its
+own tariffs give `4(ℓ+2) + 8(ℓ+2)²`. That exceeds `9(ℓ+2)²` exactly when `ℓ = 1`, where it is
+84 against 81. With the corrected step, the per-network bound `25(ℓ+2)²2^ℓ + 64ℓ2^{2ℓ}` still
+holds for every `ℓ ≤ 40`, so nothing downstream changes. A one-line fix is to state the wire cost
+as `4(ℓ+2) + 8(ℓ+2)² ≤ 12(ℓ+2)²`. A smaller fix uses the true quotient length of at most 3 bits.
+
+## Not covered
+
+- The tape model and the head-movement accounting of indexed scans.
+- The Beneš scan recurrence, which is only re-derived here, as in #4377.
+- Reservoir placement, sparse repair and the outer theorem.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/crt-evaluator-independent-check --check-only
+python3.12 -B scripts/research_package.py --package research/crt-evaluator-independent-check
+```
+
+The verifier prints `PASS_CRT_EVALUATOR_INDEPENDENT_CHECK` in under a second, using only the
+standard library.
+
+## Open next questions
+
+1. **Does any #4100 caller use more than `m + 1` modular inverses per axis?**
+   - *Why it matters:* the per-axis bill has almost no room left at `m = 1`.
+   - *First step:* trace the inverse macro's own offset computation, which #4377 prices as a
+     second pair of networks.
+   - *Blocked by:* nothing.
+
+## Credit
+
+The proof and its tariffs are unpaidmoon's (#4377). The CRT construction and the retained
+`decode_group`/`balanced` code are Cinna Davis's (#4100). ToikY's #4192 is the predecessor Beneš
+audit.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/crt-evaluator-independent-check/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/check_batched_crt.py",
+      "usage": "input",
+      "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc",
+      "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e"
+    }
+  ]
+}

research/crt-evaluator-independent-check/TASK.json

@@ -0,0 +1,74 @@
+{
+  "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": "Independently check #4377's E(p,ell) <= 2^(4 ell)(p+2)^16 evaluator bound: exact re-derivation and actual-operand-size charging of the retained CRT code.",
+  "scope_change_reason": "The card asks for one quantified #4100 implication; #4377 supplies the uniform evaluator constant with no independent check.",
+  "bottleneck_link": "CRT.md section 4's guard amortization uses this evaluator bound.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at the arithmetic, the instrumented bill and the slip; do not model tapes.",
+  "outcome": "completed",
+  "evidence": "verify.py: master inequality holds with sum/B <= 1.96e-3 on p<=200, ell<=40; 653 instrumented axes within the per-axis bill (max 0.977, rising to 1 at m=1); per-wire 9(ell+2)^2 fails only at ell=1 (84>81), absorbed by the per-network bound.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Does any #4100 caller use more than m+1 modular inverses per axis?",
+      "why_it_matters": "The per-axis bill has almost no room at m=1.",
+      "first_step": "Trace the inverse macro's offset computation.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/crt-evaluator-independent-check/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/unconditional-batched-crt/check_batched_crt.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Pinned retained decode_group/balanced lines; #4377 tariffs, six terms, master inequality and guard amortization on p=2..200, ell=1..40; instrumented operand-size charging of 653 CRT axes against the per-axis bill, offsets equal to the retained code; per-wire slip exactly at ell=1 and its absorption."
+    }
+  ]
+}