The digit calculus, the χ-plumbing, and the kernel witnesses

Piece 3/6 of GQ2.Roe.Labute.StageLemma (see that module for the mathematical overview and the statement freeze). The 2-adic digit facts driving SL2 (lifting the exponent, the dichotomy, the automatic digit), the translation between χ-values and divisibility, and the explicit ker d̄ witnesses. Consumed by both SL1 and SL2.

The digit calculus (SL2's internal mechanism; spike §2.4, memo §1)

A level-k triple carries character values χ(Tᵢ) = targetᵢ·ρᵢ with ρᵢ ≡ 1 mod 2^k (the invariant P); SL2 must kill the fresh level-k digits of the ρᵢ. Three 2-adic facts do it, all proved here from scratch over ℤ₂ (parity steps run through the residue field 𝔽₂ = ZMod (2^1)):

• lifting the exponent (sharp_pow_two_pow): v₂(u − 1) = 2 forces v₂(u^{2^m} − 1) = m + 2. All three relevant orientation units are ≡ 5 (mod 8) (η, X, S — chiTargetR0_three, chiTargetR2_three), so their 2^{k-2}-powers have a sharp digit at level k — and the 1 mod 2^k deviation carried along by the actual triple is invisible there (sharp_move: its junk enters at 2^{2k-2}, and 2k − 2 ≥ k + 1 exactly when k ≥ 3);
• the dichotomy (dvd_or_dvd_mul): against such a move, one of ρ, ρ·μ is ≡ 1 mod 2^{k+1} — one move per free slot suffices;
• the automatic digit (dvd_succ_of_sq, memo §1.1): the slot carrying the relator's square needs no move at all. Its level-(k+1) clause follows from the level-(k+1) relator clause itself: the corrected word lies in λ_{k+1}, so its χ-value lies in 1 + 2^{k+2}ℤ₂ (twoCentralSeries_units_le at index k+1), and with the ⁴-slot contributing only at 2^{k+2} this reads ρ² ≡ 1 mod 2^{k+2}, forcing ρ ≡ 1 mod 2^{k+1}. Both exact target relations hold in ℤ₂ˣ on the nose: (−1)²·1⁴ = 1 and X⁻⁴·Y² = 1 (YvalUnit_sq_eq).

theorem GQ2.Roe.Labute.two_pow_dvd_iff {n : ℕ} {x : ℤ_[2]} : 2 ^ n ∣ x ↔ (PadicInt.toZModPow n) x = 0

2^n ∣ x read off the mod-2^n reduction.

theorem GQ2.Roe.Labute.two_not_dvd_mul {r m : ℤ_[2]} (hr : ¬2 ∣ r) (hm : ¬2 ∣ m) : ¬2 ∣ r * m

A product of odd 2-adic integers is odd.

theorem GQ2.Roe.Labute.two_not_dvd_one_add_two_mul (x : ℤ_[2]) : ¬2 ∣ 1 + 2 * x

1 + 2x is odd.

theorem GQ2.Roe.Labute.dvd_mul_sub_one {A B : ℤ_[2]} {n : ℕ} (hA : 2 ^ n ∣ A - 1) (hB : 2 ^ n ∣ B - 1) : 2 ^ n ∣ A * B - 1

Congruences to 1 multiply.

theorem GQ2.Roe.Labute.dvd_sub_one_of_mul {A B : ℤ_[2]} {n : ℕ} (h : 2 ^ n ∣ A * B - 1) (hB : 2 ^ n ∣ B - 1) : 2 ^ n ∣ A - 1

Congruences to 1 cancel.

theorem GQ2.Roe.Labute.dvd_pow_sub_one {A : ℤ_[2]} {n : ℕ} (hA : 2 ^ n ∣ A - 1) (b : ℕ) : 2 ^ n ∣ A ^ b - 1

Congruences to 1 are inherited by powers.

theorem GQ2.Roe.Labute.dvd_pow_two_pow_sub_one {ρ : ℤ_[2]} {k : ℕ} (hk : 1 ≤ k) (h : 2 ^ k ∣ ρ - 1) (n : ℕ) : 2 ^ (k + n) ∣ ρ ^ 2 ^ n - 1

Squaring deepens a congruence: ρ ≡ 1 mod 2^k gives ρ^{2^n} ≡ 1 mod 2^{k+n}.

theorem GQ2.Roe.Labute.dvd_or_dvd_mul {ρ μ d : ℤ_[2]} {k : ℕ} (hk : 1 ≤ k) (hρ : 2 ^ k ∣ ρ - 1) (hμ : μ - 1 = 2 ^ k * d) (hd : ¬2 ∣ d) : 2 ^ (k + 1) ∣ ρ - 1 ∨ 2 ^ (k + 1) ∣ ρ * μ - 1

The digit dichotomy: a sharp level-k move fixes the level-k digit of ρ.

theorem GQ2.Roe.Labute.dvd_succ_of_sq {ρ : ℤ_[2]} {k : ℕ} (hk : 2 ≤ k) (hρ : 2 ^ k ∣ ρ - 1) (hsq : 2 ^ (k + 2) ∣ ρ ^ 2 - 1) : 2 ^ (k + 1) ∣ ρ - 1

The automatic digit (memo §1.1): ρ ≡ 1 mod 2^k together with ρ² ≡ 1 mod 2^{k+2} already gives ρ ≡ 1 mod 2^{k+1} (k ≥ 2).

theorem GQ2.Roe.Labute.sharp_move {base c : ℤ_[2]ˣ} {k : ℕ} (hk : 3 ≤ k) (hbase : (PadicInt.toZModPow 3) ↑base = 5) (hc : 2 ^ k ∣ ↑(c * base⁻¹) - 1) : ∃ (d : ℤ_[2]), ↑(c ^ 2 ^ (k - 2)) - 1 = 2 ^ k * d ∧ ¬2 ∣ d

The move digit (memo §1.2): the 2^{k-2}-power of a unit whose target is 5 mod 8 has a sharp level-k digit — the 1 mod 2^k deviation of the actual triple slot only enters at 2^{2k-2}, and 2k − 2 ≥ k + 1 exactly at the calculus threshold k ≥ 3.

The χ-plumbing and the kernel witnesses (SL2 fill helpers)

theorem GQ2.Roe.Labute.dvd_of_chiLevel_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : G →ₜ* ℤ_[2]ˣ) (target : ℤ_[2]ˣ) {n : ℕ} {q : levelQuot G n} {a : G} (haq : (levelMk G n) a = q) (h : (chiLevel χ n) q = (Units.map ↑(PadicInt.toZModPow n)) target) : 2 ^ n ∣ ↑(χ a * target⁻¹) - 1

