[unpaidmoon]

Change and mathematical scope

Finite certificate, scope refined, no new κ. The selected conditional κ stays 0.001672660197076918.

Let C = |Sp(72,2)| * 14826 be the selected m=73 finite stock from research/selected-stock-envelope-m73, with |Sp(72,2)| = 2^1296 * prod_{j=1..36} (2^(2j) - 1) and 14826 = 14336 + 480 + 8 + 2. This package proves

2^2641 <= C < 2^2642

and, for every integer q > 2^80,

log_q C < 34.

So A = 0 and B = 34 satisfy the coarse-depth slot log_q C(w) <= A*w + B at every atom width w >= 1. The integer B = 33 does not: the prime q = 2^80 + 13 has C > q^33 and C <= q^34.

research/selected-stock-shape-a-zero already set A = 0 and substituted the bit length 2642 into

sigma <= (43/26) * (1 - s) * 2642 + rho.

2642 remains a valid log_q upper bound (log_q C < log2(C) < 2642 for every integer q > 2). It is not necessary on q > 2^80. The C-part ratio before the unbound leaf constant rho is exactly 2642/34 = 1321/17.

rho stays unbound, so this is not a numerical sigma. No cutoff margins are recomputed. No supplier, caller, or selected frontier changes. The ordinary BIT coefficients 8194, 6748 and 6741 are a different producer. Historical 57604 and 252 are not used.

Task and overlap

Base bb4bccbf42844d2801487450727c2f63e10d1d0f (upstream main at PR CrocSwap#3725). Task card selected-stock-envelope, priority revision 6, method 2: an exact missing implication for a proposed selected-stage stock envelope. Scope status is refined: the shape note already plugged bit length 2642 into a log_q slot, and this package separates that plug-in from a sufficient log_q coefficient. It does not rederive the bit length or a reserve recurrence.

Session item 28 of the ordered eligible list (eight still-open chronological handoffs, then catalogue methods in file/weight order). Items 1–10 were left for sibling sessions. Item 28 is catalogue method 20.

Nearest predecessors, retained and not replaced:

• research/selected-stock-envelope-m73 and merged Selected stock envelope at m=73: bound quantities and the exact missing shape lemma CrocSwap/integer-mult-bounds#3113 supply C, the family split 14826, and bit length 2642.
• research/selected-coarse-depth-stock supplies the slot log_q C(w) <= A*w + B.
• research/selected-stock-shape-a-zero and merged Research: selected m=73 complex stock shape A=0 under finite-stock-as-C (no new kappa) CrocSwap/integer-mult-bounds#3421 supply the composition sentence that substitutes 2642.

Open row-ledger notes such as CrocSwap#3667 and CrocSwap#3766 also leave rho unbound. This package does not rerun those ledgers. No open PR found that proves B = 34 on q > 2^80 or the prime 2^80 + 13.

Validation

Environment: Python 3.12, no extra requirements. Author-checked finite certificate. Primality of 2^80 + 13 is Pocklington, not a formal kernel and not an OpenSSL prime call. The factored part of each predecessor is the whole predecessor. Small prime factors are trial-proved through their square roots. Exponent comparisons are integer powers: (2^80 + 1)^34 > 2^2720 > C, and C > (2^80 + 13)^33.

python3.12 -B scripts/research_package.py --package research/logq-stock-shape-gap
python3.12 -I -B research/logq-stock-shape-gap/verify.py
python3.12 -I -O -B research/logq-stock-shape-gap/verify.py
python3.12 -I -B research/logq-stock-shape-gap/independent.py

verify.py exits by SystemExit rather than assert, so -O does not disable the checks. independent.py rebuilds C by multiplying the odd symplectic factors first and does not import verify.py. Expected lines include PASS_LOGQ_STOCK_SHAPE_GAP, PASS_LOGQ_STOCK_SHAPE_INDEPENDENT, and PASS_REGISTERED_RESEARCH_PACKAGE research/logq-stock-shape-gap outcome=completed.

Not run: selected cold replay, Lean, Docker, hosted CI, and any cutoff-margin table.

Credit

The symplectic formula, the family split 14826, and the bit length 2642 are from research/selected-stock-envelope-m73. The log_q slot is from research/selected-coarse-depth-stock. The substitution of 2642 is the composition sentence in research/selected-stock-shape-a-zero. Those packages retain their own predecessor credit. The base-change certificate and the prime 2^80 + 13 are new.

Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. No independent human or formal-kernel review is claimed.

Open next questions

From research/logq-stock-shape-gap/TASK.json:

1. Bind rho for this finite stock, or prove it is zero under a completed-leaf interface. The 1321/17 gap scales only the C-part; a large rho can dominate 34 and 2642 alike. Blocked because the retained complex sources still do not state a per-leaf reserve recurrence.
2. Check one selected stage at the actual atom width w = ceil(e^s). A uniform log_q coefficient is not yet a stage-width envelope. Blocked because rho is missing, so neither coefficient is a closed sigma.

Workflow feedback (optional)

CrocSwap#1200