SL2 and the stage step

Piece 6/6 of GQ2.Roe.Labute.StageLemma (see that module for the mathematical overview and the statement freeze). The two digit-adjustment statements stageSL2R0 / stageSL2R2, and the composability certificates stageStepR0 / stageStepR2 that Assembly.lean consumes.

theorem GQ2.Roe.Labute.stageSL2R0 (k : ℕ) (hk : 3 ≤ k) {T : Fin 3 → levelQuot (↑DR.toProfinite.toTop) k} (hT : T ∈ sPR0 k) (hδ : defectR0 k T = 1) : ∃ (w : Fin 3 → levelQuot (↑DR.toProfinite.toTop) (k + 1)), (∀ (i : Fin 3), w i ∈ lambdaImage (↑DR.toProfinite.toTop) (k - 1) (k + 1)) ∧ dbarWordR0 (canonLift (↑DR.toProfinite.toTop) k (T 0)) (canonLift (↑DR.toProfinite.toTop) k (T 1)) (canonLift (↑DR.toProfinite.toTop) k (T 2)) w = 1 ∧ (fun (i : Fin 3) => canonLift (↑DR.toProfinite.toTop) k (T i) * w i) ∈ sPR0 (k + 1)

SL2 (digit adjustment), direction 1: for T ∈ S^P_ₖ (k ≥ 3) with vanishing defect, some ker d̄-modification of the canonical lift lands in S^P_{k+1} — the memo's "ker d̄ₖ → (ℤ/2)² onto" in its consumed form (the digit bookkeeping, including the automatic vanishing of the π'd slot's fresh digit, is L4a's internal mechanism; the dimension-count fallback of spike §2.5(c) is equally admissible). Fill: L4a.

theorem GQ2.Roe.Labute.stageSL2R2 (k : ℕ) (hk : 3 ≤ k) {T : Fin 3 → levelQuot (↑D0.toProfinite.toTop) k} (hT : T ∈ sPR2 k) (hδ : defectR2 k T = 1) : ∃ (w : Fin 3 → levelQuot (↑D0.toProfinite.toTop) (k + 1)), (∀ (i : Fin 3), w i ∈ lambdaImage (↑D0.toProfinite.toTop) (k - 1) (k + 1)) ∧ dbarWordR2 (canonLift (↑D0.toProfinite.toTop) k (T 0)) (canonLift (↑D0.toProfinite.toTop) k (T 1)) (canonLift (↑D0.toProfinite.toTop) k (T 2)) w = 1 ∧ (fun (i : Fin 3) => canonLift (↑D0.toProfinite.toTop) k (T i) * w i) ∈ sPR2 (k + 1)

SL2 (digit adjustment), direction 2. Fill: L4a.

theorem GQ2.Roe.Labute.stageStepR0 (k : ℕ) (hk : 3 ≤ k) (h : (sPR0 k).Nonempty) : (sPR0 (k + 1)).Nonempty

The stage step, direction 1 (spike §2.4's conclusion; the exact interface the assembly consumes): S^P_ₖ ≠ ∅ → S^P_{k+1} ≠ ∅ for k ≥ 3.

Proved here from the frozen statements (SL1 → shift formula → modification stability → SL2) as the L1 composability certificate — no fill needed; it inherits the upstream sorries.

theorem GQ2.Roe.Labute.stageStepR2 (k : ℕ) (hk : 3 ≤ k) (h : (sPR2 k).Nonempty) : (sPR2 (k + 1)).Nonempty

The stage step, direction 2 (proved from the frozen statements; composability certificate).