def Q2Presentation.Lifting.expSum (g : Gen) : GExpr → ZMod 2

Mod-2 exponent sum of a generator in a word, with ω₂-powers counted once (the residue length is odd).

Equations

• Q2Presentation.Lifting.expSum g Q2Presentation.GExpr.one = 0
• Q2Presentation.Lifting.expSum g (Q2Presentation.GExpr.gen a) = if a = g then 1 else 0
• Q2Presentation.Lifting.expSum g (u.mul v) = Q2Presentation.Lifting.expSum g u + Q2Presentation.Lifting.expSum g v
• Q2Presentation.Lifting.expSum g u.inv = Q2Presentation.Lifting.expSum g u
• Q2Presentation.Lifting.expSum g (u.powNat k) = ↑k * Q2Presentation.Lifting.expSum g u
• Q2Presentation.Lifting.expSum g u.powOmega2 = Q2Presentation.Lifting.expSum g u

theorem Q2Presentation.Lifting.nsmul_eq_parity_smul {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (k : ℕ) (x : V) : k • x = ↑k • x

Nat-smul by parity in a ZMod 2-module.

theorem Q2Presentation.Lifting.foxShadowGen_of_ops_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (hone : ∀ (y : Yt.Y), Φ.op y = 1) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (q : Marking Yt.Y) (n : Gen → V) (w : GExpr) : foxShadowGen Φ.op q n w = ∑ g : Gen, expSum g w • n g

The trivial-section Jacobian: with all operators trivial, shadows are exponent-sum combinations.

theorem Q2Presentation.Lifting.expSum_tameRelator_tau : expSum Gen.tau Q2Word.tameRelator = 1

Exponent sums of the tame relator.

theorem Q2Presentation.Lifting.expSum_tameRelator_sigma : expSum Gen.sigma Q2Word.tameRelator = 0

theorem Q2Presentation.Lifting.expSum_tameRelator_x0 : expSum Gen.x0 Q2Word.tameRelator = 0

theorem Q2Presentation.Lifting.expSum_tameRelator_x1 : expSum Gen.x1 Q2Word.tameRelator = 0

theorem Q2Presentation.Lifting.expSum_wildRelator_tau : expSum Gen.tau Q2Word.wildRelator = 1

Exponent sums of the wild relator.

theorem Q2Presentation.Lifting.expSum_wildRelator_sigma : expSum Gen.sigma Q2Word.wildRelator = 0

theorem Q2Presentation.Lifting.expSum_wildRelator_x0 : expSum Gen.x0 Q2Word.wildRelator = 0

theorem Q2Presentation.Lifting.expSum_wildRelator_x1 : expSum Gen.x1 Q2Word.wildRelator = 0

theorem Q2Presentation.Lifting.trivial_section_rows {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (hone : ∀ (y : Yt.Y), Φ.op y = 1) (hodd : Odd (omega2Mod (Nat.card Yt.Y)).val) (q : Marking Yt.Y) (n : Gen → V) : (foxShadowGen Φ.op q n Q2Word.tameRelator, foxShadowGen Φ.op q n Q2Word.wildRelator) = (n Gen.tau, n Gen.tau)

The trivial-section row map is the τ-diagonal.