fv: machine-check all 104 chip determinism theorems in Lean

[eigmax]

Summary

Every core chip with a determinism statement (57 chips, 104 theorems) is machine-checked in Lean 4: for each, #print axioms lists only propext, Classical.choice and Quot.sound (no sorry, no added axiom). The statements exposed three soundness gaps, now closed in the constraints (#534, #535, #536).

• Determinism replay (crates/fv/picus): the analyser's derivation of every output column is replayed as Lean step lemmas; gadget summaries (field operations, byte comparison, leading-one, canonical word, septic chord/sqrt) are library theorems proved once, and accelerator snippets are generated per chip by family generators, shipped in the archive below. The propagation maps are BTreeMaps, so generation is deterministic.
• Regeneration and parallel check: regen_all.sh (regenerates every chip file and the 24 generated snippets, byte-identical across runs) and check.sh (splits a chip file into dependency-ordered modules, rewrites the large proofs, and builds them in parallel under a 30-minute cap per module) are not in this PR; they and the snippet generators ship in the archive below (src/crates/fv/lean4/check, src/crates/fv/lean4/snippets/tools) and land in a follow-up PR. The chip files are generated, so they are no longer committed.
• Paper (docs/paper): one arithmetisation section (frame, buses and chips); "Putting it all together" after the components, with an end-to-end block-proof protocol; one Security section (proved relation and open hypotheses, soundness accounting, composition, key binding, digest assumption, trace uniqueness, conformance and determinism, post-quantum); six review passes.
• Toolchain: pinned to nightly-2026-09-17, the date of the latest zkm toolchain release; the lints it adds are fixed (recursion limit in zkm-curves and zkm-core-machine, two index loops in zkm-pcs).
• Other: the PLONK verifier template defines VK_ROOT() and keeps hashPublicValues' doc comment; SysLinux and the Global gadgets gain doc comments and analyser marks only; README drops the AI-assistant acknowledgement. No AIR, verifying key or recursion program changes.

The checked chip files and snippets, with a per-chip table (STATUS.md, CLOSED.txt), are archived at https://zkm-toolchain.s3.amazonaws.com/fv/ziren-fv-lean-20261001b.tar.gz (.sha256 beside it); BASE_COMMIT.txt names this commit.

Test plan

• regen_all.sh run three times: chip files and snippets byte-identical across runs.
• Every chip file checked with check.sh on one 124-core machine: 104/104 deterministic theorems with standard axioms only; all 7,414 modules of the 62 chip files build with rc=0 and no sorry; slowest module 1,300 s under the 30-minute cap. The archived files are the ones checked.
• CI test job on the self-hosted box with nightly-2026-09-17: fmt, clippy (workspace and ark), the twelve-package cargo test -r loop, zkm-picus tests, zkm-core-machine cost and Weierstrass tests, verifier malformed-input tests under both feature sets — all passed.
• Paper builds with no errors, undefined references or overfull boxes (60 pages); seven review passes.