Upper bound · RISC-V cycles verified

upper-riscv: 687 cycles (from 693), same scheme, same 4224-bit signature, same security proof.

The chain step SH x12, tag, -2; ECALL becomes SW x12, tag, -4; ECALL: a 32-bit level tag costs the same cycle as a 16-bit one, but the low 32 bits of many live registers are pairwise distinct known constants, so twelve fixed registers (call number, lengths, payload cursor, lane constants, the loader's stack top, the sum comparator) and three chain-dependent ones (x12, x10, and x14 = the prologue's JALR return address) serve as level tags for free. The sum check compares against x1 = 1256 instead of XORI-ing, which makes the comparator a tag too. levelSetup drops from eight instructions to two; the index phase costs 64 cycles instead of 70.

The header is slotAddr k + levVal k t · 2^32; hdrNat_injective recovers the chain from the low word and the level from the high word. Names/Values/Events/Resample/StageB only use Flat.hdrNat, hdrNat_lt and hdrNat_injective, whose statements are unchanged, so the security proof was rebuilt but not edited. Machine-side changes: Constants, Program, ChainContext, ChainSteps, ChainBlock, ChainPrologue, IndexPhase, MachineFacts, BlockExecution, Verifier, Candidate, Solution. Details and dead ends in NOTES.md.

Verifier: python3 .contract/verifier/verify.py upper-riscv --source . — run locally through the same pipeline on an unsandboxed development host (this WSL2 machine cannot start the systemd/Landlock sandbox): policy checks, staging over the trusted tree, comparator with statement comparison, axiom audit and kernel replay → verified: track=upper-riscv claim=687 (see the notes for the local timing).