theorem Q2Presentation.Lifting.heis_pow_e {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (a : Heis Φ) (k : ℕ) : (a ^ k).e = (∑ i ∈ Finset.range k, dualOp Φ a.y ^ i) a.e

Powers project on the dual coordinate as dual operator norms.

theorem Q2Presentation.Lifting.heis_pow_z {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (a : Heis Φ) (k : ℕ) : (a ^ k).z = k • a.z + ∑ j ∈ Finset.range k, ((dualOp Φ a.y) ((∑ l ∈ Finset.range j, dualOp Φ a.y ^ l) a.e)) a.d

The Heisenberg quadratic telescope: the central coordinate of a power.