The shift formula, modification stability, and the span theorem #
Piece 2/6 of GQ2.Roe.Labute.StageLemma (see that module for the mathematical overview
and the statement freeze). Contains the transported shift formulas defectR0_mul /
defectR2_mul, the level-k modification facts feeding sPR0_mul_mem / sPR2_mul_mem,
the Frattini generation transfer, and the span theorem span_free_* / span_descent_*.
Shift formula and modification stability (spike §2.1–2.2; concrete towers) #
The transported shift formula, direction 1 (spike §2.2, machine-verified 24/24):
modifying a level-k triple by the projection of a λ_{k-1}-modification w shifts the
defect by exactly d̄(w) at the canonical lift. No relator hypothesis: the identity is
pure k ≥ 3 λ-calculus. Fill: L4a.
The transported shift formula, direction 2. Fill: L4a.
Level-k modification facts (L4a fill helpers) #
At its own level a λ_{k-1}-modification is already central of exponent 2 in Qₖ — both
v² and commP v g land in λₖ, which is trivial in Qₖ. So the relator clause of S⁰ₖ
is preserved for the cheapest possible reason, and the χ-clause survives because
χ(λ_{k-1}) ⊆ 1 + 2^kℤ₂ — one digit sharper than chiShadow_eq_one_of_mem gives, which is
exactly the design reason the invariant P is stated at modulus 2^k.
The χ-clause survives (spike §2.1's design reason for the modulus 2^k): a character
kills λ_{k-1} to precision 2^k, one digit sharper than the generic layer bound, because
λ_{k-1}(ℤ₂ˣ) ⊆ 1 + 2^kℤ₂ (twoCentralSeries_units_le at index k - 1).
D_R is topologically generated by {s, x, y}, Finset form (private replica of the
Assembly-file packaging of dr_topGen; needed here for the tower instance pack).
D₀ is topologically generated by {A, S, Y}, Finset form (private replica).
Frattini generation transfer (the non-generator argument at the level quotients) #
λ₂ is Frattini in every level quotient: the image λ₂λₘ/λₘ ≤ Qₘ lies in the
Frattini-like subgroup Φ(Qₘ) = Qₘ²[Qₘ, Qₘ] (SectionSeven.frattiniLike ⊤). Immediate
from the atomization principle lambdaImage_induction at j = 1 (λ₁ = ⊤): λ₂ is
verbally generated by squares and commutators of λ₁-elements, and both kinds of residue
are Frattini generators.
Generation transfer (Frattini non-generation): a generating family T of a level
quotient Qₘ stays generating after each member is multiplied by an element of the
λ₂-image. Indeed T i = (T i · u i) · (u i)⁻¹ puts ⟨T⟩ = ⊤ inside H ⊔ λ₂, where
H = ⟨T · u⟩; since Qₘ is a finite 2-group and λ₂ ≤ Φ(Qₘ), Frattini non-generation
(frattiniLike_nongen) upgrades H ⊔ Φ(Qₘ) = ⊤ to H = ⊤.
Modification stability of S^P_ₖ, direction 1 (spike §2.1 + §2.4): λ_{k-1}-moves
preserve all three clauses — relator kill (the shift lands in λₖ), generation
(Frattini: λ_{k-1} ⊆ λ₂ for k ≥ 3), and the χ-clause (χ(λ_{k-1}) ⊆ 1 + 2^k ℤ₂ — the
design reason P survives the calculus). Fill: L4a.
Modification stability, direction 2. Fill: L4a.
The span theorem (spike §2.3; L4b) #
The span theorem, free form, r₀-shape (spike §2.3; Serre 252 §7 p. 151 with the
2^{h-1} erratum): for k ≥ 3, the graded layer Zₖ(F₃) is contained in the subgroup
generated by the d̄-image over λ_{k-1}-modifications at the standard generators
together with the two adapted tails g₁^{2^{k-1}}, g₂^{2^{k-1}} (the non-π'd generators
(S, Y)-slots = generators 1, 2). Machine-verified k ≤ 5 free / k ≤ 6 towers
(20/20 rank rows). Fill: L4b — via the structural reduction of spike §2.5(a); on a snag,
plan §7 O1/O2 apply (owner gate).
The span theorem, free form, r₂-shape: tails at the (s, x)-slots = generators
0, 1 (the relator-adapted pair — spike §2.3's caught wrong-pair failure makes this
placement load-bearing). Fill: L4b.
Span descent, direction 1 (spike §2.3: λ is verbal, so the statement descends
along F₃ ↠ D_R and holds at any generating triple of Q_{k+1}(D_R); tails at the
(S, Y)-slots of the triple). Fill: L4b (from span_free_r0 + map_twoCentralSeries_eq
- the congruence calculus).
Span descent, direction 2 (tails at the (s, x)-slots). Fill: L4b.