GL-D: the Magnus coefficient algebra (Lazard fragment; insurance lane)

Design record: docs/orchestration/span-gradedlie-plan.md §4. Interface NOT frozen — the GL-D worker has latitude; nothing in the main lane cites this file. Review with the orchestrator before anything else consumes it.

Content (Serre 252 §6, "la méthode de Lazard", at q = p = 2):

• the coefficient ring MagnusA := FreeMonoid (Fin 3) → ℤ_[2] under convolution (finite sums over word splits; no topology needed for the ring operations);
• the mixed filtration magnusFil j = {f | ∀ w, 2^(j − |w|) ∣ f w} (the ideal generated by 2 and the letters, j-th power);
• the congruence unit group MagnusU = 1 + m₀ with the product topology: a profinite pro-2 group carrying the instance pack that freeProTwoLift requires;
• the Magnus morphism magnusHom := freeProTwoLift _ (fun i ↦ 1 + ξᵢ) and the filtration estimate λ_j(MagnusU) ≤ congrSub j, which combined with map_twoCentralSeries_le gives coefficient valuations v₂(coeff_w (μ z)) ≥ j − |w| for z ∈ λ_j(F₃);
• per-(word, level) coordinate functionals Zₖ → 𝔽₂: additive, λ_{k+1}-killing.

Numerically validated end to end (memo §5: span_model.py — filtration, PBW separation rank = N_k, column span, coker(d̄) = 2).

Role: fallback certificate route for the k = 3 base case should GL-C snag, and the ker(ab)-sensitive functional infrastructure the (out-of-scope) SL1 design gap will want later. Do NOT build Lyndon-word combinatorics unless the orchestrator re-scopes.

Design decisions (GL-D, recorded per the dispatch spec)

• Bespoke ring, not MonoidAlgebra. The unit group needs full-support series: (1 + ξ₀)⁻¹ = 1 − ξ₀ + ξ₀² − … has infinite support, so a finitely-supported model (MonoidAlgebra ℤ_[2] (FreeMonoid (Fin 3))) is not closed under the group operation. Mathlib has no non-commutative power-series ring (MvPowerSeries is indexed by σ →₀ ℕ, i.e. commuting variables), so MagnusA is built here from scratch, following the MvPowerSeries boilerplate pattern (def + Pi additive structure + bespoke Mul/One, mul_assoc by Finset.sum_sigma'/Finset.sum_nbij').
• Split indexing by prefix length. A split w = u · v is recorded by the single natural number i = |u| ∈ {0, …, |w|}, so the convolution is a Finset.range sum and no word-antidiagonal Finset (which would need DecidableEq gymnastics through the FreeMonoid type synonym) is required.
• The unit group is 1 + m₀, m₀ = {a | a 1 = 0}, i.e. {f | f 1 = 1}. The dispatch spec's {f // f 1 = 1 ∧ f − 1 ∈ magnusFil 1} has a redundant second clause (f 1 = 1 already forces 2 ∣ (f − 1) 1 = 0, and at |w| ≥ 1 the divisor is 2⁰): see mem_magnusFil_one_iff and sub_one_mem_magnusFil_one. Restricting to constant term exactly 1 (rather than the larger 1 + magnusFil 1 = {f | f 1 ≡ 1 mod 2}, which is also a group) makes the inverse a finite geometric sum with no scalar inversion in ℤ_[2]: a := 1 − f is coefficientwise nilpotent (aⁿ w = 0 for n > |w|, coeff_pow_eq_zero), so f⁻¹ w = ∑_{n ≤ |w|} (aⁿ) w. The Magnus image lands in this smaller group anyway (1 + ξᵢ has constant term 1).
• The digit map avoids division. ℤ_[2] has no total division, so the level-k coordinate of a 2^m-divisible coefficient is defined as digit m x = 0 ↔ 2^{m+1} ∣ x rather than as x / 2^m mod 2; digit_two_pow_mul identifies it with the mod-2 reduction of the cofactor, which is where additivity comes from.

Interface (for orchestrator review; nothing here is frozen)

• ring: MagnusA, coeff, coeff_mul, xi; Ring MagnusA.
• filtration: magnusFil j : AddSubgroup MagnusA, mul_mem_magnusFil (the valuation estimate m^p · m^q ⊆ m^{p+q}), add_self_mem_magnusFil, mul_mem_magnusFil_left/right.
• unit group: MagnusU, Group/IsTopologicalGroup/CompactSpace/T2Space/ TotallyDisconnectedSpace instances, MagnusU.congrSub j : Subgroup MagnusU, MagnusU.sq_mem_congrSub_succ, MagnusU.commutator_mem_congrSub_succ, MagnusU.exists_congrSub_le, MagnusU.isProP_two.
• Magnus expansion: magnusGen, magnusHom, MagnusU.twoCentralSeries_le_congrSub : λⱼ(MagnusU) ≤ congrSub j, and its corollary two_pow_dvd_coeff_magnusHom.
• functionals: digit, digit_add, coord w k, coord_mul, coord_eq_zero_of_mem_succ, coordHom : λₖ(F₃) →* Multiplicative (ZMod 2), and the layer versions zCoord/zCoordHom : Zₖ →* Multiplicative (ZMod 2) (Zₖ = zLayer freeProTwo k).

The file is sorry-free and uses no axioms beyond propext, Classical.choice, Quot.sound.

Words in three letters

