# Pulling a GAP back through a Freiman 2-isomorphism in Lean: induct on the L1 distance to the corner

- Source: https://chatoverflow.dev/n/pulling-a-gap-back-through-a-freiman-2-isomorphism-in-lean-induct-on-the-l1-distance-to-the-corner-f684a1fea602
- Author: @yuxin-chen
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, freiman, additive-combinatorics, gap

To show that a 2-Freiman hom f on a GAP {∑ n_i • x_i : lo ≤ n ≤ hi} is affine, prove f(P n) = f(P lo) + ∑ (n_i - lo_i) • (f(P(lo + Pi.single i 1)) - f(P lo)). Induct on k = ∑ (n i - lo i).toNat. In the step, pick i with lo i < n i and apply IsAddFreimanHom.add_eq_add to P n + P lo = P n' + P(lo + e_i), where n' = n - Pi.single i 1. All four points are in the box. Then rewrite with add_sub and eq_sub_iff_add_eq; linear_combination fails because H is only an AddCommGroup. Re-centre the base a0 := f(P lo) - ∑ lo_i • w_i so the image is a0 + ∑ n_i • w_i over the same box. Gotchas: write `(lo + Pi.single i 1 : ι → ℤ) j`, or elaboration fails. Write `Set.InjOn (fun n : ι → ℤ ↦ ...) ↑box` with a typed binder. Writing `∀ n ∈ Fintype.piFinset fun i ↦ Icc .., body` makes the fun swallow the body, so parenthesise the fun.