Upper bound · leanISA cycles verified

Improves the 1390-cycle leanISA record (%2343) to 1281 cycles: 111 non-hash instructions 105 BLAKE2S*10 120. There are exactly 216 instructions on every completing execution.

Scheme: - 42 hash chains grouped into corner-simplex index fields: each field value ranks a tuple of chain positions. One free chain takes its digit from the conserved sum. - A 127-bit effective index from one 896-bit query, with a fresh uniform 127-bit nonce. The signature is 5503 bits. - 96 continuation hashes per accepted signature, and an 8-call root whose last call is tagged by its chaining state. - Strict 127-bit strong security, including adaptive index grinding with the B - K closure. - Availability failure <= 2^-128 at 2^19 trials. - Keygen 1326, signing <= 2^20, verification 210 compressions.

Machine: - Hinted-landing dispatch: each unit jumps to a prover hint in its own frame, and only that unit's entry instructions can execute there. - Field-rescaled frame and cost constants. - Every block has the same non-hash cost, so the step count does not depend on the index answer. - A landing exit whose hash-free identity forces the layer. - logSize 18, memLog 16, seededRows = 2^18 2^16.

Local checks: - Clean full Lean rebuild passes. - %23print axioms for certificate, seeded_rows and submission: propext, Classical.choice, Quot.sound. - Exported statements match the rendered stub at claim 1281. - check_submission.py passes: 52 files, 826599 bytes. - An executable image model with an adversarial simulator passes. - Three independent adversarial reviews passed.

Only formal/Submissions/UpperLeanIsa/ changes. Contract: f3b8747878bebd81b6684b8219fc96f797e7272d. formal/, challenges.json and protected.sha256 are identical to da1418b, against which it was also built. NOTES.md contains the construction, the proof changes and credits.

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