theorem Q2Presentation.Lifting.foxShadow_tameRelator {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (n : Gen → NAdd E) : foxShadow E q n Q2Word.tameRelator = (conjEndN E (q Gen.tau ^ 2)⁻¹) ((conjEndN E (q Gen.sigma)) ((conjEndN E (q Gen.tau)) ((conjEndN E (q Gen.sigma)⁻¹) (n Gen.sigma)) + n Gen.tau) + n Gen.sigma) + (conjEndN E (q Gen.tau ^ 2)⁻¹) ((∑ i ∈ Finset.range 2, conjEndN E (q Gen.tau) ^ i) (n Gen.tau))

The tame shadow, unfolded (definitional recursion on the word).

theorem Q2Presentation.Lifting.foxShadow_tameRelator_factored {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (n : Gen → NAdd E) : foxShadow E q n Q2Word.tameRelator = (conjEndN E (q Gen.tau ^ 2)⁻¹) ((conjEndN E (q Gen.sigma) * (1 + conjEndN E (q Gen.tau))) ((conjEndN E (q Gen.sigma)⁻¹) (n Gen.sigma)) + (conjEndN E (q Gen.sigma) + 1 + conjEndN E (q Gen.tau)) (n Gen.tau))

Tame-row factorization: the tame shadow is the unit conjugate C_{(qτ²)⁻¹} of the word-complex tame row at Sinv := Cσ, T := Cτ, evaluated at the unit-changed variable C_{(qσ)⁻¹} nσ.

Arithmetic of the ω₂-residue and operator powers

theorem Q2Presentation.Lifting.omega2Mod_val_odd {m : ℕ} (hm : m ≠ 0) (h2 : 2 ∣ m) : Odd (omega2Mod m).val

The ω₂-residue is odd whenever the modulus is even.

theorem Q2Presentation.Lifting.conjEndN_pow {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (y : Yt.Y) (k : ℕ) : conjEndN E (y ^ k) = conjEndN E y ^ k

Conjugation operators of powers are powers of the operator.

theorem Q2Presentation.Lifting.sum_range_one_pow_of_odd {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] {R : ℕ} (hodd : Odd R) : ∑ i ∈ Finset.range R, 1 ^ i = 1

An odd sum of copies of 1 is 1 (char 2).

Coordinate decomposition and support vanishing

def Q2Presentation.Lifting.single {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (a : Gen) (x : NAdd E) : Gen → NAdd E

The tuple supported on one generator.

Equations

• Q2Presentation.Lifting.single E a x b = if b = a then x else 0

@[simp]

theorem Q2Presentation.Lifting.single_same {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (a : Gen) (x : NAdd E) : single E a x a = x

theorem Q2Presentation.Lifting.tuple_decomp {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (n : Gen → NAdd E) : n = single E Gen.sigma (n Gen.sigma) + single E Gen.tau (n Gen.tau) + single E Gen.x0 (n Gen.x0) + single E Gen.x1 (n Gen.x1)

theorem Q2Presentation.Lifting.foxShadow_decomp {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (n : Gen → NAdd E) (w : GExpr) : foxShadow E q n w = foxShadow E q (single E Gen.sigma (n Gen.sigma)) w + foxShadow E q (single E Gen.tau (n Gen.tau)) w + foxShadow E q (single E Gen.x0 (n Gen.x0)) w + foxShadow E q (single E Gen.x1 (n Gen.x1)) w

Shadows decompose over the four generator slots.

def Q2Presentation.Lifting.mentions : GExpr → Gen → Bool

Which generators a word mentions.

Equations

• Q2Presentation.Lifting.mentions Q2Presentation.GExpr.one x✝ = false
• Q2Presentation.Lifting.mentions (Q2Presentation.GExpr.gen b) x✝ = (b == x✝)
• Q2Presentation.Lifting.mentions (u.mul v) x✝ = (Q2Presentation.Lifting.mentions u x✝ || Q2Presentation.Lifting.mentions v x✝)
• Q2Presentation.Lifting.mentions u.inv x✝ = Q2Presentation.Lifting.mentions u x✝
• Q2Presentation.Lifting.mentions (u.powNat a) x✝ = Q2Presentation.Lifting.mentions u x✝
• Q2Presentation.Lifting.mentions u.powOmega2 x✝ = Q2Presentation.Lifting.mentions u x✝

theorem Q2Presentation.Lifting.foxShadow_single_of_not_mentions {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (a : Gen) (x : NAdd E) (w : GExpr) (hw : mentions w a = false) : foxShadow E q (single E a x) w = 0

Support vanishing: a word not mentioning a generator has zero shadow at tuples supported on that generator.

theorem Q2Presentation.Lifting.h0_not_mentions_x1 : mentions Q2Word.h0 Gen.x1 = false

h₀ does not mention x₁.

theorem Q2Presentation.Lifting.c0_not_mentions_x1 : mentions Q2Word.c0 Gen.x1 = false

c₀ does not mention x₁.

The wild relator's x₁-column

theorem Q2Presentation.Lifting.foxShadow_wild_x1_column {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (d : NAdd E) : foxShadow E q (single E Gen.x1 d) Q2Word.wildRelator = (conjEndN E (Q2Word.c0.eval q)) ((conjEndN E ((Q2Word.rconjExpr Q2Word.x1 Q2Word.sigma).eval q)) ((conjEndN E (Q2Word.u1.eval q)⁻¹) ((∑ i ∈ Finset.range (omega2Mod (Nat.card Yt.Y)).val, conjEndN E ((Q2Word.x1.mul Q2Word.tau).eval q) ^ i) ((conjEndN E (q Gen.tau)) d))) + (conjEndN E (q Gen.sigma)) d)

The x₁-column of the wild row: at tuples supported on x₁, the h₀- and c₀-shadows die (support), leaving the u₁⁻¹- and x₁^σ-factors.

Per-case surjectivity of the row map

theorem Q2Presentation.Lifting.conjEndN_isUnit {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (y : Yt.Y) : IsUnit (conjEndN E y)

Conjugation operators are units of the endomorphism ring.

theorem Q2Presentation.Lifting.conjEndN_inv_apply {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (y : Yt.Y) (x : NAdd E) : (conjEndN E y⁻¹) ((conjEndN E y) x) = x

Pointwise inverse law: C_{y⁻¹} (C_y x) = x.

theorem Q2Presentation.Lifting.conjEndN_apply_inv {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (y : Yt.Y) (x : NAdd E) : (conjEndN E y) ((conjEndN E y⁻¹) x) = x

Pointwise inverse law, other order.

theorem Q2Presentation.Lifting.tame_not_mentions_x1 : mentions Q2Word.tameRelator Gen.x1 = false

The tame relator does not mention x₁.

theorem Q2Presentation.Lifting.single_zero {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (a : Gen) : single E a 0 = 0

Zero-supported tuples are the zero tuple.

theorem Q2Presentation.Lifting.rconj_op_collapse {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (hx1 : conjEndN E (q Gen.x1) = 1) : conjEndN E ((Q2Word.rconjExpr Q2Word.x1 Q2Word.sigma).eval q) = 1

Under trivial x₁-action, the x₁^σ-coefficient collapses.

theorem Q2Presentation.Lifting.u1_op_collapse {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (hx1 : conjEndN E (q Gen.x1) = 1) (hT : conjEndN E (q Gen.tau) = 1) : conjEndN E (Q2Word.u1.eval q)⁻¹ = 1

Under trivial x₁- and τ-action, the u₁-eval acts trivially.

theorem Q2Presentation.Lifting.pop_collapse {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (hx1 : conjEndN E (q Gen.x1) = 1) (hT : conjEndN E (q Gen.tau) = 1) (htwo : 2 ∣ Nat.card Yt.Y) : ∑ i ∈ Finset.range (omega2Mod (Nat.card Yt.Y)).val, conjEndN E ((Q2Word.x1.mul Q2Word.tau).eval q) ^ i = 1

Under trivial x₁- and τ-action with even |Y|, the norm projector collapses to 1.

theorem Q2Presentation.Lifting.wild_x1_column_case_i {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (hx1 : conjEndN E (q Gen.x1) = 1) (hT : conjEndN E (q Gen.tau) = 1) (htwo : 2 ∣ Nat.card Yt.Y) (d : NAdd E) : foxShadow E q (single E Gen.x1 d) Q2Word.wildRelator = (conjEndN E (Q2Word.c0.eval q)) ((1 + conjEndN E (q Gen.sigma)) d)

Case (i) collapse of the wild x₁-column: C_{c0v}((1 + Cσ) d).

theorem Q2Presentation.Lifting.rowMap_surjective_case_i {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (htwo : 2 ∣ Nat.card Yt.Y) (hx1 : conjEndN E (q Gen.x1) = 1) (hT : conjEndN E (q Gen.tau) = 1) (hSone : IsUnit (1 + conjEndN E (q Gen.sigma))) : Function.Surjective ⇑(rowMap E q)

Row-map surjectivity, case (i) (T = 1, trivial wild action, 1 + Cσ invertible).

theorem Q2Presentation.Lifting.rowMap_surjective_case_ii {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] (q : Marking Yt.Y) (hPop : ∑ i ∈ Finset.range (omega2Mod (Nat.card Yt.Y)).val, conjEndN E ((Q2Word.x1.mul Q2Word.tau).eval q) ^ i = 0) (hTone : IsUnit (1 + conjEndN E (q Gen.tau))) : Function.Surjective ⇑(rowMap E q)

Row-map surjectivity, case (ii) (vanishing norm projector, 1 + Cτ invertible).