theorem Q2Presentation.Lifting.dualOp_of_ops_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (hone : ∀ (y : Yt.Y), Φ.op y = 1) (y : Yt.Y) : dualOp Φ y = LinearMap.id

Trivial operators have identity duals.

theorem Q2Presentation.Lifting.id_pow_sum {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (k : ℕ) : ∑ i ∈ Finset.range k, LinearMap.id ^ i = k • 1

Identity-power sums collapse to the counting multiple.

theorem Q2Presentation.Lifting.heisEval_e_of_ops_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (hone : ∀ (y : Yt.Y), Φ.op y = 1) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (w : GExpr) : (heisEval Φ q n φ w).e = ∑ g : Gen, expSum g w • φ g

The dual coordinate collapses to exponent sums at trivial operators.

theorem Q2Presentation.Lifting.heis_pow_z_of_ops_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (hone : ∀ (y : Yt.Y), Φ.op y = 1) (a : Heis Φ) (k : ℕ) : (a ^ k).z = k • a.z + ↑(k.choose 2) • a.e a.d

The quadratic collapse: at trivial operators the power's central coordinate is the binomial parity times the self-pairing.