theorem Q2Presentation.Lifting.betaShadow_tame_x0 {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (c : V) (lam : Module.Dual (ZMod 2) V) : betaShadow Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) Q2Word.tameRelator = 0

The tame cup coordinate vanishes at x₀-singles.

theorem Q2Presentation.Lifting.betaShadow_wild_x0 {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) : betaShadow Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) Q2Word.wildRelator = (heisEval Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) Q2Word.h0).z + (heisEval Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) Q2Word.c0).z

The wild-relator cup coordinate splits: h₀- plus c₀-central values.

theorem Q2Presentation.Lifting.fox_wild_x0 {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) : foxShadowGen Φ.op q (famSingle Gen.x0 c) Q2Word.wildRelator = (Φ.op (Q2Word.c0.eval q)) ((Φ.op ((Q2Word.rconjExpr Q2Word.x1 Q2Word.sigma).eval q)) ((Φ.op (Q2Word.u1.inv.eval q)) (heisEval Φ q (famSingle Gen.x0 c) (famSingle Gen.x0 lam) Q2Word.h0).d))

The wild-relator value coordinate at x₀-singles is the transported h₀-value.