structure Q2Presentation.Lifting.TrivHeis : Type

Coefficient mirror of the Heisenberg evaluation over a trivial family.

• dC : Gen → ZMod 2
• eC : Gen → ZMod 2
• zC : Gen → Gen → ZMod 2

theorem Q2Presentation.Lifting.TrivHeis.ext' {a b : TrivHeis} (hd : a.dC = b.dC) (he : a.eC = b.eC) (hz : a.zC = b.zC) : a = b

def Q2Presentation.Lifting.TrivHeis.one' : TrivHeis

Equations

• Q2Presentation.Lifting.TrivHeis.one' = { dC := fun (x : Q2Presentation.Gen) => 0, eC := fun (x : Q2Presentation.Gen) => 0, zC := fun (x x_1 : Q2Presentation.Gen) => 0 }

def Q2Presentation.Lifting.TrivHeis.mul' (a b : TrivHeis) : TrivHeis

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Lifting.TrivHeis.inv' (a : TrivHeis) : TrivHeis

Equations

• a.inv' = { dC := a.dC, eC := a.eC, zC := fun (g h : Q2Presentation.Gen) => a.zC g h + a.eC g * a.dC h }

def Q2Presentation.Lifting.TrivHeis.pow' (a : TrivHeis) : ℕ → TrivHeis

Equations

• a.pow' 0 = Q2Presentation.Lifting.TrivHeis.one'
• a.pow' k.succ = (a.pow' k).mul' a

def Q2Presentation.Lifting.TrivHeis.genE (x : Gen) : TrivHeis

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Lifting.TrivHeis.pow'_dC (a : TrivHeis) (k : ℕ) (g : Gen) : (a.pow' k).dC g = ↑k * a.dC g

Closed form of the mirror powers: value coefficients.

theorem Q2Presentation.Lifting.TrivHeis.pow'_eC (a : TrivHeis) (k : ℕ) (g : Gen) : (a.pow' k).eC g = ↑k * a.eC g

Closed form of the mirror powers: dual coefficients.

theorem Q2Presentation.Lifting.TrivHeis.pow'_zC (a : TrivHeis) (k : ℕ) (g h : Gen) : (a.pow' k).zC g h = ↑k * a.zC g h + (∑ i ∈ Finset.range k, ↑i) * (a.eC g * a.dC h)

Closed form of the mirror powers: central coefficients (triangle coefficient as a range sum).

theorem Q2Presentation.Lifting.TrivHeis.sum_range_cast_4m1 (m : ℕ) : ∑ i ∈ Finset.range (4 * m + 1), ↑i = 0

The triangle sum vanishes at exponents ≡ 1 mod 4.

theorem Q2Presentation.Lifting.TrivHeis.pow'_of_4m1 (a : TrivHeis) (Ω : ℕ) (hΩ : Ω % 4 = 1) : a.pow' Ω = a.pow' 1

Mirror ω₂-collapse: at exponents ≡ 1 mod 4 the mirror power is the first power.

def Q2Presentation.Lifting.trivEval (Ω : ℕ) : GExpr → TrivHeis

The mirror evaluation, ω₂-exponent as a parameter.

Equations

• Q2Presentation.Lifting.trivEval Ω Q2Presentation.GExpr.one = Q2Presentation.Lifting.TrivHeis.one'
• Q2Presentation.Lifting.trivEval Ω (Q2Presentation.GExpr.gen a) = Q2Presentation.Lifting.TrivHeis.genE a
• Q2Presentation.Lifting.trivEval Ω (u.mul v) = (Q2Presentation.Lifting.trivEval Ω u).mul' (Q2Presentation.Lifting.trivEval Ω v)
• Q2Presentation.Lifting.trivEval Ω u.inv = (Q2Presentation.Lifting.trivEval Ω u).inv'
• Q2Presentation.Lifting.trivEval Ω (u.powNat k) = (Q2Presentation.Lifting.trivEval Ω u).pow' k
• Q2Presentation.Lifting.trivEval Ω u.powOmega2 = (Q2Presentation.Lifting.trivEval Ω u).pow' Ω

theorem Q2Presentation.Lifting.trivEval_collapse (Ω : ℕ) (hΩ : Ω % 4 = 1) (w : GExpr) : trivEval Ω w = trivEval 1 w

Mirror evaluations collapse to exponent 1 at ω₂ ≡ 1 mod 4.

def Q2Presentation.Lifting.TrivRel {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (a : Heis Φ) (A : TrivHeis) : Prop

The bridge relation: the evaluation's coordinates are the mirror's coefficient contractions.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Lifting.pair_expand {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (E D : Gen → ZMod 2) : (∑ g : Gen, E g • φ g) (∑ h : Gen, D h • n h) = ∑ g : Gen, ∑ h : Gen, E g * D h * (φ g) (n h)

Pairing expansion of contracted sums.

theorem Q2Presentation.Lifting.trivRel_dualOp {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) (lam : Module.Dual (ZMod 2) V) : (dualOp Φ y) lam = lam

theorem Q2Presentation.Lifting.trivRel_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (hone : ∀ (y : Yt.Y), Φ.op y = 1) : TrivRel Φ n φ 1 TrivHeis.one'

theorem Q2Presentation.Lifting.trivRel_mul {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (hone : ∀ (y : Yt.Y), Φ.op y = 1) {a b : Heis Φ} {A B : TrivHeis} (ha : TrivRel Φ n φ a A) (hb : TrivRel Φ n φ b B) : TrivRel Φ n φ (a * b) (A.mul' B)

theorem Q2Presentation.Lifting.trivRel_inv {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (hone : ∀ (y : Yt.Y), Φ.op y = 1) {a : Heis Φ} {A : TrivHeis} (ha : TrivRel Φ n φ a A) : TrivRel Φ n φ a⁻¹ A.inv'

theorem Q2Presentation.Lifting.trivRel_pow {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] {Φ : OperatorFamily Yt V} (n : Gen → V) (φ : Gen → Module.Dual (ZMod 2) V) (hone : ∀ (y : Yt.Y), Φ.op y = 1) {a : Heis Φ} {A : TrivHeis} (ha : TrivRel Φ n φ a A) (k : ℕ) : TrivRel Φ n φ (a ^ k) (A.pow' k)

theorem Q2Presentation.Lifting.trivRel_gen {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) (x : Gen) : TrivRel Φ n φ { d := n x, e := φ x, z := 0, y := q x } (TrivHeis.genE x)

theorem Q2Presentation.Lifting.heisEval_trivRel {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) (w : GExpr) : TrivRel Φ n φ (heisEval Φ q n φ w) (trivEval (omega2Mod (Nat.card Yt.Y)).val w)

The bridge: the evaluation over a trivial family realizes the mirror coefficients.

theorem Q2Presentation.Lifting.betaShadow_trivial {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) (h4 : (omega2Mod (Nat.card Yt.Y)).val % 4 = 1) (w : GExpr) : betaShadow Φ q n φ w = ∑ g : Gen, ∑ h : Gen, (trivEval 1 w).zC g h * (φ g) (n h)

The trivial β-table: the cup coordinate over a trivial family is the mirror matrix contraction, at the collapsed exponent when ω₂ ≡ 1 mod 4.