theorem Q2Presentation.Lifting.heisEval_rconj_triple {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (a : Gen) (x : V) (lam : Module.Dual (ZMod 2) V) (w g : GExpr) (hg : mentions g a = false) : (heisEval Φ q (famSingle a x) (famSingle a lam) (Q2Word.rconjExpr w g)).d = (Φ.op (g.eval q)) (heisEval Φ q (famSingle a x) (famSingle a lam) w).d ∧ (heisEval Φ q (famSingle a x) (famSingle a lam) (Q2Word.rconjExpr w g)).e = (dualOp Φ (g.eval q)) (heisEval Φ q (famSingle a x) (famSingle a lam) w).e ∧ (heisEval Φ q (famSingle a x) (famSingle a lam) (Q2Word.rconjExpr w g)).z = (heisEval Φ q (famSingle a x) (famSingle a lam) w).z

The conjugation triple: rconj by a non-mentioning word transports d and e by the evaluation and preserves z.

theorem Q2Presentation.Lifting.heis_sq_triple {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (A : Heis Φ) (hA : Φ.op A.y = 1) : (A * A).d = 0 ∧ (A * A).e = 0 ∧ (A * A).z = A.e A.d

The square triple at trivially-acting parts: vanishing first-order coordinates, pairing diagonal centrally.

theorem Q2Presentation.Lifting.heis_mul_z_of_op_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (A B : Heis Φ) (hB : Φ.op B.y = 1) : (A * B).z = A.z + B.z + A.e B.d

The product central rule at trivially-acting parts.

theorem Q2Presentation.Lifting.heis_mul_de_of_op_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (A B : Heis Φ) (hB : Φ.op B.y = 1) : (A * B).d = A.d + B.d ∧ (A * B).e = A.e + B.e

First-order coordinates of products at trivially-acting parts.