theorem Q2Presentation.Lifting.add_self_eq_zero_End {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (B : Module.End (ZMod 2) V) : B + B = 0

Doubles vanish in the endomorphism ring.

theorem Q2Presentation.Lifting.add_one_sq {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (B : Module.End (ZMod 2) V) : (B + 1) * (B + 1) = B * B + 1

Char-2 squares: (B + 1)² = B² + 1.

theorem Q2Presentation.Lifting.add_one_pow_two_pow {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (A : Module.End (ZMod 2) V) (k : ℕ) : (A + 1) ^ 2 ^ k = A ^ 2 ^ k + 1

Char-2 Frobenius for X + 1.

theorem Q2Presentation.Lifting.isNilpotent_add_one_of_two_pow {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (U : Module.End (ZMod 2) V) (k : ℕ) (hord : U ^ 2 ^ k = 1) : IsNilpotent (U + 1)

2-power-order endomorphisms have nilpotent U + 1.

theorem Q2Presentation.Lifting.isUnit_sq_add_add_one {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (U : Module.End (ZMod 2) V) (k : ℕ) (hord : U ^ 2 ^ k = 1) : IsUnit (U * U + U + 1)

U² + U + 1 is a unit at 2-power order.

theorem Q2Presentation.Lifting.isUnit_one_add_add_inv {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (U Uinv : Module.End (ZMod 2) V) (hUinv : U * Uinv = 1) (hUinvU : Uinv * U = 1) (k : ℕ) (hord : U ^ 2 ^ k = 1) : IsUnit (1 + U + Uinv)

The ramified pairing operator 1 + U + U⁻¹ is a unit at 2-power order, with the inverse supplied operationally.