Upper bound · leanISA cycles verified

1096-cycle leanISA construction: 106 ordinary instructions 87 BLAKE2S calls × 10 120 public-boundary cycles. Every completing execution has 193 instructions. This is fourteen cycles below our complete 1110-cycle ancestor. The signature remains 5504 bits, including the full 128-bit nonce; there are 327680 seeded rows.

The construction combines a linear security potential, mixed four- and five-child binding packets, four internal child chains, and unequal alias multiplicities within cost bands. Exact kernel-checked multiplicative counting connects the actual 127-bit codec to all 440 security tiers. Composing the last two counting profiles and certified prefix caching reduce proof-checking cost without changing the construction.

The complete Certificate 1096 covers admissibility, 127-bit strong security, bytecode validity, honest-prover faithfulness, soundness against arbitrary committed images at every allowed memory size, and the universal cycle bound. The separate seeded_rows theorem is included. Competition definitions and rules are unchanged.

Local validation passed: clean build (423.679 s), exact exported statement/primitive comparison, permitted-axiom dependency audit, and fresh unchanged Lean kernel replay of 62151 declarations (695.624 s for replay; 743.160 s for the entire comparison/replay process). Root policy passes: 142 files, 4151624 bytes.

Timing warning: measured required standalone build/export/check stages total 1187.366 s (19m47s), only about 13 seconds below the 20-minute limit. This is not an official end-to-end measurement; hosted timeout remains a material risk. Peak sampled PSS was about 17.5 GiB during the build, not a hosted cgroup measurement.

The official local Linux driver fails closed because this host lacks Landlock; no sandbox requirement was bypassed. This PR requests hosted verification, not recognition of a prior hosted verdict.

Only formal/Submissions/UpperLeanIsa/ changes. NOTES.md records the construction, failed approaches, exact proof engineering, validation limits and credits. Checked source commit: 160c0512643ce48ae0de583bce2de1b0c46d6b5c. Pinned contract: ca67ddc3fc9db8272fddedc3e739af59bd09fb90.