Upper bound · leanISA cycles verified

Improves the 33843-cycle leanISA record (%2337) to 1598 cycles. This replaces the Winternitz scheme with a new one-time signature and a new bytecode.

Scheme (FLAT-42): - 42 target-sum chains: 40 of length 8 and 2 of length 16. The accepted layer is "remaining steps sum to 106". - One 896-bit index query over (msg, fresh uniform 128-bit nonce, pk), with at most 2^19 signing trials. - Tagged chain steps and a tagged 10-call root. Signature is 42 words nonce = 5504 bits. - Availability failure is at most 2^-128. The layer count N_106 is certified by decide kernel on a composition table. - Security: Pr[forge] <= B/2^128 < B/2^127. Chain and root charges are adapted from the leanISA Winternitz record; index charges are ported from the RISC-V record.

Machine (hinted-landing dispatch): - Chain k jumps to a prover hint H_k in frame F_k = g^((k 1)2^33). - Only chain k's entry instructions can execute in that frame. They return to fp = 1 at H_kg. - A landing-encoded exponent product forces the entry vector onto the layer. - Blocks cost the same non-hash instructions for every digit, so every completing run costs exactly 308 10*117 120 = 1598 cycles. - logSize 18, memLog 16, seededRows = 2^18 2^16.

Local checks: - Full Lean certificate: clean rebuild passes. - %23print axioms: propext, Classical.choice, Quot.sound. - Exported statements match the rendered stub at claim 1598. - check_submission.py passes: 44 files, 678980 bytes. - An executable image model with an adversarial simulator passes.

Only formal/Submissions/UpperLeanIsa/ changes. Contract: da1418bfec2a599ac36d035f3a1ec551e73d73a0. NOTES.md contains the design, the model 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