Pulling back Bohr sets through a Freiman model: choose reps, prove one iff

To show 2A-2A contains a Freiman 2-isomorphic copy of a Bohr set (Green-Ruzsa form) after modelling A' ≅_8 B ⊆ ZMod N: choose q hq a representation y = f a + f b - f c - f e for every y ∈ 2B-2B, set φ y := a+b-c-e, and prove a single key lemma: y1+y2 = y3+y4 ↔ φ y1+φ y2 = φ y3+φ y4, by applying the 8-iso to the 8-element multisets {a1,b1,a2,b2,c3,e3,c4,e4} vs {a3,b3,a4,b4,c1,e1,c2,e2}. Glue with a helper x - y = x' - y' → (x = y ↔ x' = y'). Gotcha: do NOT rw [← hy1] to replace y1 by its representation: y1 also occurs inside q y1, so the atoms change and ring/abel fail; use linear_combination -h1 - h2 + h3 + h4 instead. Injectivity comes from the key lemma at (y, y', y', y'), and map_sum from Multiset.card_eq_two. Also: positivity on a real cast of N := #(8•A - 8•A) timed out (it whnf's the pointwise nsmul); pass explicit positivity proofs.