Word is the index monoid of the Magnus algebra. It is definitionally List (Fin 3); wlen, wtake, wdrop are List.length, List.take, List.drop transported through the FreeMonoid type synonym (all the lemmas below are the List ones, by rfl).

@[reducible, inline]

abbrev GQ2.Roe.Labute.Magnus.Word : Type

The index monoid of the Magnus algebra: words in the three marked letters.

Equations

• GQ2.Roe.Labute.Magnus.Word = FreeMonoid (Fin 3)

@[implicit_reducible]

instance GQ2.Roe.Labute.Magnus.instDecidableEqWord : DecidableEq Word

Equations

• GQ2.Roe.Labute.Magnus.instDecidableEqWord = GQ2.Roe.Labute.Magnus.instDecidableEqWord._aux_1

def GQ2.Roe.Labute.Magnus.wlen (w : Word) : ℕ

The length |w| of a word.

Equations

• GQ2.Roe.Labute.Magnus.wlen w = (FreeMonoid.toList w).length

def GQ2.Roe.Labute.Magnus.wtake (i : ℕ) (w : Word) : Word

The prefix of w of length i (all of w if i ≥ |w|).

Equations

• GQ2.Roe.Labute.Magnus.wtake i w = FreeMonoid.ofList (List.take i (FreeMonoid.toList w))

def GQ2.Roe.Labute.Magnus.wdrop (i : ℕ) (w : Word) : Word

The suffix of w after its first i letters (empty if i ≥ |w|).

Equations

• GQ2.Roe.Labute.Magnus.wdrop i w = FreeMonoid.ofList (List.drop i (FreeMonoid.toList w))

@[simp]

theorem GQ2.Roe.Labute.Magnus.wlen_one : wlen 1 = 0

@[simp]

theorem GQ2.Roe.Labute.Magnus.wtake_zero (w : Word) : wtake 0 w = 1

@[simp]

theorem GQ2.Roe.Labute.Magnus.wdrop_zero (w : Word) : wdrop 0 w = w

@[simp]

theorem GQ2.Roe.Labute.Magnus.wlen_wtake (i : ℕ) (w : Word) : wlen (wtake i w) = min i (wlen w)

@[simp]

theorem GQ2.Roe.Labute.Magnus.wlen_wdrop (i : ℕ) (w : Word) : wlen (wdrop i w) = wlen w - i

@[simp]

theorem GQ2.Roe.Labute.Magnus.wtake_wlen (w : Word) : wtake (wlen w) w = w

@[simp]

theorem GQ2.Roe.Labute.Magnus.wdrop_wlen (w : Word) : wdrop (wlen w) w = 1

theorem GQ2.Roe.Labute.Magnus.wtake_wtake (i j : ℕ) (w : Word) : wtake i (wtake j w) = wtake (min i j) w

theorem GQ2.Roe.Labute.Magnus.wdrop_wtake (i j : ℕ) (w : Word) : wdrop i (wtake j w) = wtake (j - i) (wdrop i w)

theorem GQ2.Roe.Labute.Magnus.wdrop_wdrop (i j : ℕ) (w : Word) : wdrop i (wdrop j w) = wdrop (j + i) w

theorem GQ2.Roe.Labute.Magnus.wtake_mul_wdrop (i : ℕ) (w : Word) : wtake i w * wdrop i w = w

theorem GQ2.Roe.Labute.Magnus.wlen_eq_zero {w : Word} : wlen w = 0 ↔ w = 1

theorem GQ2.Roe.Labute.Magnus.wtake_ne_one {i : ℕ} {w : Word} (hi : i ≠ 0) (hiw : i ≤ wlen w) : wtake i w ≠ 1

A nonzero-length prefix is a nonempty word.

theorem GQ2.Roe.Labute.Magnus.wdrop_ne_one {i : ℕ} {w : Word} (hi : i < wlen w) : wdrop i w ≠ 1

A proper suffix is a nonempty word.

The coefficient ring MagnusA

def GQ2.Roe.Labute.Magnus.MagnusA : Type

The Magnus coefficient ring ℤ₂⟪ξ₀, ξ₁, ξ₂⟫: all (not necessarily finitely supported) ℤ_[2]-valued functions on words, with the convolution product (f * g) w = ∑_{w = u·v} f u · g v.

Equations

• GQ2.Roe.Labute.Magnus.MagnusA = (GQ2.Roe.Labute.Magnus.Word → ℤ_[2])

def GQ2.Roe.Labute.Magnus.coeff (f : MagnusA) (w : Word) : ℤ_[2]

Coefficient extraction: coeff f w is the coefficient of the word w in f.

Equations

• GQ2.Roe.Labute.Magnus.coeff f w = f w

theorem GQ2.Roe.Labute.Magnus.MagnusA.ext {f g : MagnusA} (h : ∀ (w : Word), coeff f w = coeff g w) : f = g

theorem GQ2.Roe.Labute.Magnus.MagnusA.ext_iff {f g : MagnusA} : f = g ↔ ∀ (w : Word), coeff f w = coeff g w

@[implicit_reducible]

noncomputable instance GQ2.Roe.Labute.Magnus.instAddCommGroupMagnusA : AddCommGroup MagnusA

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GQ2.Roe.Labute.Magnus.coeff_zero (w : Word) : coeff 0 w = 0

@[simp]

theorem GQ2.Roe.Labute.Magnus.coeff_add (f g : MagnusA) (w : Word) : coeff (f + g) w = coeff f w + coeff g w

