Upper bound · RISC-V cycles verified

This lowers the RISC-V bound to 360 cycles by a four-chain change to dhsorens's 364-cycle ascending cell grid (#28), which extends the 372-cycle dense dispatch (#27) and the constructions it credits. (Our 362 in #29 uses a different, non-grid layout; this one builds on the grid.)

Idea

In the 364 image every chain k writes its 32-byte answer block at outAddr k = cell k − 8. A chain is "on the grid" (no move, no redirect) when its wire value starts exactly at its cell. But a hash reads its input from x10, which has no alignment requirement — only the output pointer x12 must be 8-aligned. So any wire value that lies inside its own chain's block can be hashed in place with input offset j = x10 − x12, provided the other bytes of the block are dead when the chain runs.

In the 364 wire the last 152-bit value of each 96-byte group sits at group offset 77, i.e. five bytes above its own cell. Those four chains (execution 7, 11, 15, 19) are hashed in place with j = 13: x12 = outAddr k as before, x10 = outAddr k + 13, next state = answer bytes [13, 32). The 13 bytes below the state are the previous chain's discarded top 8 bytes and already-read wire bytes, so no unread input and no committed root byte is overwritten. Each of these chains drops its expansion hash's redirect (ADDI x10, x12, 8); the hash itself stays (it is the chain's +1). Root input, wire, rows and dispatch are unchanged: every chain still commits answer bytes [0, 24) at outAddr k.

Accounting

40 (index) + (189 hashes + 64 pointer + 12 redirects + 32 dispatch + 2 width changes = 299) + 21 (root, 12 blocks, and decision) = 360. Image 12340 instructions + 104 data bytes = 49464 bytes, as in #28.

Proof changes

Names.truncOff (bit 104 for the four chains, 64 otherwise) and trunc at that offset; a general counting lemma Values.card_filter_extract_le (a fixed window at any offset), through which card_filter_trunc_le' goes; MixedProgram.expands/work, with the machine invariants stated at work k and every per-chain fact checked by kernel decision; cost 299 in MixedCost/MixedPhase. Security constants are unchanged. See NOTES.md.

Validation

• Before the push, a Python port of the edited image definitions reproduced the 364 image exactly, checked every new kernel table fact, and a pinned-machine emulation measured 360 = 40/299/21 on every accepting run (364 = 40/303/21 for the unmodified port) with byte-provenance replay over 202 digit vectors.
• The Lean certificate builds and passes the stub statement, axiom check (propext, Classical.choice, Quot.sound) and the pinned comparator ("Your solution is okay!") on a CI mirror of the verifier against core da1418b: https://github.com/scaraven/ots.golf-submissions/actions/runs/35855600733 (commit 2bcf47a; this PR's root is identical except NOTES.md).
• This PR requests the hosted check.