theorem Q2Presentation.Lifting.op_cancel {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (x : V) (h : (Φ.op y) x = 0) : x = 0

Operator cancellation: values killed by an operator vanish.

theorem Q2Presentation.Lifting.tame_content_of_cycle {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (hcyc : foxShadowGen Φ.op q n Q2Word.tameRelator = 0) : (Φ.op (q Gen.sigma) * (1 + Φ.op (q Gen.tau))) ((Φ.op (q Gen.sigma)⁻¹) (n Gen.sigma)) + (Φ.op (q Gen.sigma) + 1 + Φ.op (q Gen.tau)) (n Gen.tau) = 0

Extract the factored tame content from a tame cycle.

theorem Q2Presentation.Lifting.add_shuffle_aba {W : Type} [AddCommGroup W] [Module (ZMod 2) W] (a b : W) : a + b + a = b

Char-2 triple shuffle.

theorem Q2Presentation.Lifting.dualPairingFaithful_structured {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] (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) (htame : Φ.op (Q2Word.tameRelator.eval q) = 1) (hwild : Φ.op (Q2Word.wildRelator.eval q) = 1) (hcase : (Φ.op (q Gen.tau) = 1 ∧ Φ.op (Q2Word.sigma2.eval q) = 1 ∧ ∀ (x : V), (Φ.op (q Gen.sigma)) x = x → x = 0) ∨ ∀ (x : V), (Φ.op (q Gen.tau)) x = x → x = 0) : dualPairingFaithful Φ q

Dual-pairing faithfulness at nontrivial simple tame frames.