[jwr404]

Change and mathematical scope

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

On the equality-case layout p = 1, ell = 2, G = 256, r_max = 2,

6 · 2^{-256} · 2^{8} · 3^{16} = 3^{17} / 2^{247}.

The printed room line is 1 / (2^{120} · 3^{48}). The ratio is 3^{65} / 2^{127}, which lies in [2^{-24}, 2^{-23}). The product is strictly below the room, and strictly below 1/6400 of the room: the integer quotient is 2580. C_E is a common factor and is not evaluated. The scalar constant 1/6400 still fails on this layout; the envelope slack (3/4)^{64} is what restores the product.

On the admitted layout p = 2, ell = 2, r_max = 2, p+2 is a power of two, so the same ratio is exactly 6 and the product exceeds the room.

Task and overlap

• Base: canonical main 624de9dc66858af0945e5f8a0942488d62280d43, fetched 2026-10-23T00:00:26Z, priority revision 7.
• Card: formal-interface-lemma, scope refined. This is the open question of PR Record the uniform reservoir constant 3 r_max / p (no new κ) #4923.
• Predecessor: PR Audit CRT reservoir placement and split-axis coordinate descriptors #4174 admits the layouts. PR Compare the sharp compact-switch window with CRT.md's repair room. #4646 prints the envelope and the room line. PR Record the uniform reservoir constant 3 r_max / p (no new κ) #4923 supplies the prefactor 6.
• Package: research/crt-reservoir-envelope-product/.
• Overlap at 2026-10-23T00:00:22Z: this package only. No other evaluation of 3^{65}/2^{127}.

Validation

Python 3.12, standard library only:

python3.12 -B scripts/research_package.py --package research/crt-reservoir-envelope-product

Observed PASS_CRT_RESERVOIR_ENVELOPE_PRODUCT ratio=3^65/2^127 below_room=1 below_6400=1 control_ratio=6, then PASS_REGISTERED_RESEARCH_PACKAGE research/crt-reservoir-envelope-product outcome=completed.

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

Credit

Hiroki KUMAZAKI, PR #4174, for the constructor. PR #4646 for the envelope and room line. PR #4923 for the prefactor 3 r_max. 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 production plan p = 9240576, ell = 24, r_max = 5, is 3 r_max ((p+2)/2^{ceil(log2(p+2))})^{64} at most 1/6400? First step: compute ceil(log2(9240578)) and compare 15 (p+2)^{64} with 2^{64 ceil(log2(p+2))} / 6400.