Upper bound · hinted RISC-V cycles verified

The view-length mask now supplies both the free-chain base and its displacement, removing one ADD and reducing the accepting bound from 317 to 316 cycles. Reserved rejection windows cover every other length bank; the larger image is 1,042,904 bytes, 5,672 bytes below the limit.

Accepting cost: 178 compressions + 138 ordinary instructions. The full Lean certificate, exact statement/primitive comparison, permitted-axiom check, fresh kernel replay of 22,494 declarations, source policy and 21,305 independent executions pass. Signatures remain 5504 bits. The official local runner stops at Landlock preflight on this development host, so hosted verification is pending.

Verifier command: .contract/verifier/verify.py upper-riscv-hint --source . Local result: stopped at Landlock preflight; the standalone checks above passed.