theorem Q2Presentation.Lifting.foxShadowGen_invariant_dual_collapse {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (f : Module.Dual (ZMod 2) V) (hf : ∀ (y : Yt.Y) (v : V), f ((Φ.op y) v) = f v) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → V) (w : GExpr) : f (foxShadowGen Φ.op q n w) = ∑ g : Gen, expSum g w * f (n g)

The invariant-dual collapse: a family-invariant functional sees any Fox shadow as the mod-2 exponent-sum combination of the tuple — foxShadowGen_relative_fixed at W := ⊤ with floor W'' := ker f.

theorem Q2Presentation.Lifting.foxShadow_invariant_dual_tau {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) (f : Module.Dual (ZMod 2) (NAdd E)) (hf : ∀ (y : Yt.Y) (m : NAdd E), f ((conjEndN E y) m) = f m) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → NAdd E) (w : GExpr) (hτ : expSum Gen.tau w = 1) (hσ : expSum Gen.sigma w = 0) (h0 : expSum Gen.x0 w = 0) (h1 : expSum Gen.x1 w = 0) : f (foxShadow E q n w) = f (n Gen.tau)

Scalar collapse at a τ-diagonal word: with the exponent-sum profile of the two relators, a conjugation-invariant dual sees the concrete Fox shadow as f (n τ).

theorem Q2Presentation.Lifting.rowMap_fst_invariant_dual {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) (f : Module.Dual (ZMod 2) (NAdd E)) (hf : ∀ (y : Yt.Y) (m : NAdd E), f ((conjEndN E y) m) = f m) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → NAdd E) : f ((rowMap E q) n).1 = f (n Gen.tau)

The first (tame) relator row collapses to f (n τ) under a conjugation-invariant dual.

theorem Q2Presentation.Lifting.rowMap_snd_invariant_dual {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) (f : Module.Dual (ZMod 2) (NAdd E)) (hf : ∀ (y : Yt.Y) (m : NAdd E), f ((conjEndN E y) m) = f m) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → NAdd E) : f ((rowMap E q) n).2 = f (n Gen.tau)

The second (wild) relator row collapses to f (n τ) under a conjugation-invariant dual.

theorem Q2Presentation.Lifting.rowMap_pair_invariant_dual {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) (f : Module.Dual (ZMod 2) (NAdd E)) (hf : ∀ (y : Yt.Y) (m : NAdd E), f ((conjEndN E y) m) = f m) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → NAdd E) : f (((rowMap E q) n).1 + ((rowMap E q) n).2) = 0

The rows diagonal: under a conjugation-invariant dual both relator rows agree (both are f (n τ)), so the sum of the two row values dies — the dual containment of the row image in the marked sum-line.