[jwr404]

Change and mathematical scope

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

On the #4174 production plan p = 9240576, ell = 24, G = 3072, r_max = 5,

ceil(log2(9240578)) = 24,
R = 15 (9240578 / 2^{24})^{64}.

The numerator has bit length 1485 and the denominator is 2^{1536}, so 2^{-52} ≤ R < 2^{-51}. Thus R < 1/6400. The quotient of 1/6400 by R is 393602022308 with a positive remainder. The bare room's quotient by R is 2519052942774845, also with a positive remainder.

L ≤ p does not force the bound. The constructor accepts p = 2^{24} - 2, ell = 24, and 65,536 widths of 23, with L = 1507328 ≤ p and r_max = 4. There p+2 is a power of two, so R = 12, which exceeds both 1/6400 and the bare room.

Task and overlap

• Base: canonical main 624de9dc66858af0945e5f8a0942488d62280d43, fetched 2026-10-23T00:04:29Z, priority revision 7.
• Card: formal-interface-lemma, scope refined. This is the open question of PR Record the equality-case envelope product (no new κ) #4924.
• Predecessor: PR Audit CRT reservoir placement and split-axis coordinate descriptors #4174 for the production layout. PR Compare the sharp compact-switch window with CRT.md's repair room. #4646 for the envelope. PR Record the equality-case envelope product (no new κ) #4924 for the ratio on the equality case.
• Package: research/crt-reservoir-production-ratio/.
• Overlap at 2026-10-23T00:04:25Z: this package and PR Record the equality-case envelope product (no new κ) #4924's open question. No other evaluation of this production ratio.

Validation

Python 3.12, standard library only:

python3.12 -B scripts/research_package.py --package research/crt-reservoir-production-ratio

Observed PASS_CRT_RESERVOIR_PRODUCTION_RATIO log=24 ratio_bits=52 below_6400=1 edge_ratio=12, then PASS_REGISTERED_RESEARCH_PACKAGE research/crt-reservoir-production-ratio outcome=completed.

Not run: the 104,864-plan schedule, the real E polynomial, Lean, and Docker.

Credit

Hiroki KUMAZAKI, PR #4174, for the production layout. PR #4646 for the printed envelope. PR #4924 for the equality-case ratio. 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 edge layout p = 2^{24} - 2, ell = 24, r_max = 4, the envelope ratio equals 12. Is 12 still at most p/6400? First step: compare 12 · 6400 with 16777214.