The χ-twisted crossed derivations, d̄-additivity, and tail separation

Piece 4/6 of GQ2.Roe.Labute.StageLemma (see that module for the mathematical overview and the statement freeze). SL1's separating functionals: the finite lift group WL N = ℤ/2^N ⋊ (ℤ/2^N)ˣ, the two coordinate derivations out of the towers, the d̄-image subgroup structure, and the endgame showing the derivations separate the two tails.

The χ-twisted crossed derivations (SL1's separating functionals)

SL1 needs functionals on Zₖ that kill Im d̄ and the defect but pair non-degenerately with the two tails. The numerics report (docs/orchestration/sl1-numerics.md §6) identifies them as digit-(k−1) shadows of θ-crossed derivations; the repo already carries the exact (un-truncated) version of that calculus — Labute's descent condition IsLabuteOrientationDatum (GQ2/Roe/CrossedDerivation.lean), which says that for the canonical orientation χ every crossed derivation D(gh) = Dg + χ(g)·Dh kills the presenting relator. So the functionals descend to the towers on the nose, with no relation module theory: a derivation is just the .u-component of a hom into A ⋊ ℤ₂ˣ.

Since ℤ₂ ⋊ ℤ₂ˣ is not known here to be pro-2 (the universal properties drLiftHom / d0LiftHom demand that), we run the whole calculus at the finite shadow WL N = ℤ/2^N ⋊ (ℤ/2^N)ˣ, which is a finite 2-group by cardinality. All the sharp 2-adic input (the orientation values, η⁻¹ = −3, v₂(X−1) = v₂(S−1) = 2, v₂(Y+1) = 3) stays in ℤ₂ and is pushed down by the reduction ring hom.

@[reducible, inline]

abbrev GQ2.Roe.Labute.WL (N : ℕ) : Type

The finite lift group ℤ/2^N ⋊ (ℤ/2^N)ˣ (WordLift, product law (u,g)(v,h) = (u + g·v, gh)): the mod-2^N shadow of Labute's ℤ₂(χ) ⋊ ℤ₂ˣ.

Equations

• GQ2.Roe.Labute.WL N = GQ2.FoxH.WordLift (ZMod (2 ^ N)) (ZMod (2 ^ N))ˣ

@[implicit_reducible]

def GQ2.Roe.Labute.instTopologicalSpaceWL (N : ℕ) : TopologicalSpace (WL N)

Equations

• GQ2.Roe.Labute.instTopologicalSpaceWL N = ⊥

theorem GQ2.Roe.Labute.instDiscreteTopologyWL (N : ℕ) : DiscreteTopology (WL N)

@[implicit_reducible]

def GQ2.Roe.Labute.instTopUnitsZMod (N : ℕ) : TopologicalSpace (ZMod (2 ^ N))ˣ

Equations

• GQ2.Roe.Labute.instTopUnitsZMod N = ⊥

theorem GQ2.Roe.Labute.instDiscUnitsZMod (N : ℕ) : DiscreteTopology (ZMod (2 ^ N))ˣ

noncomputable def GQ2.Roe.Labute.redWL (N : ℕ) : FoxH.WordLift ℤ_[2] ℤ_[2]ˣ →* WL N

The reduction ℤ₂ ⋊ ℤ₂ˣ → ℤ/2^N ⋊ (ℤ/2^N)ˣ (a group hom: reduction is a ring hom, so it intertwines the two product laws).

Equations

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

@[simp]

theorem GQ2.Roe.Labute.redWL_g (N : ℕ) (p : FoxH.WordLift ℤ_[2] ℤ_[2]ˣ) : ((redWL N) p).g = (Units.map ↑(PadicInt.toZModPow N)) p.g

2-power divisibility in ℤ/2^N, read through the reductions

theorem GQ2.Roe.Labute.two_pow_dvd_toZModPow_iff {N j : ℕ} (hj : j ≤ N) {x : ℤ_[2]} : 2 ^ j ∣ (PadicInt.toZModPow N) x ↔ 2 ^ j ∣ x

Divisibility by 2^j in ℤ/2^N is read off any 2-adic lift (j ≤ N).

The congruence filtration of WL N and the λ-bound

The derivations out of the two towers

noncomputable def GQ2.Roe.Labute.derivR (N : ℕ) (hN : 1 ≤ N) (v : Fin 3 → ℤ_[2]) : ↑DR.toProfinite.toTop →ₜ* WL N

Direction 1: the derivation D_R → WL N with generator data (v i, χ_R). It exists because χ_R is Labute's orientation — every crossed derivation kills r₂ (isLabuteOrientation_chiR), which is exactly the relator hypothesis drLiftHom wants.

Equations

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

@[simp]

theorem GQ2.Roe.Labute.derivR_drS (N : ℕ) (hN : 1 ≤ N) (v : Fin 3 → ℤ_[2]) : (derivR N hN v) drS = (redWL N) { u := v 0, g := chiR drS }

@[simp]

theorem GQ2.Roe.Labute.derivR_drX (N : ℕ) (hN : 1 ≤ N) (v : Fin 3 → ℤ_[2]) : (derivR N hN v) drX = (redWL N) { u := v 1, g := chiR drX }

@[simp]

theorem GQ2.Roe.Labute.derivR_drY (N : ℕ) (hN : 1 ≤ N) (v : Fin 3 → ℤ_[2]) : (derivR N hN v) drY = (redWL N) { u := v 2, g := chiR drY }

theorem GQ2.Roe.Labute.derivR_base (N : ℕ) (hN : 1 ≤ N) (v : Fin 3 → ℤ_[2]) (a : ↑DR.toProfinite.toTop) : ((derivR N hN v) a).g = (Units.map ↑(PadicInt.toZModPow N)) (chiR a)

The base component is χ_R (mod 2^N): both sides are continuous homs D_R → (ℤ/2^N)ˣ agreeing on s, x, y, so dr_hom_ext applies. The right-hand side is continuous because it factors through the discrete level quotient Q_N.

theorem GQ2.Roe.Labute.d0Word_wordLift_target (Da Ds Dy : ℤ_[2]) : d0Word { u := Da, g := -1 } { u := Ds, g := 1 } { u := Dy, g := etaUnit } = 1

The r₀-side Labute datum: with the orientation values (−1, 1, η) every crossed derivation kills r₀ = A²S⁴[S,Y]. The computation is the one 2-adic miracle behind SL1: the S⁴-block contributes 4·Ds and the commutator (η⁻¹ − 1)·Ds, and η⁻¹ = −3 exactly, so the total (3 + η⁻¹)·Ds vanishes on the nose.

noncomputable def GQ2.Roe.Labute.deriv0 (N : ℕ) (hN : 1 ≤ N) (v : Fin 3 → ℤ_[2]) : ↑D0.toProfinite.toTop →ₜ* WL N

Direction 2: the derivation D₀ → WL N with generator data (v i, (−1, 1, η)).

Equations

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

@[simp]

theorem GQ2.Roe.Labute.deriv0_d0A (N : ℕ) (hN : 1 ≤ N) (v : Fin 3 → ℤ_[2]) : (deriv0 N hN v) d0A = (redWL N) { u := v 0, g := -1 }

@[simp]

theorem GQ2.Roe.Labute.deriv0_d0S (N : ℕ) (hN : 1 ≤ N) (v : Fin 3 → ℤ_[2]) : (deriv0 N hN v) d0S = (redWL N) { u := v 1, g := 1 }

@[simp]

theorem GQ2.Roe.Labute.deriv0_d0Y (N : ℕ) (hN : 1 ≤ N) (v : Fin 3 → ℤ_[2]) : (deriv0 N hN v) d0Y = (redWL N) { u := v 2, g := etaUnit }

theorem GQ2.Roe.Labute.deriv0_base (N : ℕ) (hN : 1 ≤ N) (v : Fin 3 → ℤ_[2]) (a : ↑D0.toProfinite.toTop) : ((deriv0 N hN v) a).g = (Units.map ↑(PadicInt.toZModPow N)) (chiD0pres a)

The base component of the D₀-derivation is the mod-2^N shadow of χ₀.

The derivation kernel in Zₖ, and the tail pairing

theorem GQ2.Roe.Labute.deriv_mem_wlCong {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : ℕ} (hN : 1 ≤ N) (Φ : G →ₜ* WL N) {j : ℕ} (hj : 1 ≤ j) {a : G} (ha : a ∈ twoCentralSeries G j) : Φ a ∈ GQ2.Roe.Labute.wlCong✝ N j

Transport of the filtration bound λ_j(WL N) ⊆ K_j to the tower along a derivation.

def GQ2.Roe.Labute.derivKer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : ℕ} (Φ : G →ₜ* WL N) (k : ℕ) : Subgroup (levelQuot G (k + 1))

