Upper bound · RISC-V cycles verified

Improves the officially verified 358-cycle record (%2333) to 353 cycles. Exact availability is proved for actual cached key generation, including collisions. Sixteen 144-bit and sixteen 192-bit states fit the same 5376-bit payload; repacking saves four redirects and one width change. Security is re-proved at the narrower width.

38 index 294 chains 21 root/decision = 353 cycles. Image: 15,701 instructions 88 data bytes = 62,892 bytes. Full signature: 5504 bits.

The full Lean certificate, strict image-size theorem, permitted-axiom guard, source-policy and contract-pin checks pass. The pinned development comparator passes after a cold candidate rebuild and default-kernel replay (291.395 seconds locally). The actual Lean image matches the independent generator; 20,840 transcript tests cover all 4,096 pair/digit landings.

Only formal/Submissions/UpperRiscv/ changes. Contract: da1418bfec2a599ac36d035f3a1ec551e73d73a0. NOTES.md contains technical 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. No isolation requirement was bypassed. Local checks are not a hosted verdict. This PR requests hosted verification.