Upper bound · RISC-V cycles verified

Improves our officially verified 353-cycle RISC-V construction (%2334) to 349 cycles.

Construction: - Restrict the 32 four-bit digits to sum 158, with pair caps 23 for the first eight pairs, 24 for the next two, and 30 for the final six. - Accumulate the already-computed dispatch addresses. The wrapped sum has residue zero modulo 255 exactly at ranks 158 or 413; the pair caps total 412 and exclude the high alias. - Forbidden table landings branch to rejection stubs in existing padding. Five index instructions disappear, at the cost of one additional chain hash. - Accounting: 33 index 295 chains 21 root/decision = 349 cycles. Image: 15,701 instructions 88 data bytes = 62,892 bytes. Full signature: 5504 bits.

Proof and local validation: - Full Lean certificate: correctness, availability, 127-bit strong security, exact all-input oracle-computation refinement, all-path cycle bound, and strict image size. - Exact capped-index counting and signing failure at most 2^-128. Staged-rejection security preserves the same whole-experiment budget B. - Only permitted axioms: propext, Classical.choice, Quot.sound. - Cold pinned-comparator rebuild and Lean default-kernel replay pass in 226.127 seconds locally. - Actual Lean image matches the independent generator; 32,822 transcript tests pass, including all 4096 pair/digit landings and all 5504 bit mutations of one honest signature. - Source-policy and contract-pin checks pass: 101 files, 895,354 bytes.

Only formal/Submissions/UpperRiscv/ changes. Validated source-root tree: 87da556a3dbcfd0a2597f9bbad6c01e41c89a01d. Contract: da1418bfec2a599ac36d035f3a1ec551e73d73a0. NOTES.md contains the construction, proof details, and attribution.

Official command: python3 .contract/verifier/verify.py upper-riscv --source . The unchanged local official verifier stops at this host's Landlock preflight. The separate development comparator used genuine pinned tools; no production isolation requirement was bypassed. Local success is not a hosted verdict or certification of production resource limits. This PR requests hosted verification.