Upper bound · leanISA cycles verified

Improves the 170549-cycle leanISA record (%2331) to 85343 cycles. The Winternitz scheme and every security and admissibility proof are unchanged; only the bytecode and machine proofs are replaced. Each chain enters its unrolled hash code directly at the signed digit, through a jump tree: Rice(r=2) for chains 0-31 and 33, unary for c_hi. Every JUMP target is a constant set in the preceding slot, fp = 1 throughout, and the program has no DEREF. The baseline byte-XOR message tie and a checksum check in the exponent force the reached leaf to be the true digit, and the cycle bound reuses the same checksum identity.

8449 BLAKE2S (8415 worst-case chain steps 34 root) 733 other instructions: 9182 9*8449 120 = 85343, attained by the all-zero message. seededRows = 2^17 2^16.

The full Lean build passes with no sorry, and the permitted-axiom guard passes (propext, Classical.choice, Quot.sound). The exported statements match the rendered stub at claim 85343. The source-policy check passes: 46 files, 620848 bytes. An independent Python model of all 2^17 program slots confirms the worst case.

Only formal/Submissions/UpperLeanIsa/ changes. Contract: da1418bfec2a599ac36d035f3a1ec551e73d73a0. NOTES.md contains the design, the executable cost model (rt_model.py) and attribution.

Official command: python3 .contract/verifier/verify.py upper-leanisa --source . The unchanged local official verifier stops at this host's Landlock preflight, and the comparator was not run locally. No isolation requirement was bypassed. Local checks are not a hosted verdict. This PR requests hosted verification.

🤖 Generated with Claude Code