theorem Q2Presentation.Lifting.fox_rconj_of_op_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (w g : GExpr) (n : Gen → V) (hw : Φ.op (w.eval q) = 1) : foxShadowGen Φ.op q n (Q2Word.rconjExpr w g) = (Φ.op (g.eval q)) (foxShadowGen Φ.op q n w)

The conjugation row formula: at trivially-evaluating w the g-terms cancel.

theorem Q2Presentation.Lifting.op_eval_x1tau {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx1 : Φ.op (q Gen.x1) = 1) : Φ.op ((Q2Word.x1.mul Q2Word.tau).eval q) = Φ.op (q Gen.tau)

theorem Q2Presentation.Lifting.op_eval_u1_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx1 : Φ.op (q Gen.x1) = 1) (e : ℕ) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) : Φ.op (Q2Word.u1.eval q) = 1

The u₁-evaluation acts trivially.

theorem Q2Presentation.Lifting.fox_d0_general {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx0 : Φ.op (q Gen.x0) = 1) (e : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → V) : foxShadowGen Φ.op q n Q2Word.d0 = (∑ i ∈ Finset.range e, Φ.op (q Gen.tau) ^ i) (n Gen.x0) + (∑ i ∈ Finset.range e, Φ.op (q Gen.tau) ^ i) (n Gen.tau) + n Gen.x0

The general d₀-row.

theorem Q2Presentation.Lifting.fox_u1inv_general {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx1 : Φ.op (q Gen.x1) = 1) (e : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → V) : foxShadowGen Φ.op q n Q2Word.u1.inv = (∑ i ∈ Finset.range e, Φ.op (q Gen.tau) ^ i) (n Gen.x1) + (∑ i ∈ Finset.range e, Φ.op (q Gen.tau) ^ i) (n Gen.tau)

The general u₁⁻¹-row.

theorem Q2Presentation.Lifting.fox_c0_general {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx0 : Φ.op (q Gen.x0) = 1) (e : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → V) : foxShadowGen Φ.op q n Q2Word.c0 = 0

The general c₀-row vanishes.

theorem Q2Presentation.Lifting.fox_h0_general {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx0 : Φ.op (q Gen.x0) = 1) (e : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → V) : foxShadowGen Φ.op q n Q2Word.h0 = (Φ.op (Q2Word.g0.eval q)) (n Gen.x0) + n Gen.x0 + (Φ.op (Q2Word.g0.eval q)) (foxShadowGen Φ.op q n Q2Word.d0) + foxShadowGen Φ.op q n Q2Word.d0

The general h₀-row: the flat four-term sum.

theorem Q2Presentation.Lifting.fox_wild_general {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx0 : Φ.op (q Gen.x0) = 1) (hx1 : Φ.op (q Gen.x1) = 1) (e : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (n : Gen → V) : foxShadowGen Φ.op q n Q2Word.wildRelator = foxShadowGen Φ.op q n Q2Word.h0 + foxShadowGen Φ.op q n Q2Word.u1.inv + (Φ.op (q Gen.sigma)) (n Gen.x1)

The general wild row: the flat sum of the factor rows.