theorem Q2Presentation.Lifting.sum_expSum_famSingle {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (c : Gen → ZMod 2) (a : Gen) (x : V) : ∑ g : Gen, c g • famSingle a x g = c a • x

Exponent-sum collapse on single-slot tuples.

theorem Q2Presentation.Lifting.foxShadowGen_relative_fixed {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W'' W : Submodule (ZMod 2) V) (hst : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (htriv : ∀ (y : Yt.Y), ∀ x ∈ W, (Φ.op y) x - x ∈ W'') (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → V) (hn : ∀ (g : Gen), n g ∈ W) (w : GExpr) : foxShadowGen Φ.op q n w ∈ W ∧ foxShadowGen Φ.op q n w - ∑ g : Gen, expSum g w • n g ∈ W''

The relative fixed-shadow lemma: shadows of window-valued, relatively fixed tuples stay in the window and are exponent-sum diagonals modulo the floor.

theorem Q2Presentation.Lifting.reach_of_relative_witness {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) (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) (hwitness : ∀ (W : Submodule (ZMod 2) V), (∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) → ∀ (w : V), (∀ (y : Yt.Y), (Φ.op y) w - w ∈ W) → w ∉ W → ∃ (n : Gen → V), foxShadowGen Φ.op q n Q2Word.tameRelator - w ∈ W ∧ foxShadowGen Φ.op q n Q2Word.wildRelator ∈ W) (W : Submodule (ZMod 2) V) : (∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) → famReach Φ q W

Window reach from relative witnesses: with the frame data and the relative-witness hypothesis, every stable window's targets are hit.