theorem Q2Presentation.Lifting.heisEval_h0_triple {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) (c : V) (lam : Module.Dual (ZMod 2) V) : (heisEval Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) Q2Word.h0).d = (Φ.op (Q2Word.g0.eval q)) c + c + (Φ.op (Q2Word.g0.eval q)) (foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0) + foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0 ∧ (heisEval Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) Q2Word.h0).e = (dualOp Φ (Q2Word.g0.eval q)) lam + lam + (dualOp Φ (Q2Word.g0.eval q)) (foxShadowGen (dualFamily Φ).op q (famSingle Gen.x0 lam) Q2Word.d0) + foxShadowGen (dualFamily Φ).op q (famSingle Gen.x0 lam) Q2Word.d0 ∧ (heisEval Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) Q2Word.h0).z = (foxShadowGen (dualFamily Φ).op q (famSingle Gen.x0 lam) Q2Word.d0) (foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0) + (foxShadowGen (dualFamily Φ).op q (famSingle Gen.x0 lam) Q2Word.d0) ((Φ.op (Q2Word.g0.eval q)) (foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0)) + ((dualOp Φ (Q2Word.g0.eval q)) lam) c + ((dualOp Φ (Q2Word.g0.eval q)) lam) ((Φ.op (Q2Word.g0.eval q)) (foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0)) + ((dualOp Φ (Q2Word.g0.eval q)) lam) (foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0) + lam ((Φ.op (Q2Word.g0.eval q)) (foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0)) + lam (foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0)

The h₀-telescope.