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

The marked augmentation: operator differences over the marked closure.

Equations

• Q2Presentation.Lifting.markedAug Φ q = Submodule.span (ZMod 2) {x : V | ∃ c ∈ Subgroup.closure (Set.range q), ∃ (v : V), (Φ.op c) v - v = x}

theorem Q2Presentation.Lifting.op_diff_mem_markedAug {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) {c : Yt.Y} (hc : c ∈ Subgroup.closure (Set.range q)) (v : V) : (Φ.op c) v - v ∈ markedAug Φ q

theorem Q2Presentation.Lifting.gen_diff_mem_markedAug {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 ∈ markedAug Φ q

theorem Q2Presentation.Lifting.markedAug_le_aug {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) : markedAug Φ q ≤ augSubmodule Φ

theorem Q2Presentation.Lifting.op_closure_invariant_of_gen {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (lam : Module.Dual (ZMod 2) V) (h : ∀ (g : Gen) (v : V), lam ((Φ.op (q g)) v) = lam v) (c : Yt.Y) : c ∈ Subgroup.closure (Set.range q) → ∀ (v : V), lam ((Φ.op c) v) = lam v

Generator-invariance extends over the marked closure.

theorem Q2Presentation.Lifting.kills_markedAug_iff {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (lam : Module.Dual (ZMod 2) V) : (∀ x ∈ markedAug Φ q, lam x = 0) ↔ ∀ (g : Gen) (v : V), lam ((Φ.op (q g)) v) = lam v

Killing the marked window is generator-invariance.

theorem Q2Presentation.Lifting.foxShadowGen_sub_expSum_mem_markedAug {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 ∈ markedAug Φ q

Marked shedding: shadows are exponent-sum diagonals modulo the marked window.

theorem Q2Presentation.Lifting.rows_sum_mem_markedAug {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 ∈ markedAug Φ q

The traced Stokes constraint, marked form: the row-map sum lies already in the marked window.

theorem Q2Presentation.Lifting.markedAug_eq_top {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hinvgen : ∀ (f : Module.Dual (ZMod 2) V), (∀ (g : Gen) (v : V), f ((Φ.op (q g)) v) = f v) → f = 0) : markedAug Φ q = ⊤

Marked fullness: if no nonzero functional is generator-invariant, the marked window is everything.