@[simp]

theorem GQ2.Roe.Labute.Magnus.coeff_neg (f : MagnusA) (w : Word) : coeff (-f) w = -coeff f w

@[simp]

theorem GQ2.Roe.Labute.Magnus.coeff_sub (f g : MagnusA) (w : Word) : coeff (f - g) w = coeff f w - coeff g w

@[implicit_reducible]

noncomputable instance GQ2.Roe.Labute.Magnus.instOneMagnusA : One MagnusA

Equations

• GQ2.Roe.Labute.Magnus.instOneMagnusA = { one := fun (w : GQ2.Roe.Labute.Magnus.Word) => if w = 1 then 1 else 0 }

@[implicit_reducible]

noncomputable instance GQ2.Roe.Labute.Magnus.instMulMagnusA : Mul MagnusA

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.Roe.Labute.Magnus.coeff_one (w : Word) : coeff 1 w = if w = 1 then 1 else 0

@[simp]

theorem GQ2.Roe.Labute.Magnus.coeff_one_self : coeff 1 1 = 1

@[simp]

theorem GQ2.Roe.Labute.Magnus.coeff_one_of_ne {w : Word} (hw : w ≠ 1) : coeff 1 w = 0

theorem GQ2.Roe.Labute.Magnus.coeff_mul (f g : MagnusA) (w : Word) : coeff (f * g) w = ∑ i ∈ Finset.range (wlen w + 1), coeff f (wtake i w) * coeff g (wdrop i w)

Ring axioms

theorem GQ2.Roe.Labute.Magnus.coeff_one_mul (f : MagnusA) (w : Word) : coeff (1 * f) w = coeff f w

theorem GQ2.Roe.Labute.Magnus.coeff_mul_one (f : MagnusA) (w : Word) : coeff (f * 1) w = coeff f w

theorem GQ2.Roe.Labute.Magnus.coeff_zero_mul (f : MagnusA) (w : Word) : coeff (0 * f) w = 0

theorem GQ2.Roe.Labute.Magnus.coeff_mul_zero (f : MagnusA) (w : Word) : coeff (f * 0) w = 0

theorem GQ2.Roe.Labute.Magnus.coeff_add_mul (f g h : MagnusA) (w : Word) : coeff ((f + g) * h) w = coeff (f * h) w + coeff (g * h) w

theorem GQ2.Roe.Labute.Magnus.coeff_mul_add (f g h : MagnusA) (w : Word) : coeff (f * (g + h)) w = coeff (f * g) w + coeff (f * h) w

theorem GQ2.Roe.Labute.Magnus.coeff_mul_mul_left (f g h : MagnusA) (w : Word) : coeff (f * g * h) w = ∑ i ∈ Finset.range (wlen w + 1), ∑ j ∈ Finset.range (i + 1), coeff f (wtake j w) * coeff g (wtake (i - j) (wdrop j w)) * coeff h (wdrop i w)

The triple-convolution normal form of (f * g) * h, indexed by pairs j ≤ i ≤ |w| (the two cut points of the three-fold split w = u·v·x).

theorem GQ2.Roe.Labute.Magnus.coeff_mul_mul_right (f g h : MagnusA) (w : Word) : coeff (f * (g * h)) w = ∑ j ∈ Finset.range (wlen w + 1), ∑ l ∈ Finset.range (wlen w - j + 1), coeff f (wtake j w) * (coeff g (wtake l (wdrop j w)) * coeff h (wdrop (j + l) w))

The triple-convolution normal form of f * (g * h), indexed by pairs j, l with j + l ≤ |w|.

theorem GQ2.Roe.Labute.Magnus.coeff_mul_assoc (f g h : MagnusA) (w : Word) : coeff (f * g * h) w = coeff (f * (g * h)) w

@[implicit_reducible]

noncomputable instance GQ2.Roe.Labute.Magnus.instRingMagnusA : Ring MagnusA

Equations

• One or more equations did not get rendered due to their size.

The letters

noncomputable def GQ2.Roe.Labute.Magnus.xi (i : Fin 3) : MagnusA

The i-th Magnus letter ξᵢ: the indicator function of the one-letter word i.

Equations

• GQ2.Roe.Labute.Magnus.xi i w = if w = FreeMonoid.of i then 1 else 0

theorem GQ2.Roe.Labute.Magnus.coeff_xi (i : Fin 3) (w : Word) : coeff (xi i) w = if w = FreeMonoid.of i then 1 else 0

@[simp]

theorem GQ2.Roe.Labute.Magnus.coeff_xi_self (i : Fin 3) : coeff (xi i) (FreeMonoid.of i) = 1

@[simp]

theorem GQ2.Roe.Labute.Magnus.wlen_of (i : Fin 3) : wlen (FreeMonoid.of i) = 1

@[simp]

theorem GQ2.Roe.Labute.Magnus.coeff_xi_one (i : Fin 3) : coeff (xi i) 1 = 0

The filtration m^j

magnusFil j is the j-th power of the maximal ideal m = (2, ξ₀, ξ₁, ξ₂), described by the valuation bound v₂(f w) ≥ j − |w| (truncated subtraction). Only the two containments actually used downstream are proved: additivity in j under multiplication (mul_mem_magnusFil, the core estimate) and the trivial monotonicity.

noncomputable def GQ2.Roe.Labute.Magnus.magnusFil (j : ℕ) : AddSubgroup MagnusA

