theorem Q2Presentation.Lifting.famRows_image_of_diamond {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] (htwo : 2 ∣ Nat.card Yt.Y) (h4Y : 4 ∣ Nat.card Yt.Y) (hx1LY : q Gen.x1 ∈ Yt.LY) (hdecomp : ∀ (y : Yt.Y), ∃ w ∈ Subgroup.closure {q Gen.sigma, q Gen.tau}, y * w⁻¹ ∈ Yt.LY) (hrel : rconj (Yt.piY (q Gen.tau)) (Yt.piY (q Gen.sigma)) = Yt.piY (q Gen.tau) ^ 2) (htame : Φ.op (Q2Word.tameRelator.eval q) = 1) (hwild : Φ.op (Q2Word.wildRelator.eval q) = 1) (hfaithNT : ∀ (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W'), W' < W → (∀ U < W, W' ≤ U → (∀ (y : Yt.Y), ∀ m ∈ U, (Φ.op y) m ∈ U) → U = W') → (¬∀ (y : Yt.Y), (sectionFamily Φ W' W hW hW').op y = 1) → dualPairingFaithful (sectionFamily Φ W' W hW hW') q) (u v : V) : u + v ∈ markedAug Φ q → ∃ (n : Gen → V), (famRowsMap Φ q) n = (u, v)

The diamond image: pairs whose sum lies in the marked window are hit by the rows — diamondAtW_all at the top window, no fullness hypothesis.