GL-E: span assembly

The strong induction composing GL-C (base, k = 3) with GL-B (step). Complete as written (the GL0 composability certificate, L1's stageStep pattern) — it inherits the upstream sorries and self-heals as GL-B/GL-C land. StageLemma.lean's frozen span_free_r0/r2 are filled by these theorems definitionally (SpanTargetR0/R2 are the verbatim statement bodies).

theorem GQ2.Roe.Labute.span_free_r0_proof (k : ℕ) (hk : 3 ≤ k) : zLayer (↑freeProTwo.toProfinite.toTop) k ≤ SpanTargetR0 k

The span theorem, r₀ shape, in span-target form (= span_free_r0 verbatim).

theorem GQ2.Roe.Labute.span_free_r2_proof (k : ℕ) (hk : 3 ≤ k) : zLayer (↑freeProTwo.toProfinite.toTop) k ≤ SpanTargetR2 k

The span theorem, r₂ shape, in span-target form (= span_free_r2 verbatim).