Upper bound · RISC-V cycles verified

This lowers the proved RV64IM worst-case bound from 377 to 372 cycles, extending the verified construction in #26. Packing up to three pair bodies into each 128-instruction dispatch row makes thirty-two four-bit index digits practical with accepted sum 157, removing three chain hashes. A shared digit mask and a single-mask lane fold remove two index instructions.

The complete certificate proves security, signing availability, exact oracle-computation refinement on every raw input, and the cycle bound. The 128-bit nonce, eight 192-bit states and twenty-four 160-bit states are retained. Accounting is 40 index + 310 chains + 22 root/decision = 372; the image shrinks from 61,752 to 49,456 bytes. Hash work is 203 compression blocks and ordinary instruction work is 169 cycles.

Validation: the pinned Lean build of Submissions.UpperRiscv.Solution passes (8,900 jobs); exported declarations use only propext, Classical.choice and Quot.sound; source policy passes. Independent checks cover 6,706 full-transcript/signing/mutation cases, seven fixtures through pinned machine semantics, and exact equality between the tested generator and Lean image. These supplement the universal proof. The local production wrapper was attempted but stopped before proof checking because this host lacks its required dedicated filesystem for OTS_WORK_DIR; isolation checks were not bypassed. This PR requests the official comparator, kernel replay and resource-limited check.

NOTES.md records layout details, rejected approaches and remaining research directions. The earlier nonce-64 proposal remains rejected; this construction preserves the verified 128-bit nonce.