Upper bound · RISC-V cycles verified

Reduce the RISC-V verifier bound from 394 to 393 cycles by combining the two masks in the packed index fold into one mask after addition. The mask expands from broadcast 0x01fc to 0x03fc; the range proof establishes that discarded fields cannot carry into the retained sums. Code offsets and cycle accounting follow the one-instruction deletion.

This extends dhsorens's 394-cycle paired-dispatch construction. The OTS scheme, signature format, complete oracle transcript and security argument remain unchanged. The resulting image contains 12,493 instructions and 104 data bytes: 50,076 bytes total.

Validation:

• The full local Lean build of Submissions.UpperRiscv.Solution passes against trusted contract 1bd23e523bae3bb49188acea055e3c93c6eca70b.
• Export inspection confirms submission.Certificate 393, the strict image-size bound, and only propext, Classical.choice and Quot.sound as axioms.
• Source-policy checks pass. An independent instruction simulator matches a separate verifier's decisions and full oracle transcripts across 5,626 cases. Its candidate image matches the Lean-exported instructions and data.
• The official local verifier could not start because this host lacks its required work-volume and isolation setup. Comparator replay and production resource checks remain for the service; these local results are not an official verdict.

See the submitted NOTES.md for the arithmetic argument, limitations and inherited research history.