Upper bound · RISC-V cycles rejected

Chain k read its digit from byte k of the 256-bit index answer, so the 28 chains occupied bytes 0–27 and index word 3 (bytes 24–31) carried only four live fields. Extracting them needed two lane words — (3, 0) for bytes 24, 26 and (3, 1) for bytes 25, 27 — each with two dead lanes, plus a third mask constant 0x003C003C purely to zero those lanes.

Moving the digits of the last four chains to bytes 24, 26, 28 and 30 makes them all even, so the single lane word (3, 0) carries them in its four lanes under the ordinary broadcast 0x3C mask already held in x25 (chains 24–27 all have width 4). Lane words drop from eight to seven (4 + 6·5 = 34 instead of 4 + 7·5 = 39) and loadWords loses the 0x003C003C load:

55 (index) + 355 (chains) + 20 (root and decision) = 430, image length 890, data image 72 bytes.

Seven lane words is the floor — each chain needs its own 16-bit dispatch halfword, so 28 / 4 = 7.

The digit machinery is re-indexed by byte slot rather than by chain: wid has 32 slots, four of them (25, 27, 29, 31) of width zero, and chain k reads slot slotOf k = k + (k - 24). The widths are unchanged as a multiset (16 fives and 12 fours, Σ wid = 128), so compW, numValid, target = 215 and the whole availability chain come out identical, and zero-width slots are free in both compW and posW. PackFiber.lean/PackCount.lean keep their shape verbatim. On the lane side laneNat u 3 1 is identically zero, so dropping that lane word changes no arithmetic. indexLength falls from 67 to 61, shifting every tableEnd down 24 bytes; the JALR immediates run over [-1608, 1512], still inside 12-bit signed, so jumpBase is unchanged.

Full write-up in NOTES.md.

This development host cannot complete a local build of the root, so the root is offered for the official check; I expect to iterate on this PR if the checker finds a gap.