Span-theorem foundation: shift words, grading, descent infra, the free pro-2 group

(GL-campaign ticket GL0)

Text-moved out of StageLemma.lean (2026-07-26, statements byte-identical) so that the GL-campaign files (GQ2/Roe/Labute/GradedLie/) can sit below StageLemma.lean in the import graph: StageLemma imports GradedLie.SpanAssembly, which needs the definitions here. Design record: docs/orchestration/span-gradedlie-plan.md.

Contents (in original StageLemma.lean order):

• the shift word shapes dbarWordR0 / dbarWordR2 and their smoke lemmas;
• the λ-grading lemma (GRAD) section;
• the descent infrastructure (lambdaImage_induction and friends);
• the free pro-2 group freeProTwo, its marked generators, universal property and topological generation (freeTopGenFinset made public in the move — the GL fills need the hfg-hypothesis shape);
• NEW (GL0): the span-target subgroups SpanTargetR0/R2 — the verbatim right-hand sides of the frozen span_free_r0/r2 statements, kept as plain defs so the StageLemma fills are definitional.

The shift word shapes

def GQ2.Roe.Labute.dbarWordR0 {G : Type u_1} [Group G] (a s y : G) (w : Fin 3 → G) : G

The r₀-side defect-shift word d̄(w) = w₁²·[w₁,a]·[w₂,y]·[w₃,s] at the triple (a, s, y) (spike §2.2; repo commP). A word shape in any group; its homomorphism property on Z-layer classes is part of the L4a calculus, not of the definition.

Equations

• GQ2.Roe.Labute.dbarWordR0 a s y w = w 0 ^ 2 * GQ2.commP (w 0) a * GQ2.commP (w 1) y * GQ2.commP (w 2) s

def GQ2.Roe.Labute.dbarWordR2 {G : Type u_1} [Group G] (s x y : G) (w : Fin 3 → G) : G

