GL-C: the span base case k = 3

Design record: docs/orchestration/span-gradedlie-plan.md §2.2 (which follows L4b's by-hand closure of k = 3 — "colπ-at-π-towers, tails, left-normed columns"). Statements frozen (GL0); fills ticket GL-C.

Q₄(F₃) has order 2^23 — no decide; the proof is structural. Everything happens in Q₄ = levelQuot freeProTwo 4, where the λ-calculus is exact (λ₄-image = ⊥), so no "mod λ" bookkeeping is needed anywhere:

• Λ₂ := lambdaImage _ 2 4 is abelian ([λ₂,λ₂] ⊆ λ₄ = 1);
• Λ₃ := lambdaImage _ 3 4 = zLayer _ 3 is central of exponent 2;
• every commP lands in Λ₂, every square lands in Λ₂, every commP against a Λ₂-element lands in Λ₃.

The two frozen statements are instances of one private core lemma span_base_core, parameterized by the twisted generator τ = mgen t (r₀: t = 0; r₂: t = 2) and the two bracket/tail generators. The route (orchestrator-derived ordering — the naive "triples first" order is circular):

1. Generator fourth powers. β⁴ are the two tails (2^{3-1} = 4); τ⁴ is the twisted column at the modification τ², where commP (τ²) τ = 1 (diagonal trick).
2. Squares of generator brackets. The exact identity commP u g ^ 2 = commP (u²) g · (commP (commP u g) u)⁻¹ (commP_sq_eq) at u = β: the first factor is a single-slot column at the modification β² ∈ Λ₂ (or the twisted column corrected by β⁴), the second is a single-slot column at the modification commP β g ∈ Λ₂. commP_symm transports to the τ-left pairs.
3. Squares of all brackets. (a, b) ↦ (commP a b)² is exactly bimultiplicative in Q₄ (commP_sq_mul_left/right: the corrections are Λ₃-central involutions and Λ₂-elements commute), so two closure inductions reduce to step 2. This replaces the memo's word-length induction: no measure is needed.
4. Fourth powers. (ab)⁴ = a⁴·b⁴·(commP b a)² exactly (pow_four_mul), so {a | a⁴ ∈ K} is a subgroup once step 3 is known; step 1 seeds the generators.
5. key_sq: v² ∈ K for all v ∈ Λ₂, by lambdaImage_induction at j = 1 — the two atom families are exactly steps 3 and 4.
6. Bracket atoms: commP v g ∈ K for v ∈ Λ₂ and all g (β-slots directly, the τ-slot after dividing the twisted column by v² ∈ K from step 5).
7. Assemble by lambdaImage_induction at j = 2.

No new axioms, no decide, no native_decide. Small private helpers restated binder-for-binder from StageLemma.lean (house precedent; this file must not import it).

Stage 0: pure group identities

Single-slot evaluations of the two shift words

Stage 0': the exact λ-calculus of Q₄

All statements below are for the level-4 quotient of an arbitrary pro-2-style G; the only input is lambdaImage G 4 4 = ⊥, which makes every "mod λ" congruence an equality.

The three exact identities

Support subgroups

Stage 0'': the marked classes generate Q₄(F₃)

The base case, role-generic core

The two frozen statements

theorem GQ2.Roe.Labute.span_base_r0 : zLayer (↑freeProTwo.toProfinite.toTop) 3 ≤ SpanTargetR0 3

The span base case, r₀ shape (memo §2.2). Fill: GL-C.

theorem GQ2.Roe.Labute.span_base_r2 : zLayer (↑freeProTwo.toProfinite.toTop) 3 ≤ SpanTargetR2 3

The span base case, r₂ shape. Fill: GL-C.