Reference words and SL1

Piece 5/6 of GQ2.Roe.Labute.StageLemma (see that module for the mathematical overview and the statement freeze). The congruence bookkeeping at the pinned targets, then the two reachability statements stageSL1R0 / stageSL1R2.

The congruence bookkeeping: reference words at the pinned targets

Both "functional vanishes" statements (φ(δ) = 0 and φ(Im d̄) = 0) are proved by comparison: the actual triple is congruent, modulo the two-sided congruence subgroup wlKer N k, to a reference triple whose χ-values are the pinned targets exactly. At the reference the word value is computed in closed form — and vanishes, by Labute's descent datum (for δ) or by the target valuations (for d̄).

The stage lemma: SL1, SL2, and the step (spike §2.4)

theorem GQ2.Roe.Labute.stageSL1R0 (k : ℕ) (hk : 3 ≤ k) {T : Fin 3 → levelQuot (↑DR.toProfinite.toTop) k} (hT : T ∈ sPR0 k) : ∃ (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 = (defectR0 k T)⁻¹

SL1 (reachability), direction 1: for T ∈ S^P_ₖ (k ≥ 3), the defect is reachable — some λ_{k-1}-modification's shift equals δ(T)⁻¹ (inverse form; in Zₖ inverses are trivial, so this is the memo's δₖ(T) ∈ Im d̄ₖ(T)). This is where the invariant P earns its keep: the spike's census shows the statement is false without the χ-clause (192/192 P-violating classes unreachable at k = 4). Fill: L4b (span theorem + the two separating functionals of spike §2.5(b)).

theorem GQ2.Roe.Labute.stageSL1R2 (k : ℕ) (hk : 3 ≤ k) {T : Fin 3 → levelQuot (↑D0.toProfinite.toTop) k} (hT : T ∈ sPR2 k) : ∃ (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 = (defectR2 k T)⁻¹

SL1 (reachability), direction 2. Fill: L4b.