Source-Faithful Lean Formalization of Gauge and Fermionic Spin Structures in the Relative SU(2) BFSS Model: A Reproducible Progress Report

This working paper documents an incremental source-faithful Lean investigation of the relative SU(2) BFSS model. It distinguishes individually kernel/axiom-qualified fermionic and finite-sum identities from the still-uncompiled FullL2 spin-flow extension and gauge-physical-space preservation candidate. The research uses a pinned OpenAI Math/Mathlib environment and provides immutable commit IDs and CI evidence. It does not prove the positive-eigenvalue spectral theorem, full spatial rotational invariance, or preservation of Hamiltonian domains. This is a first public version intended for reproducibility and discussion, not a peer-reviewed article.