The congruence calculus and the shift-calculus toolkit

Piece 1/6 of GQ2.Roe.Labute.StageLemma (see that module for the mathematical overview and the statement freeze). Generic pro-2 G at the calculus threshold k ≥ 3: the λ-congruence rules that make the shift words well defined on modification classes, and the pure group-identity toolkit (commP move rules, central reorderings) that the level shift computations run on.

The congruence calculus (spike §2.1; generic pro-2 G, k ≥ 3)

The full profinite instance pack is carried deliberately (the fills run through closed-map/compactness arguments on λ-layers); the three instantiations D_R, D₀, freeProTwo all satisfy it.

theorem GQ2.Roe.Labute.lambdaImage_self {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) : lambdaImage G m m = ⊥

λₘ dies in Qₘ (the top layer image is trivial).

theorem GQ2.Roe.Labute.lambdaImage_one_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) : lambdaImage G 1 m = ⊤

λ₁ = ⊤ survives to every level quotient.

theorem GQ2.Roe.Labute.commP_mem_lambdaImage_add {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {a b m : ℕ} {v g : levelQuot G m} (hv : v ∈ lambdaImage G a m) (hg : g ∈ lambdaImage G b m) : commP v g ∈ lambdaImage G (a + b) m

The λ-grading lemma, transported to the level quotients and to the repo commutator convention: commP λₐ λᵦ ⊆ λ_{a+b} in Qₘ.

theorem GQ2.Roe.Labute.dbarWordR0_congr_slots {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (k : ℕ) (hk : 3 ≤ k) {a s y a' s' y' : levelQuot G (k + 1)} (ha : a⁻¹ * a' ∈ lambdaImage G 2 (k + 1)) (hs : s⁻¹ * s' ∈ lambdaImage G 2 (k + 1)) (hy : y⁻¹ * y' ∈ lambdaImage G 2 (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 = dbarWordR0 a' s' y' w

Frattini-only dependence on the triple slots (spike §2.1: [v, g] depends only on g mod λ₂ for v ∈ λ_{k-1}; §4.3: worth its own lemma — it makes the census-style base-case checks small): the r₀-shift word is unchanged when the slots move by λ₂-classes. Fill: L4a.

theorem GQ2.Roe.Labute.dbarWordR2_congr_slots {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (k : ℕ) (hk : 3 ≤ k) {s x y s' x' y' : levelQuot G (k + 1)} (hs : s⁻¹ * s' ∈ lambdaImage G 2 (k + 1)) (hx : x⁻¹ * x' ∈ lambdaImage G 2 (k + 1)) (hy : y⁻¹ * y' ∈ lambdaImage G 2 (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 = dbarWordR2 s' x' y' w

Frattini-only dependence, r₂ side. Fill: L4a.

theorem GQ2.Roe.Labute.dbarWordR0_congr_mod {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)) (hww' : ∀ (i : Fin 3), (w i)⁻¹ * w' i ∈ lambdaImage G k (k + 1)) : dbarWordR0 a s y w = dbarWordR0 a s y w'

Z_{k-1}-class dependence on the modification (spike §2.1: v ↦ v² is 𝔽₂-linear on classes and [v, g] depends only on v mod λₖ): the r₀-shift word is unchanged when w moves by λₖ-classes. Fill: L4a.

theorem GQ2.Roe.Labute.dbarWordR2_congr_mod {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)) (hww' : ∀ (i : Fin 3), (w i)⁻¹ * w' i ∈ lambdaImage G k (k + 1)) : dbarWordR2 s x y w = dbarWordR2 s x y w'

Z_{k-1}-class dependence on the modification, r₂ side. Fill: L4a.

Shift-calculus toolkit (L4a fill helpers; not part of the frozen interface)

The whole shift computation runs on three facts about a modification v ∈ λ_{k-1} of Q_{k+1} with k ≥ 3: v² and every commP v g lie in the central involutive layer Zₖ, and v commutes with λ₂ outright ([λ₂, λ_{k-1}] ⊆ λ_{k+1} = 1). Everything else is the move rule v * a = a * v * commP v a, which is a pure group identity.

theorem GQ2.Roe.Labute.commP_mul_left {H : Type u_1} [Group H] (x u g : H) : commP (x * u) g = u⁻¹ * commP x g * u * commP u g

Left expansion of commP (pure group identity).

theorem GQ2.Roe.Labute.commP_mul_right {H : Type u_1} [Group H] (x g v : H) : commP x (g * v) = commP x v * (v⁻¹ * commP x g * v)

Right expansion of commP (pure group identity).

theorem GQ2.Roe.Labute.conj_eq_self_of_commP_eq_one {H : Type u_1} [Group H] {x u : H} (h : commP x u = 1) : u⁻¹ * x * u = x

A vanishing commP is exactly a trivial conjugation.

theorem GQ2.Roe.Labute.commP_eq_one_of_mul_comm {H : Type u_1} [Group H] {x y : H} (h : x * y = y * x) : commP x y = 1

Commuting elements have trivial commP (pure group identity).

theorem GQ2.Roe.Labute.lambdaImage_le_of_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j j' m : ℕ} (h : j ≤ j') : lambdaImage G j' m ≤ lambdaImage G j m

The layer images are antitone in the depth index.

theorem GQ2.Roe.Labute.sq_mem_zLayer {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (hk : 3 ≤ k) {v : levelQuot G (k + 1)} (hv : v ∈ lambdaImage G (k - 1) (k + 1)) : v ^ 2 ∈ zLayer G k

A λ_{k-1}-modification squares into the central layer.

theorem GQ2.Roe.Labute.commP_mem_zLayer {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (hk : 3 ≤ k) {v : levelQuot G (k + 1)} (hv : v ∈ lambdaImage G (k - 1) (k + 1)) (g : levelQuot G (k + 1)) : commP v g ∈ zLayer G k

Every commP of a λ_{k-1}-modification is central.

theorem GQ2.Roe.Labute.mul_comm_lambdaImage {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (k : ℕ) (hk : 3 ≤ k) {u v : levelQuot G (k + 1)} (hu : u ∈ lambdaImage G (k - 1) (k + 1)) (hv : v ∈ lambdaImage G (k - 1) (k + 1)) : u * v = v * u

theorem GQ2.Roe.Labute.drWord_mul_lambdaImage {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 : Fin 3 → levelQuot G (k + 1)} (hw : ∀ (i : Fin 3), w i ∈ lambdaImage G (k - 1) (k + 1)) : drWord (s * w 0) (x * w 1) (y * w 2) = drWord s x y * dbarWordR2 s x y w

The r₂ shift identity (spike §2.2): the x-block is π-inert but contributes both cross terms, the [y, y^s] block is fully inert, and the y² block gives the diagonal.

theorem GQ2.Roe.Labute.d0Word_mul_lambdaImage {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 : Fin 3 → levelQuot G (k + 1)} (hw : ∀ (i : Fin 3), w i ∈ lambdaImage G (k - 1) (k + 1)) : d0Word (a * w 0) (s * w 1) (y * w 2) = d0Word a s y * dbarWordR0 a s y w

The r₀ shift identity (spike §2.2): modifying the triple (a, s, y) by λ_{k-1}-elements multiplies the relator value by dbarWordR0 — the S⁴ block is inert, the A² block contributes the π-diagonal w₀²·[w₀,a], and [S,Y] the two cross terms.