theorem Q2Presentation.Lifting.sectionFamily_op_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') (y : Yt.Y) (h : Φ.op y = 1) : (sectionFamily Φ W' W hW hW').op y = 1

Section operators of trivially-acting elements are trivial.

theorem Q2Presentation.Lifting.fixed_ne_bot_of_two_pow {V : Type} [AddCommGroup V] [Module (ZMod 2) V] [Nontrivial V] (A : Module.End (ZMod 2) V) (k : ℕ) (hord : A ^ 2 ^ k = 1) : ∃ (x : V), x ≠ 0 ∧ A x = x

Nilpotent operators on nontrivial simple-lattice modules have nonzero kernels of their unit translates.

theorem Q2Presentation.Lifting.hfaithNT_of_frame {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] (htwo : 2 ∣ Nat.card Yt.Y) (hx0LY : q Gen.x0 ∈ Yt.LY) (hx1LY : q Gen.x1 ∈ Yt.LY) (hdecomp : ∀ (y : Yt.Y), ∃ w ∈ Subgroup.closure {q Gen.sigma, q Gen.tau}, y * w⁻¹ ∈ Yt.LY) (hrel : rconj (Yt.piY (q Gen.tau)) (Yt.piY (q Gen.sigma)) = Yt.piY (q Gen.tau) ^ 2) (htame : Φ.op (Q2Word.tameRelator.eval q) = 1) (hwild : Φ.op (Q2Word.wildRelator.eval q) = 1) (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') : W' < W → (∀ U < W, W' ≤ U → (∀ (y : Yt.Y), ∀ m ∈ U, (Φ.op y) m ∈ U) → U = W') → (¬∀ (y : Yt.Y), (sectionFamily Φ W' W hW hW').op y = 1) → dualPairingFaithful (sectionFamily Φ W' W hW hW') q

The section faithfulness discharge: every nontrivial maximal stable section has faithful dual pairing.