def Q2Presentation.Lifting.pElem {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (lam : Module.Dual (ZMod 2) V) : Heis Φ

The dual translation element.

Equations

• Q2Presentation.Lifting.pElem Φ lam = { d := 0, e := lam, z := 0, y := 1 }

def Q2Presentation.Lifting.zElem {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (t : ZMod 2) : Heis Φ

The central element.

Equations

• Q2Presentation.Lifting.zElem Φ t = { d := 0, e := 0, z := t, y := 1 }

theorem Q2Presentation.Lifting.pElem_sq {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (lam : Module.Dual (ZMod 2) V) : pElem Φ lam * pElem Φ lam = 1

theorem Q2Presentation.Lifting.zElem_mul {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (t : ZMod 2) (h : Heis Φ) : zElem Φ t * h = { d := h.d, e := h.e, z := t + h.z, y := h.y }

theorem Q2Presentation.Lifting.mul_zElem {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (t : ZMod 2) (h : Heis Φ) : h * zElem Φ t = { d := h.d, e := h.e, z := t + h.z, y := h.y }

theorem Q2Presentation.Lifting.zElem_add {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (s t : ZMod 2) : zElem Φ s * zElem Φ t = zElem Φ (s + t)

theorem Q2Presentation.Lifting.zElem_zero {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) : zElem Φ 0 = 1

theorem Q2Presentation.Lifting.zElem_inv {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (t : ZMod 2) : (zElem Φ t)⁻¹ = zElem Φ t

theorem Q2Presentation.Lifting.zElem_mul_pow {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (t : ZMod 2) (h : Heis Φ) (k : ℕ) : (zElem Φ t * h) ^ k = zElem Φ (↑k * t) * h ^ k

Central shifts distribute over powers.

theorem Q2Presentation.Lifting.pElem_conj_gen {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (lam : Module.Dual (ZMod 2) V) (x : V) (c : Yt.Y) : pElem Φ lam * { d := x, e := 0, z := 0, y := c } * pElem Φ lam = zElem Φ (((dualOp Φ c) lam) x) * { d := x, e := (dualOp Φ c) lam + lam, z := 0, y := c }

The generator conjugation: dual coboundary entry plus central correction.

def Q2Presentation.Lifting.stokesCorrection {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (lam : Module.Dual (ZMod 2) V) (w : GExpr) : ZMod 2

The Stokes correction: exponent-sum weighted generator pairings.

Equations

• Q2Presentation.Lifting.stokesCorrection Φ q n lam w = ∑ g : Q2Presentation.Gen, Q2Presentation.Lifting.expSum g w * lam ((Φ.op (q g)⁻¹) (n g))

theorem Q2Presentation.Lifting.stokesCorrection_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (lam : Module.Dual (ZMod 2) V) : stokesCorrection Φ q n lam GExpr.one = 0

theorem Q2Presentation.Lifting.stokesCorrection_gen {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (lam : Module.Dual (ZMod 2) V) (a : Gen) : stokesCorrection Φ q n lam (GExpr.gen a) = lam ((Φ.op (q a)⁻¹) (n a))

theorem Q2Presentation.Lifting.stokesCorrection_mul {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (lam : Module.Dual (ZMod 2) V) (u v : GExpr) : stokesCorrection Φ q n lam (u.mul v) = stokesCorrection Φ q n lam u + stokesCorrection Φ q n lam v

theorem Q2Presentation.Lifting.stokesCorrection_inv {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (lam : Module.Dual (ZMod 2) V) (u : GExpr) : stokesCorrection Φ q n lam u.inv = stokesCorrection Φ q n lam u

theorem Q2Presentation.Lifting.stokesCorrection_powNat {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (lam : Module.Dual (ZMod 2) V) (u : GExpr) (k : ℕ) : stokesCorrection Φ q n lam (u.powNat k) = ↑k * stokesCorrection Φ q n lam u

theorem Q2Presentation.Lifting.stokesCorrection_powOmega2 {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (lam : Module.Dual (ZMod 2) V) (u : GExpr) : stokesCorrection Φ q n lam u.powOmega2 = stokesCorrection Φ q n lam u

theorem Q2Presentation.Lifting.stokes_conj {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (lam : Module.Dual (ZMod 2) V) (w : GExpr) : pElem Φ lam * heisEval Φ q n (fun (x : Gen) => 0) w * pElem Φ lam = zElem Φ (stokesCorrection Φ q n lam w) * heisEval Φ q n (fun (g : Gen) => (dualOp Φ (q g)) lam + lam) w

The conjugation telescope: the dual translation conjugates the zero-dual evaluation into the coboundary evaluation, up to the central Stokes correction.

theorem Q2Presentation.Lifting.heis_pow_ez {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (a : Heis Φ) (he : a.e = 0) (hz : a.z = 0) (k : ℕ) : (a ^ k).e = 0 ∧ (a ^ k).z = 0

Zero-dual power evaluations keep zero dual and central parts.

theorem Q2Presentation.Lifting.heisEval_ez_zero {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (w : GExpr) : (heisEval Φ q n (fun (x : Gen) => 0) w).e = 0 ∧ (heisEval Φ q n (fun (x : Gen) => 0) w).z = 0

The zero-dual evaluation has zero dual and central coordinates.

theorem Q2Presentation.Lifting.word_stokes {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (lam : Module.Dual (ZMod 2) V) (w : GExpr) : betaShadow Φ q n (fun (g : Gen) => (dualOp Φ (q g)) lam + lam) w = lam ((Φ.op (w.eval q)⁻¹) (foxShadowGen Φ.op q n w)) + stokesCorrection Φ q n lam w

The finite-word Stokes identity (eq:wordstokes2, right convention): the coboundary-dual cup value is the transported pairing with the shadow, corrected by the exponent sums.

theorem Q2Presentation.Lifting.traced_stokes {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (lam : Module.Dual (ZMod 2) V) : betaShadow Φ q n (fun (g : Gen) => (dualOp Φ (q g)) lam + lam) Q2Word.tameRelator + betaShadow Φ q n (fun (g : Gen) => (dualOp Φ (q g)) lam + lam) Q2Word.wildRelator = lam ((Φ.op (Q2Word.tameRelator.eval q)⁻¹) (foxShadowGen Φ.op q n Q2Word.tameRelator)) + lam ((Φ.op (Q2Word.wildRelator.eval q)⁻¹) (foxShadowGen Φ.op q n Q2Word.wildRelator))

The traced Stokes identity (prop:tracedstokes): at the relator pair the correction terms cancel.