Upper bound · RISC-V cycles verified

This reduces the RISC-V upper bound from 393 to 377 cycles with a mixed-width 32-chain construction and a complete Lean certificate. The 5504-bit signature retains the 128-bit nonce; eight chains use 192-bit states and twenty-four use 160-bit states.

Verification performs 192 chain hashes. Backward expansion of the packed narrow states preserves unread inputs, and completed outputs form the 6272-bit root input without a copy pass. Packed two-digit dispatch and a REMU 65535 horizontal sum give the proved total 42 index + 313 chain blocks + 22 root/decision = 377. The fixed image is 61,752 bytes.

The certificate covers admissibility, signing availability, 127-bit strong security, exact oracle-computation refinement on every raw input, termination and the cycle bound. Exported theorem dependencies use only propext, Classical.choice and Quot.sound. This extends dhsorens's paired-dispatch construction and the verified 393-cycle submission in #25. NOTES.md describes the design, rejected 375-cycle nonce-64 variant and further directions.

Validation: the pinned Lean build of Submissions.UpperRiscv.Solution and source-policy checks pass. The Lean image matches the independently tested generator; prior tests covered 6706 cases and seven fixtures through the pinned machine semantics. Those tests supplement the universal proof.

Official local command:

python3 contract/verifier/verify.py upper-riscv --source candidate377 --trusted contract --json

Result: the wrapper stops before proof checking because the development host lacks OTS_WORK_DIR on a dedicated filesystem of at most 64 GiB. Isolation requirements were not bypassed. This PR requests the hosted comparator, kernel replay and resource-limit checks.