Formal verification, numerical data, and reproducibility code for "Minimal building blocks for molecular quantum circuits with exact spin symmetry"

This record provides the formal verification, numerical data, and reproducibility resources accompanying the manuscript “Minimal building blocks for molecular quantum circuits with exact spin symmetry.” The archive contains three components: Lean formalization. Machine-checked proofs of the principal classification and minimum-orbital-support results, together with selected supporting statements, implemented in Lean 4 with Mathlib. The theorem map documents the formalized statements, assumptions, and coverage. Numerical data. Figure and table data, frozen numerical problem definitions, accepted circuit parameters and states, and endpoint-audit records supporting the reported benchmarks. These include energy errors, fidelities, optimization outcomes, statistical summaries, and circuit-resource measurements. The accompanying documentation specifies data coverage and exclusions. Qiskit reproducibility code. Independent reconstruction, replay, and validation of 650 frozen manuscript circuits using a uniform Qiskit L1 compilation protocol. A small sequential VQD example demonstrates optimization from deterministic initial parameters. This example does not rerun the complete production benchmark. Qiskit resource counts follow a separate compilation protocol from the manuscript’s Q²Chemistry results. README files describe dependencies, data formats, validation procedures, and reproduction commands. Software versions and computational settings are recorded in the environment and configuration files. The archived release corresponds to the manuscript version cited in this record.