[aliromman]

This conditional precision theorem covers the entire current selected PR6030 word, including every native MOVE. Under an explicit conditional mean-zero completed-error contract, it certifies 13 guard bits for individual RMS error and 16 guard bits for a whole-word failure probability below 2^-41. The matched absolute-error formula needs 17 bits. These are different guarantees; no new complete κ, physical rounder or selected assumption discharge is claimed. Selected κ remains 0.003125804.

Review the proof, feedback argument and stopped Hilbert tail, exact ledger and rational certificate, two transfer engines, verification and controls, and source manifest. Reviewed commit: f2431f81bfc1a7b418ce3a1b02b958d5f259f50b. Canonical main base: 7c49fe32c55de02c2c873655c804b16e4c3fef0a.

The exact selected source word has 22,803 events, 770 arbitrary public inputs and 29 owned labels. Native charts are supplied deterministic unitaries; COPY, INIT and CLEAR are exact. Completed MOVE/ADD/SCALE defects have conditional mean zero given the full past and the stated relative norm allowance on actual operands. Neither independence nor merely unconditional unbiasedness is substituted for that condition.

For input field norm bound B > 0 and every integer t >= 0:

Allowance	Certified guarantee
u <= 2^(-t-13)	Each field at every prefix has RMS error below B 2^-t; final public RMS is at most (24842101/31854592) B 2^-t.
u <= 2^(-t-16)	The probability of any field at any prefix reaching error norm B 2^-t is below 2^-41.
u <= 2^(-t-17)	The matched absolute-error formula gives error below B 2^-t for every allowed defect sequence.

The exact squared signed-transfer maxima are J² = 48,438,375 and K² = 5,490,111/32. Integer upper roots J = 6,960 and K = 415 give the feedback bound E_RMS <= B*u*J/(1-u*K). The tail proof stops at the first prefix excursion, retains actual-input feedback, and uses a self-contained dimension-independent Hilbert exponential-moment inequality. Its numerical step is the exact rational certificate

45606 exp(-2147483648/54390625) < 2^-41.

A 65-term positive Taylor sum certifies this strict inequality. At B=0 all errors are exactly zero; the proof handles that case separately and does not assert that Pr(0 >= 0) is small. Maximum individual RMS is kept distinct from RMS of the maximum. Multiple invocations require an additional union budget. The displayed guards are sufficient certificate parameters, not least machine precisions.

Validation used CPython 3.12.13 and the standard library:

python3.12 -B scripts/research_package.py --package research/selected-whole-word-stochastic
python3.12 -B scripts/check_research_commit.py --package research/selected-whole-word-stochastic --check-source-history

Normal and optimized registered runs pass. Fraction and integer/binary-denominator arithmetic agree on all 22,803 ideal operand weights. Forward and transpose engines compare every exact coefficient and score at all 799 final fields directly; receipt digests summarize those checked rows. Reverse substitution checks all peaks. There are 36 enumerated adaptive-noise cases, 218 terminal states and 900 square-root cases. Eight controls distinguish feedback, reused/biasing randomness, COPY/reset errors, erased prefix excursions and both zero-threshold events. Changed source bytes are rejected. Every smaller guard is checked for the stated RMS and absolute formulas.

PASS_SELECTED_WHOLE_WORD_STOCHASTIC 22803 events; 799 final rows; RMS guard 13 ; tail guard 16 ; absolute guard 17
PASS_REGISTERED_RESEARCH_PACKAGE research/selected-whole-word-stochastic outcome=completed
PASS_RESEARCH_COMMIT_BYTES

Nine committed package/input files, source ancestry and official export integrity/declared-input coverage pass. A read-only, Git-free optimized exported replay with empty PATH also passes; all ten exported files retain their bytes and modes. Hosted CI is pending at publication. No full predecessor native/supplier replay, physical unbiased native rounder, exact dirty restoration, sampler/tape/compiler bill, independent human review or proof-kernel verification ran. The ideal ledger finds 30 of 31 CLEAR events erase nonzero ideal data; exact reset is a retained premise. All five framework assumptions remain.

Credit DreamingOfClouds / @DreamingOfClouds for PR #6030, audited source head 772dd10a5859a1d15f4851feb371519789213ad8, and its retained P104/native/caller lineage. Ali Romman's PR #5819 and operand-weighted completed-error proof retain Adam Gall, ywz65 and earlier method credit. Nick Petalas / @petalas supplied the released whole-word idea and disclosed probability error, and PR #6026's distinct historical-prefix stochastic proof. No historical numerical constant or prefix guarantee is silently transferred. Martingale orthogonality, stopping and exponential-moment methods retain their classical credit.

The next obligation is one actual native rounder satisfying this conditional contract, followed by paid exact restoration and a complete caller failure budget. Current all-state PR/Discussion searches found no same whole-6030 stochastic contract; sparse notes, arbitrary diffs and unpublished work remain coverage limits. Scoped claim. Prepared by Ali Romman with substantial OpenAI Codex assistance. New work is Apache-2.0.