Case i: trivial τ-action

theorem Q2Presentation.Lifting.fox_d0_case_i {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 : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (hT1 : Φ.op (q Gen.tau) = 1) (c : V) : foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0 = 0

theorem Q2Presentation.Lifting.fox_dual_d0_case_i {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 : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (hT1 : Φ.op (q Gen.tau) = 1) (lam : Module.Dual (ZMod 2) V) : foxShadowGen (dualFamily Φ).op q (famSingle Gen.x0 lam) Q2Word.d0 = 0

theorem Q2Presentation.Lifting.cupForm_x0_case_i {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 : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (hT1 : Φ.op (q Gen.tau) = 1) (hU1 : Φ.op (Q2Word.sigma2.eval q) = 1) (c : V) (lam : Module.Dual (ZMod 2) V) : cupForm Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) = lam c

The unramified mixed Hessian: λ(c).

theorem Q2Presentation.Lifting.fox_wild_x0_case_i {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 : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (hT1 : Φ.op (q Gen.tau) = 1) (hU1 : Φ.op (Q2Word.sigma2.eval q) = 1) (c : V) : foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.wildRelator = 0

The x₀-singles are wild-row cycles in the unramified case.

Case ii: trivial τ-fixed space

theorem Q2Presentation.Lifting.dual_fixed_bot {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] (hfix : ∀ (x : V), (Φ.op (q Gen.tau)) x = x → x = 0) (lam : Module.Dual (ZMod 2) V) : ((dualFamily Φ).op (q Gen.tau)) lam = lam → lam = 0

Dual-fixed triviality from fixed triviality on finite modules.

theorem Q2Presentation.Lifting.fox_d0_case_ii {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 : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) [Finite V] (hfix : ∀ (x : V), (Φ.op (q Gen.tau)) x = x → x = 0) (c : V) : foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.d0 = c

theorem Q2Presentation.Lifting.fox_dual_d0_case_ii {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 : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) [Finite V] (hfix : ∀ (x : V), (Φ.op (q Gen.tau)) x = x → x = 0) (lam : Module.Dual (ZMod 2) V) : foxShadowGen (dualFamily Φ).op q (famSingle Gen.x0 lam) Q2Word.d0 = lam

theorem Q2Presentation.Lifting.cupForm_x0_case_ii {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 : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) [Finite V] (hfix : ∀ (x : V), (Φ.op (q Gen.tau)) x = x → x = 0) (c : V) (lam : Module.Dual (ZMod 2) V) : cupForm Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) = lam c + lam ((Φ.op (Q2Word.sigma2.eval q)) c) + lam ((Φ.op (Q2Word.sigma2.eval q)⁻¹) c)

The ramified mixed Hessian: the three-term value.

theorem Q2Presentation.Lifting.fox_wild_x0_case_ii {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 : ℕ) (hepos : 0 < e) (heodd : Odd e) (hTe : Φ.op (q Gen.tau) ^ e = 1) (heY : e ∣ Nat.card Yt.Y) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) [Finite V] (hfix : ∀ (x : V), (Φ.op (q Gen.tau)) x = x → x = 0) (c : V) : foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.wildRelator = 0

The x₀-singles are wild-row cycles in the ramified case.