The vanishing subgroup 𝒜_Φ ⊆ Q_{k+1}: classes admitting a λₖ-representative whose derivation offset is divisible by 2^k. This is the Lean form of "the coker functional digit_{k-1} ∘ D vanishes"; derivKer_dvd shows the condition does not depend on the representative.

Equations

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

Additivity of the shift word in the modification (Im d̄ is a subgroup)

SL1 must produce a single modification, so the d̄-image has to be closed under products. It is: every factor of d̄ is 𝔽₂-linear in w up to central corrections, and for k ≥ 3 all corrections lie in Zₖ, which is central.

theorem GQ2.Roe.Labute.central_shuffle3 {H : Type u_2} [Group H] {A B C A' B' C' : H} (hA' : ∀ (t : H), A' * t = t * A') (hB' : ∀ (t : H), B' * t = t * B') : A * A' * (B * B') * (C * C') = A * B * C * (A' * B' * C')

Interleaving three central pairs.

theorem GQ2.Roe.Labute.dbarWordR0_mul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (k : ℕ) (hk : 3 ≤ k) (a s y : levelQuot G (k + 1)) {w w' : Fin 3 → levelQuot G (k + 1)} (hw : ∀ (i : Fin 3), w i ∈ lambdaImage G (k - 1) (k + 1)) (hw' : ∀ (i : Fin 3), w' i ∈ lambdaImage G (k - 1) (k + 1)) : (dbarWordR0 a s y fun (i : Fin 3) => w i * w' i) = dbarWordR0 a s y w * dbarWordR0 a s y w'

Additivity of d̄ in the modification, r₀-side.

theorem GQ2.Roe.Labute.dbarWordR2_mul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (k : ℕ) (hk : 3 ≤ k) (s x y : levelQuot G (k + 1)) {w w' : Fin 3 → levelQuot G (k + 1)} (hw : ∀ (i : Fin 3), w i ∈ lambdaImage G (k - 1) (k + 1)) (hw' : ∀ (i : Fin 3), w' i ∈ lambdaImage G (k - 1) (k + 1)) : (dbarWordR2 s x y fun (i : Fin 3) => w i * w' i) = dbarWordR2 s x y w * dbarWordR2 s x y w'

Additivity of d̄ in the modification, r₂-side.

theorem GQ2.Roe.Labute.dbarWordR0_mem_zLayer {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (hk : 3 ≤ k) (a s y : levelQuot G (k + 1)) {w : Fin 3 → levelQuot G (k + 1)} (hw : ∀ (i : Fin 3), w i ∈ lambdaImage G (k - 1) (k + 1)) : dbarWordR0 a s y w ∈ zLayer G k

The shift word lands in the central layer Zₖ.

theorem GQ2.Roe.Labute.dbarWordR2_mem_zLayer {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (hk : 3 ≤ k) (s x y : levelQuot G (k + 1)) {w : Fin 3 → levelQuot G (k + 1)} (hw : ∀ (i : Fin 3), w i ∈ lambdaImage G (k - 1) (k + 1)) : dbarWordR2 s x y w ∈ zLayer G k

The endgame: the coordinate derivations separate the two tails

theorem GQ2.Roe.Labute.tail_parity {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N k : ℕ} (hk : 3 ≤ k) (hN : 1 ≤ N) (hkN : k ≤ N) (Φ : (Fin 3 → ℤ_[2]) → G →ₜ* WL N) {x y : G} {ux uy : ℤ_[2]} (hux : 2 ^ 2 ∣ ux - 1) (huy : 2 ^ 2 ∣ uy - 1) (hgx : ∀ (v : Fin 3 → ℤ_[2]), ↑((Φ v) x).g = (PadicInt.toZModPow N) ux) (hgy : ∀ (v : Fin 3 → ℤ_[2]), ↑((Φ v) y).g = (PadicInt.toZModPow N) uy) (α β : ℕ) (hmem : ∀ (v : Fin 3 → ℤ_[2]), (levelMk G (k + 1)) ((x ^ 2 ^ (k - 1)) ^ α * (y ^ 2 ^ (k - 1)) ^ β) ∈ derivKer (Φ v) k) : ↑α • GQ2.Roe.Labute.thetaVec✝ hN Φ x + ↑β • GQ2.Roe.Labute.thetaVec✝ hN Φ y = 0

The tail parity relation: if a tail combination lies in every coordinate derivation's kernel, the two coordinate vectors satisfy the corresponding 𝔽₂-linear relation.

theorem GQ2.Roe.Labute.thetaVec_indep {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N k : ℕ} (hN : 1 ≤ N) (hk : 1 ≤ k) (Φ : (Fin 3 → ℤ_[2]) → G →ₜ* WL N) (gen a : Fin 3 → G) (hgenval : ∀ (v : Fin 3 → ℤ_[2]) (j : Fin 3), ((Φ v) (gen j)).u = (PadicInt.toZModPow N) (v j)) (hgent : Subgroup.closure (Set.range fun (i : Fin 3) => (levelMk G (k + 1)) (a i)) = ⊤) {c : Fin 3 → ZMod (2 ^ 1)} (hc : c 0 • GQ2.Roe.Labute.thetaVec✝ hN Φ (a 0) + c 1 • GQ2.Roe.Labute.thetaVec✝ hN Φ (a 1) + c 2 • GQ2.Roe.Labute.thetaVec✝ hN Φ (a 2) = 0) : c = 0

Independence of a generating triple's coordinate vectors. The coordinate map 𝔽₂³ → 𝔽₂³, c ↦ ∑ cᵢ·θ(aᵢ), hits the standard basis (the classes of the aᵢ generate Q_{k+1}, and θ factors through it), hence is onto, hence — same finite type — injective.