The χ-clause of the levelwise sets, read as a 2-adic congruence at a chosen lift.

theorem GQ2.Roe.Labute.chiLevel_eq_of_dvd {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : G →ₜ* ℤ_[2]ˣ) (target : ℤ_[2]ˣ) {n : ℕ} {q : levelQuot G n} {a : G} (haq : (levelMk G n) a = q) (h : 2 ^ n ∣ ↑(χ a * target⁻¹) - 1) : (chiLevel χ n) q = (Units.map ↑(PadicInt.toZModPow n)) target

The converse direction: a 2-adic congruence certifies the χ-clause.

theorem GQ2.Roe.Labute.dvd_chi_of_mem_twoCentralSeries {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (χ : G →ₜ* ℤ_[2]ˣ) {k : ℕ} (hk : 2 ≤ k) {r : G} (hr : r ∈ twoCentralSeries G k) : 2 ^ (k + 1) ∣ ↑(χ r) - 1

The χ-depth bound at index k (twoCentralSeries_units_le): a word that dies in Qₖ has χ-value in 1 + 2^{k+1}ℤ₂. This is the mechanism of chiLevel_lambdaImage_pred, re-instantiated one digit deeper than the generic layer bound.

theorem GQ2.Roe.Labute.pow_two_pow_mem_lambdaImage {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m : ℕ} (q : levelQuot G m) (n : ℕ) : q ^ 2 ^ n ∈ lambdaImage G (1 + n) m

The level-quotient form of the previous lemma.

theorem GQ2.Roe.Labute.dbarWordR0_kernel_witness {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (k : ℕ) (hk : 3 ≤ k) (a s y p q : levelQuot G (k + 1)) (hq : q ∈ lambdaImage G (k - 1) (k + 1)) (hp : commP p y = 1) (hqsy : commP q (s * y) = 1) : dbarWordR0 a s y ![1, p * q, q] = 1

The r₀ kernel witnesses (memo §1.2): the s-slot moves by p and the y-slot by q, where p commutes with y and q commutes with s·y. Then d̄ dies: the p-bracket vanishes outright, and the two q-brackets recombine into [q, s·y] = 1 (centrality lets them be collected). Both free digit moves of ker d̄ have this shape — p a power of y, q a power of s·y.

theorem GQ2.Roe.Labute.dbarWordR2_kernel_witness {H : Type u_1} [Group H] (s x y p q : H) (hp : commP p x = 1) (hq : commP q s = 1) : dbarWordR2 s x y ![p, q, 1] = 1

The r₂ kernel witnesses (memo §1.2): the s-slot moves by a power of x and the x-slot by a power of s; each move kills its own bracket definitionally, and the y-slot — the only one entering d̄ through a square — is left alone. No hypotheses at all.

theorem GQ2.Roe.Labute.eq_top_of_map_levelProj_eq_top (G : Type) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (hfg : ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hpro : IsProP 2 G) {k : ℕ} (hk : 2 ≤ k) {H : Subgroup (levelQuot G (k + 1))} (h : Subgroup.map (levelProj G k) H = ⊤) : H = ⊤

Generation lifts along the tower: a subgroup of Q_{k+1} surjecting onto Qₖ is everything — the kernel Zₖ ≤ λ₂ is Frattini (lambdaImage_two_le_frattiniLike), so non-generation applies.