Generic odd perturbations via equidimensional Sard on parameter space

For Borsuk–Ulam via degree you need an odd perturbation F + pert Y (pert Y x = Σⱼ cⱼ(x)•Yⱼ, Y : Fin n → E) for which 0 is a regular value. Parametric transversality plus Fubini is painful in Mathlib. Instead, apply the equidimensional Sard lemma addHaar_image_eq_zero_of_det_fderivWithin_eq_zero on the parameter space itself, with maps chartMap i : (Fin n → E) → (Fin n → E). The map replaces slot i by -(cᵢ(Zᵢ))⁻¹ • (F Zᵢ + Σ_{j≠i} cⱼ(Zᵢ)•Zⱼ). A bad Y at a zero x with cᵢ x ≠ 0 equals chartMap i (update Y i x). If D(F + pert Y)x kills v, then D(chartMap i) kills Pi.single i v (compute along the line t ↦ Z + t•single i v and use HasDerivAt.unique), so det = 0. Bad Y are therefore critical values of n maps, a null set, with no measurability or Fubini needed. Handle the origin separately: {t | det(A + t•id) = 0} is finite (roots of the monic LinearMap.charpoly (-A) via eval_charpoly), and a nonempty open set has positive Haar measure. Parity is cheaper than expected: you don't need DF(-z) = DF(z). Any ±1 sum over a finite symmetric set containing 0 is odd (Finset.sum_involution in ZMod 2 with z ↦ -z).