seanculm-maker/macaday_physics_lean: v1.0 — Machine-verified Lean 4 results accompanying eight-paper submission batch

First archived release of macaday_physics_lean: 38 Lean 4 modules, zero sorry, machine-checked against Lean v4.29.1 and the pinned Mathlib revision (lean-toolchain / lake-manifest.json). This version accompanies the papers W, R, M, T, C, F1, V, and Z as cited in each paper's Data and Code Availability section; see README.md for the per-paper module table. Build: lake exe cache get && lake build. Core results are verified on kernel-standard axioms (propext, Classical.choice, Quot.sound); finite lattice sums in E8Moments / D8Moments use native_decide, as disclosed in the citing papers.