def Q2Presentation.Lifting.augSubmodule {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) : Submodule (ZMod 2) V

The augmentation submodule: the span of all operator differences.

Equations

• Q2Presentation.Lifting.augSubmodule Φ = Submodule.span (ZMod 2) {x : V | ∃ (y : Yt.Y) (v : V), (Φ.op y) v - v = x}

theorem Q2Presentation.Lifting.op_diff_mem_aug {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (v : V) : (Φ.op y) v - v ∈ augSubmodule Φ

theorem Q2Presentation.Lifting.mem_augSubmodule_of_gen {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (g : Gen) (v : V) : (Φ.op (q g)) v - v ∈ augSubmodule Φ

theorem Q2Presentation.Lifting.eval_mem_closure {Yt : BoundaryFramedTarget} [Finite Yt.Y] (q : Marking Yt.Y) (w : GExpr) : w.eval q ∈ Subgroup.closure (Set.range q)

Evaluation values lie in the marked word closure.

theorem Q2Presentation.Lifting.foxShadowGen_sub_expSum_mem_aug {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) (w : GExpr) : foxShadowGen Φ.op q n w - ∑ g : Gen, expSum g w • n g ∈ augSubmodule Φ

Shadows are exponent-sum diagonals modulo AUG (bare-hands traced Stokes).

theorem Q2Presentation.Lifting.rows_sum_mem_aug {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) : foxShadowGen Φ.op q n Q2Word.tameRelator + foxShadowGen Φ.op q n Q2Word.wildRelator ∈ augSubmodule Φ

The traced Stokes constraint: the row map's coordinate sum lies in the augmentation window.

theorem Q2Presentation.Lifting.augSubmodule_eq_top {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (hinvY : ∀ (f : Module.Dual (ZMod 2) V), (∀ (y : Yt.Y) (v : V), f ((Φ.op y) v) = f v) → f = 0) : augSubmodule Φ = ⊤

Augmentation fullness: if no nonzero functional is invariant, AUG = ⊤.