theorem Q2Presentation.Lifting.g0_not_mentions_x0 : mentions Q2Word.g0 Gen.x0 = false

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

Conjugates of trivially-acting words act trivially.

theorem Q2Presentation.Lifting.op_eval_mul_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (u v : GExpr) (hu : Φ.op (u.eval q) = 1) (hv : Φ.op (v.eval q) = 1) : Φ.op ((u.mul v).eval q) = 1

Products of trivially-acting words act trivially.

theorem Q2Presentation.Lifting.op_eval_inv_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (u : GExpr) (hu : Φ.op (u.eval q) = 1) : Φ.op (u.inv.eval q) = 1

Inverses of trivially-acting words act trivially.

theorem Q2Presentation.Lifting.op_eval_comm_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (u v : GExpr) (hu : Φ.op (u.eval q) = 1) (hv : Φ.op (v.eval q) = 1) : Φ.op ((Q2Word.commExpr u v).eval q) = 1

Commutators of trivially-acting words act trivially.

theorem Q2Presentation.Lifting.op_eval_x0_eq_one {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) : Φ.op (Q2Word.x0.eval q) = 1

The x₀-word acts trivially.

theorem Q2Presentation.Lifting.op_eval_x0g0_eq_one {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) : Φ.op ((Q2Word.rconjExpr Q2Word.x0 Q2Word.g0).eval q) = 1

The conjugated x₀-factor acts trivially.

theorem Q2Presentation.Lifting.op_eval_dg_eq_one {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 : ℕ) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) : Φ.op (Q2Word.dg.eval q) = 1

The d_g-factor acts trivially.

theorem Q2Presentation.Lifting.op_eval_d0sq_eq_one {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 : ℕ) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) : Φ.op ((Q2Word.d0.powNat 2).eval q) = 1

The d₀²-factor acts trivially.

theorem Q2Presentation.Lifting.op_eval_hc_eq_one {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 : ℕ) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) : Φ.op (Q2Word.hc.eval q) = 1

The h_c-factor acts trivially.