The r₂-side defect-shift word d̄(u,v,w) = w²·[w,y]·[u,x]·[v,s] at the triple (s, x, y) (spike §2.2 — note the r₂-tails/cross-terms pair (u,x), (v,s), not the draft's (x, y) pairing).

Equations

• GQ2.Roe.Labute.dbarWordR2 s x y w = w 2 ^ 2 * GQ2.commP (w 2) y * GQ2.commP (w 0) x * GQ2.commP (w 1) s

theorem GQ2.Roe.Labute.map_dbarWordR0 {F : Type u_1} {G : Type u_2} {H : Type u_3} [Group G] [Group H] [FunLike F G H] [MonoidHomClass F G H] (φ : F) (a s y : G) (w : Fin 3 → G) : φ (dbarWordR0 a s y w) = dbarWordR0 (φ a) (φ s) (φ y) fun (i : Fin 3) => φ (w i)

Naturality of the r₀-shift word (smoke).

theorem GQ2.Roe.Labute.map_dbarWordR2 {F : Type u_1} {G : Type u_2} {H : Type u_3} [Group G] [Group H] [FunLike F G H] [MonoidHomClass F G H] (φ : F) (s x y : G) (w : Fin 3 → G) : φ (dbarWordR2 s x y w) = dbarWordR2 (φ s) (φ x) (φ y) fun (i : Fin 3) => φ (w i)

Naturality of the r₂-shift word (smoke).

theorem GQ2.Roe.Labute.dbarWordR0_comm {G : Type u_1} [CommGroup G] (a s y : G) (w : Fin 3 → G) : dbarWordR0 a s y w = w 0 ^ 2

Abelian collapse (smoke): only the square survives — the cross terms are honest commutators.

theorem GQ2.Roe.Labute.dbarWordR0_one {G : Type u_1} [Group G] (a s y : G) : (dbarWordR0 a s y fun (x : Fin 3) => 1) = 1

Trivial modification, trivial shift (smoke).

theorem GQ2.Roe.Labute.dbarWordR2_one {G : Type u_1} [Group G] (s x y : G) : (dbarWordR2 s x y fun (x : Fin 3) => 1) = 1

Trivial modification, trivial shift, r₂ side (smoke).

The λ-grading lemma (L4b fill helper; Hall–Witt calculus)

⁅λₐ, λᵦ⁆ ≤ λ_{a+b} — the graded-bracket bound underlying every depth estimate of the span reduction (spike §2.5(a)'s identity list). Proved by induction on b via the three subgroups lemma (transported from mathlib's ⊥-form through the quotient by λ_{a+b}) and the closed-subgroup trick for the topological closure step.

theorem GQ2.Roe.Labute.commutator_commutator_le_of_rotate {G : Type u_1} [Group G] {A B C N : Subgroup G} [N.Normal] (h1 : ⁅⁅B, C⁆, A⁆ ≤ N) (h2 : ⁅⁅C, A⁆, B⁆ ≤ N) : ⁅⁅A, B⁆, C⁆ ≤ N

The three subgroups lemma, ≤ N-form: transport of Subgroup.commutator_commutator_eq_bot_of_rotate through G ⧸ N.

theorem GQ2.Roe.Labute.commutator_twoCentralSeries_top_le (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : ℕ) : ⁅twoCentralSeries G a, ⊤⁆ ≤ twoCentralSeries G (a + 1)

One-step bound, subgroup form: ⁅λₐ, ⊤⁆ ≤ λ_{a+1}.

theorem GQ2.Roe.Labute.commutator_twoCentralSeries_le (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (b a : ℕ) : ⁅twoCentralSeries G a, twoCentralSeries G b⁆ ≤ twoCentralSeries G (a + b)

The λ-grading lemma (GRAD): ⁅λₐ, λᵦ⁆ ≤ λ_{a+b}.

theorem GQ2.Roe.Labute.commutator_mem_twoCentralSeries_add (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {a b : ℕ} {v h : G} (hv : v ∈ twoCentralSeries G a) (hh : h ∈ twoCentralSeries G b) : ⁅v, h⁆ ∈ twoCentralSeries G (a + b)

Element form of the grading lemma.

Descent infrastructure (L4b fill helpers; not part of the frozen interface)

For a topologically f.g. pro-2 G the level quotients are finite discrete groups, the λ-series of Qₘ is the image of the λ-series of G (map_twoCentralSeries_eq along levelMk), and in particular λₘ(Qₘ) = ⊥. These are the transport facts through which the free span statement descends to the towers.

theorem GQ2.Roe.Labute.discreteTopology_levelQuot (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hpro : IsProP 2 G) (m : ℕ) : DiscreteTopology (levelQuot G m)

The level quotients of a topologically f.g. pro-2 group are discrete (λₘ is open).

theorem GQ2.Roe.Labute.continuous_levelMk (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) : Continuous ⇑(levelMk G m)

The canonical projection levelMk is continuous.

theorem GQ2.Roe.Labute.lambdaImage_eq_twoCentralSeries_levelQuot (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hpro : IsProP 2 G) (j m : ℕ) : lambdaImage G j m = twoCentralSeries (levelQuot G m) j

λ-transport along levelMk: the two-index image λⱼλₘ/λₘ is the j-th layer of the λ-series of the level quotient Qₘ (verbal functoriality for the continuous epi levelMk, using discreteness of the target).

theorem GQ2.Roe.Labute.twoCentralSeries_levelQuot_self (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hpro : IsProP 2 G) (m : ℕ) : twoCentralSeries (levelQuot G m) m = ⊥

The λ-series of the level-m quotient vanishes at level m.

theorem GQ2.Roe.Labute.map_topologicalClosure_eq_of_discrete (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [DiscreteTopology H] (K : Subgroup G) (f : G →* H) (hf : Continuous ⇑f) : Subgroup.map f K.topologicalClosure = Subgroup.map f K

Mapping into a discrete group erases topological closures: the image of cl K is the image of K (the preimage of the image subgroup is clopen).

theorem GQ2.Roe.Labute.lambdaImage_induction (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hpro : IsProP 2 G) {j m : ℕ} (hj : 1 ≤ j) {p : levelQuot G m → Prop} (hsq : ∀ v ∈ twoCentralSeries G j, p ((levelMk G m) (v ^ 2))) (hbr : ∀ v ∈ twoCentralSeries G j, ∀ (g : G), p ((levelMk G m) ⁅v, g⁆)) (hone : p 1) (hmul : ∀ (x y : levelQuot G m), p x → p y → p (x * y)) (hinv : ∀ (x : levelQuot G m), p x → p x⁻¹) {q : levelQuot G m} (hq : q ∈ lambdaImage G (j + 1) m) : p q

Atomization of the layer images (L4b workhorse): for topologically f.g. pro-2 G, a property closed under the group operations that holds on the residues of squares v² and brackets ⁅v, g⁆ (v ∈ λⱼ, g ∈ G) holds on all of λ_{j+1}λₘ/λₘ ≤ Qₘ. This is the mod-λₘ shadow of the verbal generation of λ_{j+1}, with the topological closure erased by discreteness of the finite quotient.

The free pro-2 group on three generators

noncomputable def GQ2.Roe.Labute.freeProTwo : ProfiniteGrp.{0}

The free pro-2 group F₃ on three generators — the only group in which the span theorem is proved (spike §2.3: "The Lean statement only ever needs the free version"); the towers receive it by descent.

Equations

• GQ2.Roe.Labute.freeProTwo = GQ2.maxProPQuotient 2 ↑(GQ2.FreeProfiniteGroup (Fin 3)).toProfinite.toTop

noncomputable def GQ2.Roe.Labute.freeGen (i : Fin 3) : ↑freeProTwo.toProfinite.toTop

The marked generators of F₃.

Equations

• GQ2.Roe.Labute.freeGen i = (GQ2.maxProPMk 2 ↑(GQ2.FreeProfiniteGroup (Fin 3)).toProfinite.toTop) (GQ2.FreeProfiniteGroup.of i)

noncomputable def GQ2.Roe.Labute.freeProTwoLift {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] (hH : IsProP 2 H) (m : Fin 3 → H) : ↑freeProTwo.toProfinite.toTop →ₜ* H

Universal property of F₃ (L4b helper): a bare triple in a pro-2 group H classifies a continuous hom F₃ → H — drLiftHom/d0LiftHom without the relator step.

Equations

• GQ2.Roe.Labute.freeProTwoLift hH m = (GQ2.maxProPHomEquiv hH).symm (ProfiniteGrp.Hom.hom ((GQ2.FreeProfiniteGroup.homEquiv (Fin 3) (ProfiniteGrp.of H)).symm m))

@[simp]

theorem GQ2.Roe.Labute.freeProTwoLift_freeGen {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] (hH : IsProP 2 H) (m : Fin 3 → H) (i : Fin 3) : (freeProTwoLift hH m) (freeGen i) = m i

theorem GQ2.Roe.Labute.topGen_freeProTwo : (Subgroup.closure (Set.range freeGen)).topologicalClosure = ⊤

F₃ is topologically generated by its marked generators (density of the abstract free group in its profinite completion — ProfiniteGrp.ProfiniteCompletion.denseRange — pushed through the surjective pro-2 projection; the AdmissibleLimit.lean generation pattern).

theorem GQ2.Roe.Labute.freeTopGenFinset : ∃ (s : Finset ↑freeProTwo.toProfinite.toTop), (Subgroup.closure ↑s).topologicalClosure = ⊤

Finset form of topGen_freeProTwo (the hfg-hypothesis shape of the tower API; made public in the GL0 move — the GL fills need it for the instance pack).

The span-target subgroups (GL0)

The verbatim right-hand sides of the frozen span_free_r0/r2 statements, as plain (rfl-transparent) defs: span_free_r0 in StageLemma.lean is filled by span_free_r0_proof k hk : zLayer … k ≤ SpanTargetR0 k definitionally. Do NOT restate or unfold-normalize these — the expressions must stay literally identical to the frozen statement bodies.

noncomputable def GQ2.Roe.Labute.SpanTargetR0 (k : ℕ) : Subgroup (levelQuot (↑freeProTwo.toProfinite.toTop) (k + 1))

The r₀ span target: d̄-image over λ_{k-1}-modifications at the marked generators, together with the (S, Y)-tails (generators 1, 2).

Equations

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

noncomputable def GQ2.Roe.Labute.SpanTargetR2 (k : ℕ) : Subgroup (levelQuot (↑freeProTwo.toProfinite.toTop) (k + 1))

The r₂ span target: tails at the (s, x)-slots = generators 0, 1 (the relator-adapted pair).

Equations

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