The two-sided filtration ideal m^j = {f | ∀ w, 2^(j − |w|) ∣ f w}, as an additive subgroup of MagnusA.

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.Roe.Labute.Magnus.mem_magnusFil {j : ℕ} {f : MagnusA} : f ∈ magnusFil j ↔ ∀ (w : Word), 2 ^ (j - wlen w) ∣ coeff f w

@[simp]

theorem GQ2.Roe.Labute.Magnus.magnusFil_zero : magnusFil 0 = ⊤

theorem GQ2.Roe.Labute.Magnus.magnusFil_antitone {i j : ℕ} (h : i ≤ j) : magnusFil j ≤ magnusFil i

theorem GQ2.Roe.Labute.Magnus.mem_magnusFil_one_iff {f : MagnusA} : f ∈ magnusFil 1 ↔ 2 ∣ coeff f 1

At level 1 the filtration only constrains the constant term: m = {f | 2 ∣ f 1}.

theorem GQ2.Roe.Labute.Magnus.mul_mem_magnusFil {p q : ℕ} {a b : MagnusA} (ha : a ∈ magnusFil p) (hb : b ∈ magnusFil q) : a * b ∈ magnusFil (p + q)

The convolution valuation estimate (the core filtration lemma): m^p · m^q ⊆ m^{p+q}.

theorem GQ2.Roe.Labute.Magnus.add_self_mem_magnusFil {p : ℕ} {a : MagnusA} (ha : a ∈ magnusFil p) : a + a ∈ magnusFil (p + 1)

Doubling deepens the filtration by one (the 2 ∈ m half of the ideal).

theorem GQ2.Roe.Labute.Magnus.xi_mem_magnusFil_one (i : Fin 3) : xi i ∈ magnusFil 1

The letters lie in m.

theorem GQ2.Roe.Labute.Magnus.mul_mem_magnusFil_left {j : ℕ} (a : MagnusA) {b : MagnusA} (hb : b ∈ magnusFil j) : a * b ∈ magnusFil j

magnusFil j is a left ideal.

theorem GQ2.Roe.Labute.Magnus.mul_mem_magnusFil_right {j : ℕ} {a : MagnusA} (ha : a ∈ magnusFil j) (b : MagnusA) : a * b ∈ magnusFil j

magnusFil j is a right ideal.

Coefficientwise nilpotence, and inverses

theorem GQ2.Roe.Labute.Magnus.coeff_sum {ι : Type u_1} (s : Finset ι) (F : ι → MagnusA) (w : Word) : coeff (∑ i ∈ s, F i) w = ∑ i ∈ s, coeff (F i) w

theorem GQ2.Roe.Labute.Magnus.coeff_mul_at_one (f g : MagnusA) : coeff (f * g) 1 = coeff f 1 * coeff g 1

Multiplicativity of the augmentation (constant term).

theorem GQ2.Roe.Labute.Magnus.sub_one_mem_magnusFil_one {f : MagnusA} (hf : coeff f 1 = 1) : f - 1 ∈ magnusFil 1

