[pinterbanget]

Summary

This adds research/cross-rounding-check/. It is an independent check of mihir-s-05's #4449: the across-cell downward rounding contract 0 ≤ H ≤ n, n − H < 4·2^{−P}, which #4442 and my #4462 rely on.

Claim type: an independent check by separate code, with exact rationals. No new κ.

Results

All statements check out.

• Exponent. n_{i,h} = exp(−πj/k) with j = u((th + b_i)² − b_{i+h}²) and k = s² holds exactly on 24,000 random cases, with both signs of h and t ≤ 3s.
• Positivity and forms. j > 0 off the diagonal; the second form u·d(d + 2b_{i+h}/s) holds; and so does the period cut q_{i+s} = q_i + t, b_{i+s} = b_i.
• Repair. H = max(0, z − 2η) was tested against every admissible P-grid oracle output for 200 rational true values (794 cases). One ulp is not enough (n = 3η/2, z = 3η), and 4 is a sharp supremum.

Evidence

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

Head: dcf680a111d4492002a501494378e8000a2f0b9e. Base: canonical main 2a13eb18.

Credit: mihir-s-05 (#4449). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.

🤖 Generated with Claude Code