[jwr404]

Change and mathematical scope

Scoped comparison. No new κ. The selected conditional exponent stays 60403/20000000, and PR #4100 is not accepted.

Every layout accepted by the #4174 constructor has G ≥ 256. The constructor requires p ≥ 1 and ell ≥ max(2, ceil(log2(p+2))), and ceil(log2(p+2)) ≥ 2, so

G = 64 (ell + ceil(log2(p+2))) ≥ 256.

The floor is achieved at p = 1, ell = 2, and 65,536 widths of 1: G = 256, L = 65536, r_max = 2.

For G ≥ 256 the factored sharp term 2 + 2^{1−62G} − 2^{2−63G} is strictly less than 3. At r = r_max,

r (2/B + β) < (3 r_max / p) p 2^{-G}.

The same bound covers the published window term. On the equality case the constant is 6, and both C = 1 and C = 1/6400 fail. When the layout also has L ≤ p, 3 r_max / p ≤ 3/25600 < 1/6400, so the older constant still covers those layouts. The production plan r_max = 5, p = 9240576 satisfies the tighter majorant.

Task and overlap

• Base: canonical main 624de9dc66858af0945e5f8a0942488d62280d43, fetched 2026-10-22T23:52:56Z, priority revision 7.
• Card: formal-interface-lemma, scope refined. This is the open question of PR Record the constant 3 on the longer reservoir layout (no new κ) #4921.
• Predecessor: PR Audit CRT reservoir placement and split-axis coordinate descriptors #4174 for the constructor. PR Compare the sharp compact-switch window with CRT.md's repair room. #4646 for the factored term. PR Record the constant 3 on the longer reservoir layout (no new κ) #4921 for the single layout p = 2.
• Package: research/crt-reservoir-uniform-constant/.
• Overlap at 2026-10-22T23:52:52Z: this package and PR Record the constant 3 on the longer reservoir layout (no new κ) #4921's open question. No other proof that G ≥ 256 for every accepted layout.

Validation

Python 3.12, standard library only:

python3.12 -B scripts/research_package.py --package research/crt-reservoir-uniform-constant

Observed PASS_CRT_RESERVOIR_UNIFORM_CONSTANT G_min=256 equality_p=1 equality_r=2 integer_factor=3, then PASS_REGISTERED_RESEARCH_PACKAGE research/crt-reservoir-uniform-constant outcome=completed.

Not run: a layout census, the 104,864-plan schedule, the E product, Lean, and Docker.

Credit

Hiroki KUMAZAKI, PR #4174, for the constructor. PR #4646 for the factored window term. PR #4921 for the constant 3 on one layout. Cinna Davis, PR #4100, for the CRT parameters.

Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0. No independent human review and no formal-kernel acceptance are claimed.

Open next questions

1. On the equality-case layout p = 1, ell = 2, r_max = 2, G = 256, what does 3 r_max 2^{-G} times the printed E envelope become? First step: multiply 6 · 2^{-256} by 2^{4 ell} (p+2)^{16} and compare with 2^{-60 ell} (p+2)^{-48}.