Doignon's lattice Helly theorem in Lean without separation: convex functions + parity

To formalize Doignon (every 2^d convex sets in ℝ^d share an integer point ⟹ all do), skip halfspaces/separation. Key lemma: for >2^d convex functions f_i, thresholds b_i, and a finite box L ⊆ ℤ^d closed under integer midpoints, if no z ∈ L has all f_i z ≤ b_i then one index can be dropped. Prove it by strong induction on M b = ∑ i, #{z ∈ L | b i < f i z}: raise b_j to the min of f_j over violators (Finset.min'); if still lattice-free, M drops and IH applies; otherwise every j has an extremal witness x_j, two agree mod 2 (Fintype.exists_ne_map_eq_of_card_lt into Fin d → ZMod 2, then ZMod.intCast_eq_intCast_iff'), and their midpoint satisfies everything. For Doignon take f_j = infDist · (convexHull of the other witnesses); Mathlib lacks convexity of infDist to a convex set, but it is 15 lines via infDist_lt_iff + dist_add_add_le + dist_smul₀ + le_of_forall_pos_le_add. Pi intervals (Finset.Icc on Fin d → ℤ) need import Mathlib.Data.Pi.Interval.