Reproducibility archive for "A deterministic sin2-type algorithm for complex cubic irrationalities with exact periodicity certificates"

Reproducibility archive (v5.2) for the paper above. Contents: the deterministic engine and unit tests; per-experiment scripts, seeds and raw CSV tables; a pinned environment (environment.yml, environment.lock.yml, Dockerfile; Python 3.11, PARI/GP 2.17.x via cypari2, mpmath >= 1.4); a portable verifier (verify_all.py, stdlib only, ~2 s) which hash-checks every shipped table and recounts the main headline numbers of the paper; and a staged entry point (make_all.py) whose --mass target regenerates the Section 3 tables byte-identically from the 205 input polynomials. See README.md and PROTOCOL.md inside the archive. Archive SHA256: 4fbc7e9b648ce86c65958a81cf44b1055a79ab072bd686ade6e4fafa4afe16db Changelog v8: adds (i) the exact replay of all 205 mass-campaign trajectories (2265/2265 transition steps confirmed by exact comparisons in Q(alpha), 14 exact ties, zero discrepancies) with the selection-rule variant probe; (ii) an exhaustive box campaign over [-3,3]^3 (194 polynomials forming 97 mirror pairs, 194/194 unit certificates, 840/840 steps exact-replayed, 50 exact ties); (iii) a state-level cycle-identity certification of all 457 deformation runs (exact projective-state comparison modulo rotation, 457/457, no disagreement with the digit-level criterion). verify_all.py extended accordingly (26 new checks). Changelog v6: two third-party full-text files (used for literature comparisons) were replaced by minimal factual data stubs (scripts/literature_data/); internal report templates and paths were cleaned up; all archive documentation is now in English. Changelog v9: adds a self-contained Lean 4 formalization layer under lean/(kernel-only sealed theorems for the plastic transition graph, pinned toolchain, recorded axiom audit, replay instructions; no mathlib needed, replays in minutes). verify_all.py extended with Lean-layer integrity checks, a CSV-to-Lean transition-table bridge (2285/2285), and an automatic recount of the new EXP38 package (the manuscript's 120-step per-candidate score decomposition, now shipped with tests and provenance). Adds the manuscript's figure scripts (single replayable generator), a LICENSE (CC BY 4.0), and a Lean row in CLAIMS_MAP. Secondary per-experimentmanifests regenerated against the shipped tree.Archive SHA256: 72808bae53ff2eb936ce33604d466c9bef2968f24b4dc7c213279ad390ab7cb2