GL-B: the span induction step

Design record: docs/orchestration/span-gradedlie-plan.md §2.1. Statements frozen (GL0); fills ticket GL-B. May cite the (possibly still sorried) GL-A statements — axiom prints self-heal when GL-A lands (house pattern).

Proof shape (successor form, S(k) ⇒ S(k+1) for k ≥ 3, so the transport threshold k+1 ≥ 4 is automatic):

1. Atomize zLayer (k+1) by lambdaImage_induction at j = k (in Q_{k+2}): sq-atoms mk(v²) and bracket-atoms mk⁅v,g⁆, v ∈ λ_k, g ambient.
2. Bracket atoms: reduce g to the marked generator classes (commP_mul_right_of_mem/commP_inv_right_of_mem + closure_levelMk_freeGen); then commP v β IS a single-slot d̄-atom (dbarWord*_single₁/₂), and commP v τ = (v²)⁻¹ · d̄(twisted slot at v) (dbarWord*_single₀/₂), with v² a sq-atom.
3. Sq-atoms: levelProj sends v into zLayer k ⊆ Q_{k+1}; apply prev, pull the factorization back up (exists_levelProj_preimage_lambdaImage), absorb the zLayer (k+1)-defect (sq_mul_zLayer), split the square over the factors (sq_mul_of_mem_lambdaImage_pred), and transport per factor: tail lifts square to the level-(k+1) tails; d̄-atom lifts square via dbarWordR0_sq/dbarWordR2_sq to level-(k+1) d̄-atoms at the squared modifications.

Step 3 is packaged as the subgroup SpanStepAux.liftSq — the classes of Q_{k+1} that lift to λ_k(Q_{k+2}) with a controlled square — so that prev can be fed to it through Subgroup.closure_le; the one/mul/inv bookkeeping is then the subgroup structure itself and is shared by the two shapes, as are the layer-image calculus, the tail transport and the commutator-convention bridge.

Restated layer-image calculus

Private helpers restated binder-for-binder from StageLemma.lean (house precedent: the import direction — StageLemma imports this file — forbids importing it). They live in an auxiliary namespace so that nothing here can shadow a sibling file's interface.

Slot bookkeeping and the commutator-convention bridge

The free pro-2 group: marked classes and target membership

The lift-with-square subgroup (Phase 1 of the step, shape-independent)

Phase 1: the sq-atom engine

theorem GQ2.Roe.Labute.span_step_r0 (k : ℕ) (hk : 3 ≤ k) (prev : zLayer (↑freeProTwo.toProfinite.toTop) k ≤ SpanTargetR0 k) : zLayer (↑freeProTwo.toProfinite.toTop) (k + 1) ≤ SpanTargetR0 (k + 1)

The span induction step, r₀ shape (memo §2.1). Fill: GL-B.

theorem GQ2.Roe.Labute.span_step_r2 (k : ℕ) (hk : 3 ≤ k) (prev : zLayer (↑freeProTwo.toProfinite.toTop) k ≤ SpanTargetR2 k) : zLayer (↑freeProTwo.toProfinite.toTop) (k + 1) ≤ SpanTargetR2 (k + 1)

The span induction step, r₂ shape. Fill: GL-B.