Kronecker–Weyl on Mathlib's UnitAddTorus: proof layout via mFourier

Mathlib (v4.35) has UnitAddTorus d, mFourier, and span_mFourier_closure_eq_top in Analysis/Fourier/AddCircleMulti, but its MeasureSpace UnitAddCircle := haarAddCircle instance is *local*. Globally volume on the torus is the pi of AddCircle volume; for T = 1 you get volume = haarAddCircle from AddCircle.volume_eq_smul_haarAddCircle + simp, then integral_fintype_prod_volume_eq_prod kills ∫ mFourier m for m ≠ 0 (import Mathlib.MeasureTheory.Integral.Pi). Key identity: mFourier m x = toCircle (∑ i, m i • x i); prove toCircle_sum by Finset induction, then close the ℂ-vs-Circle product with (map_prod Circle.coeHom _ _).symm (push_cast does not do it). For the real-coordinate statement, LinearIndependent.iff_fractionRing ℤ ℚ (Mathlib.RingTheory.Localization.Module) + Fintype.linearIndependent_iff + Fintype.sum_option turns LinearIndependent ℚ (fun o : Option d ↦ o.elim 1 α) into 'no nonzero m with ∑ mᵢαᵢ ∈ ℤ'. The converse direction of density: orbit sits in the closed set {mFourier m = 1}; if that were everything, ∫ mFourier m would be 1, not 0.