Norm case values

theorem Q2Presentation.Lifting.norm_of_T_one {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (e : ℕ) (heodd : Odd e) (T : Module.End (ZMod 2) V) (hT : T = 1) : ∑ i ∈ Finset.range e, T ^ i = 1

The odd norm of the identity is the identity.

theorem Q2Presentation.Lifting.self_mul_norm {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (T : Module.End (ZMod 2) V) (e : ℕ) (he : T ^ e = 1) : T * ∑ i ∈ Finset.range e, T ^ i = ∑ i ∈ Finset.range e, T ^ i

The left absorption of the odd norm.

theorem Q2Presentation.Lifting.norm_of_fixed_bot {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (e : ℕ) (T : Module.End (ZMod 2) V) (he : T ^ e = 1) (hfix : ∀ (x : V), T x = x → x = 0) : ∑ i ∈ Finset.range e, T ^ i = 0

The odd norm vanishes when the τ-fixed space is trivial.

Dual frame transport

theorem Q2Presentation.Lifting.dual_hTe {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (e : ℕ) (hTe : Φ.op (q Gen.tau) ^ e = 1) : (dualFamily Φ).op (q Gen.tau) ^ e = 1

The dual family inherits the τ-power relation.

theorem Q2Presentation.Lifting.dual_hx0 {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) : (dualFamily Φ).op (q Gen.x0) = 1

The dual family inherits the trivial wild operator.

The c₀-triple

theorem Q2Presentation.Lifting.heisEval_c0_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.c0).d = 0 ∧ (heisEval Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) Q2Word.c0).e = 0 ∧ (heisEval Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) Q2Word.c0).z = (foxShadowGen (dualFamily Φ).op q (famSingle Gen.x0 lam) Q2Word.d0) (foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.z0) + (foxShadowGen (dualFamily Φ).op q (famSingle Gen.x0 lam) Q2Word.z0) (foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0)

The c₀-commutator triple at x₀-singles: vanishing first-order coordinates, bilinear central value in the subword ledger entries.