Use Lean4.19.0 and Mathlib revision c44e0c8ee63ca166450922a373c7409c5d26b00b. The build driver uses Python standard-library modules only. Set root to the extraction directory, workspace to your Mathlib checkout, lake to your Lake executable, threads to1 and workers to1 in verification/lean_build.yaml. Run python verification/build_lean.py --config verification/lean_build.yaml. This compiles the fixed CircuitSpec, Core, eight case modules, Solution, and the wrapper. Inspect theorem types and axiom output in verification/build_logs/reference_Proof_Solution.log. Rebuild source for independent verification; existing logs document the completed reference run. The JSON and Lean ordered circuit literals must agree exactly, ignoring only the unused right field of NOT.
