theorem Q2Presentation.Lifting.rows_lift_mem_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) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (n : Gen → V) (hker : foxShadowGen (Φ.descend W hW).op q (fun (g : Gen) => W.mkQ (n g)) Q2Word.tameRelator = 0 ∧ foxShadowGen (Φ.descend W hW).op q (fun (g : Gen) => W.mkQ (n g)) Q2Word.wildRelator = 0) : foxShadowGen Φ.op q n Q2Word.tameRelator ∈ W ∧ foxShadowGen Φ.op q n Q2Word.wildRelator ∈ W

Row values of quotient-cocycle lifts land in the floor.

theorem Q2Presentation.Lifting.extending_invariant_kills_rows_sum {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) (lam : Module.Dual (ZMod 2) V) (hlam : ∀ (g : Gen) (x : V), lam ((Φ.op (q g)) x) = lam x) (n : Gen → V) : lam (foxShadowGen Φ.op q n Q2Word.tameRelator + foxShadowGen Φ.op q n Q2Word.wildRelator) = 0

(F3) Generator-invariant duals kill the ∂-value sums (via the marked traced Stokes constraint).

theorem Q2Presentation.Lifting.lift_correction {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) (n t : Gen → V) (ht : ∀ (g : Gen), t g ∈ W) (hcorr : foxShadowGen Φ.op q t Q2Word.tameRelator = foxShadowGen Φ.op q n Q2Word.tameRelator ∧ foxShadowGen Φ.op q t Q2Word.wildRelator = foxShadowGen Φ.op q n Q2Word.wildRelator) : foxShadowGen Φ.op q (n + t) Q2Word.tameRelator = 0 ∧ foxShadowGen Φ.op q (n + t) Q2Word.wildRelator = 0 ∧ ∀ (g : Gen), W.mkQ ((n + t) g) = W.mkQ (n g)

(F1) Floor correction of lifts: if a lift's row defect is a restricted row value, the lift can be corrected into the full kernel.

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

The gap window: floor pairs whose sum lies in the ambient marked augmentation.

Equations

• Q2Presentation.Lifting.gapWindow Φ q W = { carrier := {p : V × V | p.1 ∈ W ∧ p.2 ∈ W ∧ p.1 + p.2 ∈ Q2Presentation.Lifting.markedAug Φ q}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem Q2Presentation.Lifting.mem_gapWindow {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) (p : V × V) : p ∈ gapWindow Φ q W ↔ p.1 ∈ W ∧ p.2 ∈ W ∧ p.1 + p.2 ∈ markedAug Φ q

theorem Q2Presentation.Lifting.diamond_step {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) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (hstep : ∀ p ∈ gapWindow Φ q W, ∃ (n : Gen → V), (famRowsMap Φ q) n = p) (hquot : ∀ (ub vb : V ⧸ W), ub + vb ∈ markedAug (Φ.descend W hW) q → ∃ (nb : Gen → V ⧸ W), (famRowsMap (Φ.descend W hW) q) nb = (ub, vb)) (u v : V) (huv : u + v ∈ markedAug Φ q) : ∃ (n : Gen → V), (famRowsMap Φ q) n = (u, v)

The dévissage step, modulo the extension input (F4): with the quotient solved, the floor solved for its own augmentation window, and every gap pair reachable, the ambient window is solved.