If f has constant term 1 then f − 1 lies in m (so the dispatch spec's second clause in {f // f 1 = 1 ∧ f − 1 ∈ magnusFil 1} is redundant).

theorem GQ2.Roe.Labute.Magnus.coeff_pow_eq_zero {a : MagnusA} (ha : coeff a 1 = 0) (n : ℕ) (w : Word) : wlen w < n → coeff (a ^ n) w = 0

Coefficientwise nilpotence of the augmentation ideal: if a has zero constant term then aⁿ vanishes on every word shorter than n.

noncomputable def GQ2.Roe.Labute.Magnus.magnusInv (f : MagnusA) : MagnusA

The inverse of a series with constant term 1, as the geometric series in 1 − f (coefficientwise a finite sum, by coeff_pow_eq_zero).

Equations

• GQ2.Roe.Labute.Magnus.magnusInv f w = ∑ n ∈ Finset.range (GQ2.Roe.Labute.Magnus.wlen w + 1), GQ2.Roe.Labute.Magnus.coeff ((1 - f) ^ n) w

theorem GQ2.Roe.Labute.Magnus.coeff_magnusInv (f : MagnusA) (w : Word) : coeff (magnusInv f) w = ∑ n ∈ Finset.range (wlen w + 1), coeff ((1 - f) ^ n) w

@[simp]

theorem GQ2.Roe.Labute.Magnus.coeff_magnusInv_at_one (f : MagnusA) : coeff (magnusInv f) 1 = 1

theorem GQ2.Roe.Labute.Magnus.coeff_magnusInv_eq_partial {f : MagnusA} (hf : coeff f 1 = 1) {N : ℕ} {w : Word} (hw : wlen w ≤ N) : coeff (magnusInv f) w = coeff (∑ n ∈ Finset.range (N + 1), (1 - f) ^ n) w

The geometric series stabilises: magnusInv f agrees with its N-th partial sum at every word of length at most N.

theorem GQ2.Roe.Labute.Magnus.mul_magnusInv {f : MagnusA} (hf : coeff f 1 = 1) : f * magnusInv f = 1

theorem GQ2.Roe.Labute.Magnus.magnusInv_mul {f : MagnusA} (hf : coeff f 1 = 1) : magnusInv f * f = 1

The congruence unit group MagnusU = 1 + m₀

@[reducible, inline]

abbrev GQ2.Roe.Labute.Magnus.MagnusU : Type

The congruence unit group of the Magnus algebra: the series with constant term exactly 1. (The dispatch spec's {f // f 1 = 1 ∧ f − 1 ∈ magnusFil 1} has a redundant second clause — sub_one_mem_magnusFil_one.)

Equations

• GQ2.Roe.Labute.Magnus.MagnusU = { f : GQ2.Roe.Labute.Magnus.MagnusA // GQ2.Roe.Labute.Magnus.coeff f 1 = 1 }

@[simp]

theorem GQ2.Roe.Labute.Magnus.MagnusU.coeff_val_one (u : MagnusU) : coeff (↑u) 1 = 1

@[implicit_reducible]

noncomputable instance GQ2.Roe.Labute.Magnus.MagnusU.instOne : One MagnusU

Equations

• GQ2.Roe.Labute.Magnus.MagnusU.instOne = { one := ⟨1, GQ2.Roe.Labute.Magnus.coeff_one_self⟩ }

@[implicit_reducible]

noncomputable instance GQ2.Roe.Labute.Magnus.MagnusU.instMul : Mul MagnusU

Equations

• GQ2.Roe.Labute.Magnus.MagnusU.instMul = { mul := fun (u v : GQ2.Roe.Labute.Magnus.MagnusU) => ⟨↑u * ↑v, ⋯⟩ }

@[implicit_reducible]

noncomputable instance GQ2.Roe.Labute.Magnus.MagnusU.instInv : Inv MagnusU

Equations

• GQ2.Roe.Labute.Magnus.MagnusU.instInv = { inv := fun (u : GQ2.Roe.Labute.Magnus.MagnusU) => ⟨GQ2.Roe.Labute.Magnus.magnusInv ↑u, ⋯⟩ }

@[simp]

theorem GQ2.Roe.Labute.Magnus.MagnusU.val_one : ↑1 = 1

@[simp]

theorem GQ2.Roe.Labute.Magnus.MagnusU.val_mul (u v : MagnusU) : ↑(u * v) = ↑u * ↑v

@[simp]

theorem GQ2.Roe.Labute.Magnus.MagnusU.val_inv (u : MagnusU) : ↑u⁻¹ = magnusInv ↑u

@[implicit_reducible]

noncomputable instance GQ2.Roe.Labute.Magnus.MagnusU.instGroup : Group MagnusU

Equations

• One or more equations did not get rendered due to their size.

def GQ2.Roe.Labute.Magnus.MagnusU.valHom : MagnusU →* MagnusA

The underlying-series homomorphism MagnusU →* MagnusA.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GQ2.Roe.Labute.Magnus.MagnusU.valHom_apply (u : MagnusU) : valHom u = ↑u

@[simp]

theorem GQ2.Roe.Labute.Magnus.MagnusU.val_pow (u : MagnusU) (n : ℕ) : ↑(u ^ n) = ↑u ^ n

The topology

@[implicit_reducible]

noncomputable instance GQ2.Roe.Labute.Magnus.MagnusU.instTopologicalSpaceMagnusA : TopologicalSpace MagnusA

Equations

• GQ2.Roe.Labute.Magnus.MagnusU.instTopologicalSpaceMagnusA = GQ2.Roe.Labute.Magnus.MagnusU.instTopologicalSpaceMagnusA._aux_1

instance GQ2.Roe.Labute.Magnus.MagnusU.instCompactSpaceMagnusA : CompactSpace MagnusA

instance GQ2.Roe.Labute.Magnus.MagnusU.instT2SpaceMagnusA : T2Space MagnusA

instance GQ2.Roe.Labute.Magnus.MagnusU.instTotallyDisconnectedSpaceMagnusA : TotallyDisconnectedSpace MagnusA

theorem GQ2.Roe.Labute.Magnus.MagnusU.continuous_coeff (w : Word) : Continuous fun (f : MagnusA) => coeff f w

theorem GQ2.Roe.Labute.Magnus.MagnusU.continuous_iff_coeff {X : Type u_1} [TopologicalSpace X] {F : X → MagnusA} : Continuous F ↔ ∀ (w : Word), Continuous fun (x : X) => coeff (F x) w

theorem GQ2.Roe.Labute.Magnus.MagnusU.continuous_coeff_mul {X : Type u_1} [TopologicalSpace X] {F G : X → MagnusA} (hF : ∀ (w : Word), Continuous fun (x : X) => coeff (F x) w) (hG : ∀ (w : Word), Continuous fun (x : X) => coeff (G x) w) (w : Word) : Continuous fun (x : X) => coeff (F x * G x) w

theorem GQ2.Roe.Labute.Magnus.MagnusU.continuous_coeff_pow {X : Type u_1} [TopologicalSpace X] {F : X → MagnusA} (hF : ∀ (w : Word), Continuous fun (x : X) => coeff (F x) w) (n : ℕ) (w : Word) : Continuous fun (x : X) => coeff (F x ^ n) w

theorem GQ2.Roe.Labute.Magnus.MagnusU.continuous_coeff_val (w : Word) : Continuous fun (u : MagnusU) => coeff (↑u) w

instance GQ2.Roe.Labute.Magnus.MagnusU.instContinuousMul : ContinuousMul MagnusU

instance GQ2.Roe.Labute.Magnus.MagnusU.instContinuousInv : ContinuousInv MagnusU

instance GQ2.Roe.Labute.Magnus.MagnusU.instIsTopologicalGroup : IsTopologicalGroup MagnusU

theorem GQ2.Roe.Labute.Magnus.MagnusU.isClosed_magnusU : IsClosed {f : MagnusA | coeff f 1 = 1}

instance GQ2.Roe.Labute.Magnus.MagnusU.instCompactSpace : CompactSpace MagnusU

The congruence filtration

noncomputable def GQ2.Roe.Labute.Magnus.MagnusU.congrSub (j : ℕ) : Subgroup MagnusU

The congruence subgroup 1 + m^j of MagnusU.

Equations

• GQ2.Roe.Labute.Magnus.MagnusU.congrSub j = { carrier := {u : GQ2.Roe.Labute.Magnus.MagnusU | ↑u - 1 ∈ GQ2.Roe.Labute.Magnus.magnusFil j}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem GQ2.Roe.Labute.Magnus.MagnusU.mem_congrSub {j : ℕ} {u : MagnusU} : u ∈ congrSub j ↔ ↑u - 1 ∈ magnusFil j

theorem GQ2.Roe.Labute.Magnus.MagnusU.congrSub_antitone {i j : ℕ} (h : i ≤ j) : congrSub j ≤ congrSub i

@[simp]

theorem GQ2.Roe.Labute.Magnus.MagnusU.congrSub_one : congrSub 1 = ⊤

instance GQ2.Roe.Labute.Magnus.MagnusU.instNormalCongrSub (j : ℕ) : (congrSub j).Normal

theorem GQ2.Roe.Labute.Magnus.MagnusU.sq_mem_congrSub_succ {j : ℕ} (hj : 1 ≤ j) {u : MagnusU} (hu : u ∈ congrSub j) : u ^ 2 ∈ congrSub (j + 1)

The square estimate: squaring deepens the congruence filtration by one.

theorem GQ2.Roe.Labute.Magnus.MagnusU.pow_two_pow_mem_congrSub (u : MagnusU) (i : ℕ) : u ^ 2 ^ i ∈ congrSub (i + 1)

theorem GQ2.Roe.Labute.Magnus.MagnusU.isPGroup_quotient_congrSub (j : ℕ) : IsPGroup 2 (MagnusU ⧸ congrSub j)

Each congruence quotient is a 2-group.

The congruence filtration is a neighbourhood basis of 1

theorem GQ2.Roe.Labute.Magnus.MagnusU.isClosed_setOf_two_pow_dvd (n : ℕ) : IsClosed {x : ℤ_[2] | 2 ^ n ∣ x}

theorem GQ2.Roe.Labute.Magnus.MagnusU.isClosed_congrSub (j : ℕ) : IsClosed ↑(congrSub j)

theorem GQ2.Roe.Labute.Magnus.MagnusU.eq_zero_of_forall_two_pow_dvd {x : ℤ_[2]} (h : ∀ (n : ℕ), 2 ^ n ∣ x) : x = 0

theorem GQ2.Roe.Labute.Magnus.MagnusU.iInter_congrSub : ⋂ (j : ℕ), ↑(congrSub j) = {1}

The congruence filtration separates points.

theorem GQ2.Roe.Labute.Magnus.MagnusU.exists_congrSub_le {V : Subgroup MagnusU} (hV : IsOpen ↑V) : ∃ (j : ℕ), congrSub j ≤ V

Neighbourhood-basis property: every open subgroup of MagnusU contains a congruence subgroup.

theorem GQ2.Roe.Labute.Magnus.MagnusU.isProP_two : IsProP 2 MagnusU

MagnusU is a pro-2 group — the last piece of the instance pack that freeProTwoLift consumes.

@[simp]

theorem GQ2.Roe.Labute.Magnus.MagnusU.congrSub_zero : congrSub 0 = ⊤

theorem GQ2.Roe.Labute.Magnus.MagnusU.commutator_mem_congrSub_succ {j : ℕ} {u : MagnusU} (hu : u ∈ congrSub j) (g : MagnusU) : ⁅u, g⁆ ∈ congrSub (j + 1)

The commutator estimate: ⁅1 + m^j, 1 + m⁆ ⊆ 1 + m^{j+1}. (Ring form: uv − vu = ab − ba ∈ m^{j+1} for a = u − 1 ∈ m^j, b = v − 1 ∈ m, transported to the group commutator by uvu⁻¹v⁻¹ − 1 = (uv − vu)·u⁻¹·v⁻¹.)

theorem GQ2.Roe.Labute.Magnus.MagnusU.twoCentralSeries_le_congrSub (j : ℕ) : twoCentralSeries MagnusU j ≤ congrSub j

The λ-filtration estimate (Serre 252 §6): the lower 2-central series of the congruence unit group is contained in the congruence filtration, λⱼ(1 + m₀) ≤ 1 + m^j.

The Magnus morphism μ : F₃ → 1 + m₀

noncomputable def GQ2.Roe.Labute.Magnus.magnusGen (i : Fin 3) : MagnusU

The Magnus image of the i-th free generator: 1 + ξᵢ.

Equations

• GQ2.Roe.Labute.Magnus.magnusGen i = ⟨1 + GQ2.Roe.Labute.Magnus.xi i, ⋯⟩

@[simp]

theorem GQ2.Roe.Labute.Magnus.val_magnusGen (i : Fin 3) : ↑(magnusGen i) = 1 + xi i

noncomputable def GQ2.Roe.Labute.Magnus.magnusHom : ↑freeProTwo.toProfinite.toTop →ₜ* MagnusU

The Magnus morphism μ : F₃ → 1 + m₀, xᵢ ↦ 1 + ξᵢ (Serre 252 §6, "la méthode de Lazard"; the universal property of freeProTwo applied to the pro-2 group MagnusU).

Equations

• GQ2.Roe.Labute.Magnus.magnusHom = GQ2.Roe.Labute.freeProTwoLift GQ2.Roe.Labute.Magnus.MagnusU.isProP_two GQ2.Roe.Labute.Magnus.magnusGen

@[simp]

theorem GQ2.Roe.Labute.Magnus.magnusHom_freeGen (i : Fin 3) : magnusHom (freeGen i) = magnusGen i

theorem GQ2.Roe.Labute.Magnus.two_pow_dvd_coeff_magnusHom {j : ℕ} {z : ↑freeProTwo.toProfinite.toTop} (hz : z ∈ twoCentralSeries (↑freeProTwo.toProfinite.toTop) j) (w : Word) : 2 ^ (j - wlen w) ∣ coeff (↑(magnusHom z) - 1) w

Filtration compatibility of the Magnus expansion (memo §5, machine-validated): for z ∈ λⱼ(F₃) every coefficient of μ z − 1 at a word w is divisible by 2^{j − |w|}.

theorem GQ2.Roe.Labute.Magnus.two_pow_dvd_coeff_magnusHom_of_ne_one {j : ℕ} {z : ↑freeProTwo.toProfinite.toTop} (hz : z ∈ twoCentralSeries (↑freeProTwo.toProfinite.toTop) j) {w : Word} (hw : w ≠ 1) : 2 ^ (j - wlen w) ∣ coeff (↑(magnusHom z)) w

The same estimate for the raw coefficient at a nonempty word (where μ z and μ z − 1 agree).

Coordinate functionals

For a word w and a level k ≥ |w|, the 2^{k−|w|}-digit of the w-th Magnus coefficient is a homomorphism λₖ(F₃) → 𝔽₂ killing λ_{k+1}, hence a functional on the graded layer Zₖ = λₖ/λ_{k+1}. No division in ℤ_[2] is needed: for x divisible by 2^m, the m-th digit is 0 exactly when 2^{m+1} ∣ x.

theorem GQ2.Roe.Labute.Magnus.two_ne_zero_padic : 2 ≠ 0

theorem GQ2.Roe.Labute.Magnus.two_dvd_iff_toZModPow {x : ℤ_[2]} : 2 ∣ x ↔ (PadicInt.toZModPow 1) x = 0

theorem GQ2.Roe.Labute.Magnus.two_pow_succ_dvd_mul_iff (m : ℕ) (a : ℤ_[2]) : 2 ^ (m + 1) ∣ 2 ^ m * a ↔ 2 ∣ a

2^{m+1} ∣ 2^m · a exactly when a is even.

noncomputable def GQ2.Roe.Labute.Magnus.digit (m : ℕ) (x : ℤ_[2]) : ZMod 2

The m-th binary digit of a 2-adic integer divisible by 2^m (junk value 1 if the divisibility fails to be one step deeper).

Equations

• GQ2.Roe.Labute.Magnus.digit m x = if 2 ^ (m + 1) ∣ x then 0 else 1

theorem GQ2.Roe.Labute.Magnus.digit_eq_zero_iff (m : ℕ) (x : ℤ_[2]) : digit m x = 0 ↔ 2 ^ (m + 1) ∣ x

theorem GQ2.Roe.Labute.Magnus.digit_eq_zero_of_dvd {m : ℕ} {x : ℤ_[2]} (h : 2 ^ (m + 1) ∣ x) : digit m x = 0

@[simp]

theorem GQ2.Roe.Labute.Magnus.digit_zero (m : ℕ) : digit m 0 = 0

theorem GQ2.Roe.Labute.Magnus.digit_eq_zero_or_one (m : ℕ) (x : ℤ_[2]) : digit m x = 0 ∨ digit m x = 1

theorem GQ2.Roe.Labute.Magnus.digit_two_pow_mul (m : ℕ) (c : ℤ_[2]) : digit m (2 ^ m * c) = (PadicInt.toZModPow 1) c

On the subgroup 2^m ℤ₂ the m-th digit is the mod-2 reduction of the cofactor.

theorem GQ2.Roe.Labute.Magnus.digit_add {m : ℕ} {x y : ℤ_[2]} (hx : 2 ^ m ∣ x) (hy : 2 ^ m ∣ y) : digit m (x + y) = digit m x + digit m y

Additivity of the digit on the subgroup 2^m ℤ₂.

noncomputable def GQ2.Roe.Labute.Magnus.coord (w : Word) (k : ℕ) (z : ↑freeProTwo.toProfinite.toTop) : ZMod 2

The (w, k) Magnus coordinate functional: the 2^{k−|w|}-digit of the w-th coefficient of μ z − 1. A homomorphism on λₖ(F₃) (coord_mul) killing λ_{k+1} (coord_eq_zero_of_mem_succ), i.e. a functional on Zₖ.

Equations

• GQ2.Roe.Labute.Magnus.coord w k z = GQ2.Roe.Labute.Magnus.digit (k - GQ2.Roe.Labute.Magnus.wlen w) (GQ2.Roe.Labute.Magnus.coeff (↑(GQ2.Roe.Labute.Magnus.magnusHom z) - 1) w)

@[simp]

theorem GQ2.Roe.Labute.Magnus.coord_one (w : Word) (k : ℕ) : coord w k 1 = 0

theorem GQ2.Roe.Labute.Magnus.coord_mul {w : Word} {k : ℕ} (hw : wlen w ≤ k) (hk : 1 ≤ k) {y z : ↑freeProTwo.toProfinite.toTop} (hy : y ∈ twoCentralSeries (↑freeProTwo.toProfinite.toTop) k) (hz : z ∈ twoCentralSeries (↑freeProTwo.toProfinite.toTop) k) : coord w k (y * z) = coord w k y + coord w k z

The coordinate functionals are additive on λₖ: the cross term A·B of μ(yz) − 1 = A + B + A·B lands in m^{2k} ⊆ m^{k+1}, one digit deeper.

theorem GQ2.Roe.Labute.Magnus.coord_eq_zero_of_mem_succ {w : Word} {k : ℕ} (hw : wlen w ≤ k) {z : ↑freeProTwo.toProfinite.toTop} (hz : z ∈ twoCentralSeries (↑freeProTwo.toProfinite.toTop) (k + 1)) : coord w k z = 0

The coordinate functionals kill the next layer.

noncomputable def GQ2.Roe.Labute.Magnus.coordHom (w : Word) (k : ℕ) (hw : wlen w ≤ k) (hk : 1 ≤ k) : ↥(twoCentralSeries (↑freeProTwo.toProfinite.toTop) k) →* Multiplicative (ZMod 2)

The (w, k) coordinate functional packaged as a homomorphism λₖ(F₃) → 𝔽₂ (multiplicatively: into Multiplicative (ZMod 2)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GQ2.Roe.Labute.Magnus.coordHom_apply (w : Word) (k : ℕ) (hw : wlen w ≤ k) (hk : 1 ≤ k) (z : ↥(twoCentralSeries (↑freeProTwo.toProfinite.toTop) k)) : (coordHom w k hw hk) z = Multiplicative.ofAdd (coord w k ↑z)

theorem GQ2.Roe.Labute.Magnus.coord_eq_of_levelMk_eq {w : Word} {k : ℕ} (hw : wlen w ≤ k) (hk : 1 ≤ k) {y z : ↑freeProTwo.toProfinite.toTop} (hz : z ∈ twoCentralSeries (↑freeProTwo.toProfinite.toTop) k) (h : (levelMk (↑freeProTwo.toProfinite.toTop) (k + 1)) y = (levelMk (↑freeProTwo.toProfinite.toTop) (k + 1)) z) : coord w k y = coord w k z

The coordinate functionals only depend on the class in Q_{k+1}, so they are genuinely functionals on the graded layer Zₖ = λₖ/λ_{k+1} ≤ Q_{k+1}.

The functionals on the graded layer Zₖ

The repo encodes Zₖ = λₖ/λ_{k+1} as the subgroup zLayer freeProTwo k ≤ Q_{k+1}, so a functional there is obtained from coord by choosing a λₖ-representative; the choice is immaterial by coord_eq_of_levelMk_eq.

theorem GQ2.Roe.Labute.Magnus.exists_rep_of_mem_zLayer {k : ℕ} (q : ↥(zLayer (↑freeProTwo.toProfinite.toTop) k)) : ∃ v ∈ twoCentralSeries (↑freeProTwo.toProfinite.toTop) k, (levelMk (↑freeProTwo.toProfinite.toTop) (k + 1)) v = ↑q

Every class in Zₖ has a λₖ-representative (unfolding of lambdaImage).

noncomputable def GQ2.Roe.Labute.Magnus.zCoord (w : Word) (k : ℕ) (q : ↥(zLayer (↑freeProTwo.toProfinite.toTop) k)) : ZMod 2

The (w, k) coordinate functional on the graded layer Zₖ ≤ Q_{k+1}.

Equations

• GQ2.Roe.Labute.Magnus.zCoord w k q = GQ2.Roe.Labute.Magnus.coord w k ⋯.choose

theorem GQ2.Roe.Labute.Magnus.zCoord_eq {w : Word} {k : ℕ} (hw : wlen w ≤ k) (hk : 1 ≤ k) {q : ↥(zLayer (↑freeProTwo.toProfinite.toTop) k)} {v : ↑freeProTwo.toProfinite.toTop} (hv : v ∈ twoCentralSeries (↑freeProTwo.toProfinite.toTop) k) (hvq : (levelMk (↑freeProTwo.toProfinite.toTop) (k + 1)) v = ↑q) : zCoord w k q = coord w k v

Evaluation of the layer functional on any representative.

noncomputable def GQ2.Roe.Labute.Magnus.zCoordHom (w : Word) (k : ℕ) (hw : wlen w ≤ k) (hk : 1 ≤ k) : ↥(zLayer (↑freeProTwo.toProfinite.toTop) k) →* Multiplicative (ZMod 2)

The (w, k) coordinate functional packaged as a homomorphism Zₖ → 𝔽₂.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GQ2.Roe.Labute.Magnus.zCoordHom_apply (w : Word) (k : ℕ) (hw : wlen w ≤ k) (hk : 1 ≤ k) (q : ↥(zLayer (↑freeProTwo.toProfinite.toTop) k)) : (zCoordHom w k hw hk) q = Multiplicative.ofAdd (zCoord w k q)