theorem Q2Presentation.Lifting.sub_eq_add_char2 {M : Type} [AddCommGroup M] [Module (ZMod 2) M] (a b : M) : a - b = a + b

char-2 subtraction is addition.

theorem Q2Presentation.Lifting.heisEval_e_dual {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) : (heisEval Φ q n φ w).e = foxShadowGen (dualFamily Φ).op q φ w

The dual coordinate is the dual-family row shadow.

theorem Q2Presentation.Lifting.foxShadowDualGen_eq {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (φ : Gen → Module.Dual (ZMod 2) V) (w : GExpr) : foxShadowDualGen Φ q φ w = foxShadowGen (dualFamily Φ).op q φ w

The dual Fox shadow is the dual-family row shadow.

theorem Q2Presentation.Lifting.dualOp_eq_one_of_op_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (h : Φ.op y = 1) : (dualFamily Φ).op y = 1

Relator triviality transports to the dual family.

theorem Q2Presentation.Lifting.betaShadow_descend {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (n : Gen → V) (e : Gen → Module.Dual (ZMod 2) V) (he : ∀ (g : Gen), W ≤ LinearMap.ker (e g)) (w : GExpr) : betaShadow (Φ.descend W hW) q (fun (g : Gen) => W.mkQ (n g)) (fun (g : Gen) => W.liftQ (e g) ⋯) w = betaShadow Φ q n e w

β-descent: the cup coordinate factors through the quotient for annihilator-valued dual tuples.

theorem Q2Presentation.Lifting.betaShadow_restrict {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (m : Gen → ↥W) (e : Gen → Module.Dual (ZMod 2) V) (w : GExpr) : betaShadow Φ q (fun (g : Gen) => ↑(m g)) e w = betaShadow (Φ.restrict W hW) q m (fun (g : Gen) => e g ∘ₗ W.subtype) w

Restriction form of β-naturality.

theorem Q2Presentation.Lifting.cupForm_descend {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (n : Gen → V) (e : Gen → Module.Dual (ZMod 2) V) (he : ∀ (g : Gen), W ≤ LinearMap.ker (e g)) : (cupForm (Φ.descend W hW) q (fun (g : Gen) => W.mkQ (n g)) fun (g : Gen) => W.liftQ (e g) ⋯) = cupForm Φ q n e

cupForm descends for annihilator-valued dual tuples.

theorem Q2Presentation.Lifting.cupForm_dual_coboundary_floor {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W : Submodule (ZMod 2) V) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → V) (lam : Module.Dual (ZMod 2) V) (hlamW : ∀ c ∈ Subgroup.closure (Set.range q), ∀ x ∈ W, lam ((Φ.op c) x) = lam x) (h1 : foxShadowGen Φ.op q n Q2Word.tameRelator ∈ W) (h2 : foxShadowGen Φ.op q n Q2Word.wildRelator ∈ W) : (cupForm Φ q n fun (g : Gen) => (dualOp Φ (q g)) lam + lam) = lam (foxShadowGen Φ.op q n Q2Word.tameRelator + foxShadowGen Φ.op q n Q2Word.wildRelator)

The χ-formula: a dual coboundary pairs with floor-window tuples by the closure-invariant-restriction value of the row sum.

theorem Q2Presentation.Lifting.cupForm_kernel_dual_coboundary {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → V) (hn1 : foxShadowGen Φ.op q n Q2Word.tameRelator = 0) (hn2 : foxShadowGen Φ.op q n Q2Word.wildRelator = 0) (lam : Module.Dual (ZMod 2) V) : (cupForm Φ q n fun (g : Gen) => (dualOp Φ (q g)) lam + lam) = 0

Dual coboundaries pair to zero with row-kernel tuples.

theorem Q2Presentation.Lifting.cupForm_coboundary_dual_cycle {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (a : V) (φ : Gen → Module.Dual (ZMod 2) V) (hc1 : foxShadowGen (dualFamily Φ).op q φ Q2Word.tameRelator = 0) (hc2 : foxShadowGen (dualFamily Φ).op q φ Q2Word.wildRelator = 0) : cupForm Φ q (coboundary Φ q a) φ = 0

Coboundary tuples pair to zero with dual-family cycles.