[pinterbanget]

Summary

This adds research/crt-evaluator-independent-check/. It independently checks unpaidmoon's #4377, which proves E(p, ℓ) ≤ 2^{4ℓ}(p+2)^{16} with constant C = 1 for #4100's sequential CRT and rotation-switch evaluator.

Claim type: an exact re-derivation plus an instrumented operand-size check. No new κ. Nothing is imported from #4377.

Results

• The arithmetic holds. These were all re-derived exactly:

  • the 8ab schoolbook and division tariffs, and the Euclid tariff 64b³;
  • the six cost terms;
  • 7·max ≤ B and Σ ≤ B on p ≤ 200, ℓ ≤ 40;
  • the guard amortization.

  The largest Σ/B is 1.96·10⁻³, so the closing inequality has about 500× slack.

• The per-axis bill holds, but tightly. The retained decode_group and balanced offset step were instrumented to charge every operation at its actual operand bit lengths, and the output was compared with the retained code. All 653 axes are within 128mW² + 128mℓ³ + 16mW. At m = 1 the ratio climbs from 0.950 at ℓ = 14 to 0.977 at ℓ = 32, because the two modular inverses use the whole 2m·64ℓ³ budget.

• One non-load-bearing slip. PROOF.md prices a rotation-table wire at 9(ℓ+2)². Its own tariffs give 4(ℓ+2) + 8(ℓ+2)², which is 84 against 81 at ℓ = 1. The per-network bound still holds with the corrected step, so nothing downstream changes. Writing ≤ 12(ℓ+2)², or using the true quotient length of at most 3 bits, fixes it.

Evidence

python3.12 -B scripts/research_package.py --package research/crt-evaluator-independent-check --check-only
  PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)
python3.12 -B scripts/research_package.py --package research/crt-evaluator-independent-check
  PASS_REGISTERED_RESEARCH_PACKAGE research/crt-evaluator-independent-check outcome=completed   (<1 s, stdlib only)

Head: f39e5c22b106be00ac16d89c19686b9c9853a0e1. Base: canonical main 12fa8c5c, priority revision 7. check_batched_crt.py is pinned.

Not covered

• The tape model and the head movement of indexed scans.
• An independent implementation of the Beneš scans.
• Reservoir placement, sparse repair and the outer theorem.

Task and overlap

• Card: uniform-transfer-audit, refined.
• Claim: Handoffs and requests for independent checks #1166 (comment)
• Overlap: no other review of Prove the uniform CRT evaluator bound with constant 1. #4377 had been posted.

Credit

@unpaidmoon for the proof (#4377). Cinna Davis for the CRT construction and retained code (#4100). ToikY's #4192 is the predecessor.

Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance; no independent human review. Apache-2.0. This PR does not merge anything or change the frontier.

🤖 Generated with Claude Code