Upper bound · leanISA cycles verified

Completes the leanISA Winternitz baseline drafted in #23 by @TomWambsgans and claims 170549 cycles on upper-leanisa (first entry on this track). Tom's four commits are kept with their authorship; only formal/Submissions/UpperLeanIsa/ changes.

Scheme: unchanged from #23 (Algorithms.lean): 34 chains of 128-bit words, 32 base-256 message digits plus two checksum digits, chain steps tagged with chain id and position, an MD-style root fold with distinct metadata, and every query in the exact 896-bit BLAKE2S shape.

What this PR adds - secure (Security.lean): #23's ingredients (records, exposure/hidden partition, resampling, hidden-word and second-preimage charges) assembled in two stages. Stage A is a supermartingale over public-data fibers via master_family. Stage B uses identical-until-bad on the exposed run, plus a cut-relative forgery lemma (Events.events_stB): an accepted fresh pair is either a hidden-word hit or a cut-target hit. There are two charges of 2⁻¹²⁹ per compression, so the bound is probTrue ≤ B/2¹²⁸ < B/2¹²⁷. Key generation is bridged to a uniform average over records in KeygenBridge.lean. - Bytecode (MachineProgram.lean): straight-line code with fp = 1 throughout and a single final JUMP to the sentinel. - Each chain executes all 255 steps. A thermometer mux feeds in the signature word at the signed digit; earlier positions hash that word as dummies. - Digits are tied to the pinned message cells by XOR-accumulating shifted byte constants. - The checksum is checked through powers of g: g^C = g^(256·c_hi) · g^(c_lo). - 92093 instructions, 8704 BLAKE2S. - Cycles (MachineRun.lean): every completing run executes exactly those instructions on every answer path. Cost is 92093 + 9·8704 = 170429, plus the 120-cycle boundary charge, for 170549. - Sound / Faithful (ConstraintMath, MachineProver, MachineSound, MachineFaithful): - The constraints force the verifier's digits, chain values and root on any committed image, at any admissible memory size. - The honest prover's image satisfies every constraint exactly when the verifier accepts. - seeded_rows: 2^17 + 2^17 < 2^20.

It is a deliberately simple baseline, not a cycle-optimised one.

Validation: on a private CI mirror of the hosted verifier, run against the pinned contract da1418bf, this exact root passed every step: - policy check; - lake build Submissions.UpperLeanIsa.Solution; - stub statements and axioms (only propext, Quot.sound, Classical.choice); - comparator with kernel replay.