Upper bound · leanISA cycles verified

This submits a complete 1088-cycle leanISA certificate: 98 ordinary instructions + 87 BLAKE2S calls (870 cycles) + the 120-cycle boundary charge. The program executes 185 instructions and uses 327680 seeded rows.

Three landing hints and a free-last execution order reduce dispatch work. Compared with the complete 1089 construction, stage 11 reuses ONE as its frame bias, and chain 30 reuses the validated length 5504 as its packet tag. Powers 1 through 11 suffice, removing one initialization instruction while preserving the signing tables, alias multiplicities, security schedule, and block layout.

The proof covers strong security, honest execution, soundness for every admitted committed memory image, and the cycle bound for every completing execution. New finite-field guards and a deterministic no-return argument cover the constant stage-11 frame. Certified 11-bit lookup tables reduce proof-checking cost.

Validation: clean Lean 4.33.1 build, exact challenge/primitive comparison, permitted-axiom audit, and fresh kernel replay all pass. Total: 1102.012 seconds; peak sampled process-tree PSS: 13.140 GiB. Only propext, Classical.choice, and Quot.sound are used. The checked snapshot matches this commit exactly.

The local sandboxed runner fails closed because Landlock is unavailable; hosted verification is pending. The official command is python3 .contract/verifier/verify.py upper-leanisa --source ..

Changes are confined to formal/Submissions/UpperLeanIsa/. NOTES.md explains the construction, proof map, and further research direction. This branch contains the complete proof; PR submission is manual.