Levelwise triple sets, the invariant P, the defect, and the k₀ = 3 base cases

(L-campaign ticket L1/L3)

Statements final (ticket L1); fills tickets L3 (base cases, witnesses, numeric pins, χ-evaluations) and L4a (defect calculus: lift-independence, membership, restriction). Design record: docs/orchestration/labute-l1-design.md; sources: labute-plan.md §2.1–2.3 and labute-spike.md §2.4 (the STATEMENT FREEZE for the sets), §3.1, §3.4, §4.

Fix the two presented pro-2 groups D_R = ⟨s,x,y | r₂⟩ (GQ2/Roe/DRPresentation.lean) and D₀ = ⟨A,S,Y | r₀⟩ (GQ2/DyadicPresentation.lean), their λ-towers (GQ2/Roe/Labute/TwoCentralTower.lean), and the χ-data:

• direction 1 (r₀-triples in the D_R-tower): triples T : Fin 3 → Qₖ(D_R) in the (A, S, Y)-slots; character χ_R = chiR (GQ2/Roe/ChiR.lean); χ-targets (−1, 1, η) with η = (1−4)⁻¹ = (−3)⁻¹ (etaUnit);
• direction 2 (r₂-triples in the D₀-tower): triples in the (s, x, y)-slots; character χ₀ = chiD0pres — built here from the presentation via d0LiftHom at (−1, 1, η), not the B3c-bundle character (GQ2/Roe/MarkedMatching.lean's chiD0G is Galois-side and census-forbidden in this lane, plan §8); χ-targets (S, X, Y) = (SvalUnit, rootXUnit, YvalUnit) (GQ2/Roe/ChiR.lean, tickets R10/R11).

The levelwise sets (spike §2.4, FINAL FORM): S⁰ₖ (sZeroR0/sZeroR2): relator-killing generating triples mod λₖ; S^P_ₖ (sPR0/sPR2): the S⁰ₖ-triples satisfying the invariant P — the χ-congruence χ̄ₖ(Tᵢ) = targetᵢ mod 2^k (modulus m(k) = k, via chiLevel).

The defect δ(T) ∈ Zₖ ⊆ Q_{k+1} (plan §2.2, spike §2.1): the relator value of the canonical lift; independent of the lift (defectR0_eq_of_lift — no k-threshold: only centrality and exponent-2 of the kernel are used, relator exponent sums even both sides).

Base cases k₀ = 3 (spike §2.4, §3.1, §3.4): explicit witnesses in Q₃ (order 2^8 = 256), stated on named generator words so L3 can discharge by transport to a concrete 256-element model + decide/structured verification (plan §2.3); the mod-8 and mod-2^9 numeric pins of the χ-targets are frozen as separate statements (spike §4.1).

Convention note: all word shapes are repo-convention (commP/conjP, board §10); see the convention paragraph in TwoCentralTower.lean.

The r₀ word shape

drWord exists in-tree (GQ2/Roe/DRPresentation.lean); its r₀-mirror is defined here in the same style. d0Word (m 0) (m 1) (m 2) is definitionally the relator expression of d0LiftHom (GQ2/SectionThree.lean:444), so triples killing d0Word classify continuous homs D₀ → H with no rewriting.

def GQ2.Roe.Labute.d0Word {G : Type u_1} [Group G] (a s y : G) : G

The dyadic relator word shape d0Word a s y = a² · s⁴ · [s, y] (r₀ = A²S⁴[S,Y], Serre 252 Cor. 4.4; repo convention [s,y] = commP s y = s⁻¹y⁻¹sy), as a word in any group — the r₀-mirror of GQ2.drWord.

Equations

• GQ2.Roe.Labute.d0Word a s y = a ^ 2 * s ^ 4 * GQ2.commP s y

theorem GQ2.Roe.Labute.map_d0Word {F : Type u_1} {G : Type u_2} {H : Type u_3} [Group G] [Group H] [FunLike F G H] [MonoidHomClass F G H] (φ : F) (a s y : G) : φ (d0Word a s y) = d0Word (φ a) (φ s) (φ y)

Naturality of the r₀ word shape under any monoid-hom-like map (mirror of map_drWord).

theorem GQ2.Roe.Labute.d0Word_comm {G : Type u_1} [CommGroup G] (a s y : G) : d0Word a s y = a ^ 2 * s ^ 4

Abelian collapse (smoke): in a commutative group d0Word a s y = a²s⁴ — the abelianized relation 2ā + 4s̄ = 0, pinning the exponents (2, 4, 0).

theorem GQ2.Roe.Labute.d0Word_eq_one : d0Word d0A d0S d0Y = 1

The relator dies on the marked generators of D₀ (smoke; definitional repackaging of d0_relation).

The χ-data: η, the presentation-side χ₀, and the pinned targets

noncomputable def GQ2.Roe.Labute.negThreeUnit : ℤ_[2]ˣ

The 2-adic unit −3 (odd, hence a unit; same recipe as GQ2.unitNegThree, replicated here to keep this lane free of the Galois-side files — plan §8).

Equations

• GQ2.Roe.Labute.negThreeUnit = GQ2.Roe.Labute.negThreeUnit._proof_1.unit

@[simp]

theorem GQ2.Roe.Labute.negThreeUnit_val : ↑negThreeUnit = -3

Value pin for negThreeUnit (smoke).

noncomputable def GQ2.Roe.Labute.etaUnit : ℤ_[2]ˣ

The secondary-depth unit η = (1 − 4)⁻¹ = (−3)⁻¹ (Labute Théorème 4 case (2) at f = 2: orientation values (−1, 1, (1−2^f)⁻¹); spike §2.4). η ≡ 5 (mod 8) — the f = 2 discriminator (η′ = (1−8)⁻¹ ≡ 1 (mod 8) for the f = 3 control, spike §3.2) — is pinned through chiTargetR0_three below.

Equations

• GQ2.Roe.Labute.etaUnit = GQ2.Roe.Labute.negThreeUnit⁻¹

noncomputable def GQ2.Roe.Labute.chiD0pres : ↑D0.toProfinite.toTop →ₜ* ℤ_[2]ˣ

The presentation-side canonical orientation of D₀: χ₀ : D₀ → ℤ₂ˣ with generator values (A, S, Y) ↦ (−1, 1, η), built by the universal property d0LiftHom at the triple (−1, 1, η) (the relator dies since ℤ₂ˣ is abelian: (−1)²·1⁴·[1,η] = 1).

This is the χ₀ of the levelwise χ-clause in direction 2. It deliberately does not reuse chiD0G (GQ2/Roe/MarkedMatching.lean), which is assembled from the B3c Galois bundle: the L-campaign must stay census-free (plan §8), so every D₀-side fact comes from the presentation.

Equations

• GQ2.Roe.Labute.chiD0pres = GQ2.SectionThree.d0LiftHom GQ2.isProP_two_unitsPadicInt ![-1, 1, GQ2.Roe.Labute.etaUnit] GQ2.Roe.Labute.chiD0pres._proof_5

theorem GQ2.Roe.Labute.chiD0pres_d0A : chiD0pres d0A = -1

χ₀(A) = −1. Fill: L3 (replicate the SectionThree.d0LiftHom_A evaluation pattern of GQ2/SectionThree.lean).

theorem GQ2.Roe.Labute.chiD0pres_d0S : chiD0pres d0S = 1

χ₀(S) = 1. Fill: L3.

theorem GQ2.Roe.Labute.chiD0pres_d0Y : chiD0pres d0Y = etaUnit

χ₀(Y) = η. Fill: L3.

noncomputable def GQ2.Roe.Labute.chiTargetUnitsR0 : Fin 3 → ℤ_[2]ˣ

χ-targets, direction 1 (r₀-triples in the D_R-tower, (A,S,Y)-slots): (−1, 1, η) (spike §2.4).

Equations

• GQ2.Roe.Labute.chiTargetUnitsR0 = ![-1, 1, GQ2.Roe.Labute.etaUnit]

noncomputable def GQ2.Roe.Labute.chiTargetUnitsR2 : Fin 3 → ℤ_[2]ˣ

χ-targets, direction 2 (r₂-triples in the D₀-tower, (s,x,y)-slots): (S, X, Y) — the Hensel-root orientation values of χ_R (spike §2.4; X ≡ 5 (mod 16), S = −X³/(X²+X+1), Y = −X²; GQ2/Roe/OrientationRoot.lean, GQ2/Roe/ChiR.lean).

Equations

• GQ2.Roe.Labute.chiTargetUnitsR2 = ![GQ2.Roe.SvalUnit, GQ2.Roe.rootXUnit, GQ2.Roe.YvalUnit]

noncomputable def GQ2.Roe.Labute.chiTargetR0 (k : ℕ) : Fin 3 → (ZMod (2 ^ k))ˣ

The mod-2^k reductions of the direction-1 targets — the right-hand sides of the invariant P at level k.

Equations

• GQ2.Roe.Labute.chiTargetR0 k i = (Units.map ↑(PadicInt.toZModPow k)) (GQ2.Roe.Labute.chiTargetUnitsR0 i)

noncomputable def GQ2.Roe.Labute.chiTargetR2 (k : ℕ) : Fin 3 → (ZMod (2 ^ k))ˣ

The mod-2^k reductions of the direction-2 targets.

Equations

• GQ2.Roe.Labute.chiTargetR2 k i = (Units.map ↑(PadicInt.toZModPow k)) (GQ2.Roe.Labute.chiTargetUnitsR2 i)

Numeric pins (spike §4.1: anchors to bake into statements)

Mod 8 (level k₀ = 3, load-bearing for L3's base-case checks) and mod 2^9 (stress). Independently re-verified during L1: X ≡ 437, S ≡ 253, Y ≡ 7, η ≡ 341 (mod 512); mod 8 these are (5, 5, 7) and η ≡ 5 — the f = 2 content.

theorem GQ2.Roe.Labute.chiTargetR0_three (i : Fin 3) : ↑(chiTargetR0 3 i) = ![7, 1, 5] i

Direction-1 targets mod 8: (−1, 1, η) ≡ (7, 1, 5). Fill: L3.

theorem GQ2.Roe.Labute.chiTargetR2_three (i : Fin 3) : ↑(chiTargetR2 3 i) = ![5, 5, 7] i

Direction-2 targets mod 8: (S, X, Y) ≡ (5, 5, 7). Fill: L3.

theorem GQ2.Roe.Labute.chiTargetR0_nine (i : Fin 3) : ↑(chiTargetR0 9 i) = ![511, 1, 341] i

Direction-1 targets mod 2^9 (stress): (−1, 1, η) ≡ (511, 1, 341). Fill: L3.

The decides below are kernel checks over the 512 residues (plan §2.3's budget question: they pass comfortably; native_decide is not used anywhere in this file). Only the elaborator's recursion budget needs raising.

theorem GQ2.Roe.Labute.chiTargetR2_nine (i : Fin 3) : ↑(chiTargetR2 9 i) = ![253, 437, 7] i

Direction-2 targets mod 2^9 (stress): (S, X, Y) ≡ (253, 437, 7) — the spike's level-9 numerics, re-verified by hand during L1. Fill: L3.

theorem GQ2.Roe.Labute.chiTargetR0_castHom (k : ℕ) (i : Fin 3) : (Units.map ↑(ZMod.castHom ⋯ (ZMod (2 ^ k)))) (chiTargetR0 (k + 1) i) = chiTargetR0 k i

Naturality of the direction-1 targets in k (consumed by the restriction maps). Fill: L3 (from PadicInt.zmod_cast_comp_toZModPow-style compatibility).

theorem GQ2.Roe.Labute.chiTargetR2_castHom (k : ℕ) (i : Fin 3) : (Units.map ↑(ZMod.castHom ⋯ (ZMod (2 ^ k)))) (chiTargetR2 (k + 1) i) = chiTargetR2 k i

Naturality of the direction-2 targets in k. Fill: L3.

The levelwise sets (spike §2.4, FINAL FORM)

def GQ2.Roe.Labute.sZeroR0 (k : ℕ) : Set (Fin 3 → levelQuot (↑DR.toProfinite.toTop) k)

S⁰ₖ, direction 1: r₀-relator-killing generating triples in Qₖ(D_R) = D_R/λₖ — the strict levelwise set without the χ-clause (plan §2.1; generation is a clause, not an afterthought — spike §3.5).

Equations

• GQ2.Roe.Labute.sZeroR0 k = {T : Fin 3 → GQ2.Roe.Labute.levelQuot (↑GQ2.DR.toProfinite.toTop) k | GQ2.Roe.Labute.d0Word (T 0) (T 1) (T 2) = 1 ∧ Subgroup.closure (Set.range T) = ⊤}

def GQ2.Roe.Labute.sPR0 (k : ℕ) : Set (Fin 3 → levelQuot (↑DR.toProfinite.toTop) k)

S^P_ₖ, direction 1 (spike §2.4, the frozen main object): the S⁰ₖ-triples satisfying the invariant P — the χ-congruence χ̄_R,ₖ(Tᵢ) = targetᵢ at modulus 2^k = 2^{m(k)}.

Equations

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

def GQ2.Roe.Labute.sZeroR2 (k : ℕ) : Set (Fin 3 → levelQuot (↑D0.toProfinite.toTop) k)

S⁰ₖ, direction 2: r₂-relator-killing generating triples in Qₖ(D₀) (word shape drWord, GQ2/Roe/DRPresentation.lean).

Equations

• GQ2.Roe.Labute.sZeroR2 k = {T : Fin 3 → GQ2.Roe.Labute.levelQuot (↑GQ2.D0.toProfinite.toTop) k | GQ2.drWord (T 0) (T 1) (T 2) = 1 ∧ Subgroup.closure (Set.range T) = ⊤}

def GQ2.Roe.Labute.sPR2 (k : ℕ) : Set (Fin 3 → levelQuot (↑D0.toProfinite.toTop) k)

S^P_ₖ, direction 2: the χ-clause runs through the presentation-side χ₀ (chiD0pres) against the Hensel-root targets.

Equations

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

Central-shift calculus (the mechanism behind lift-independence)

Two lifts of the same level-k triple differ coordinatewise by elements of Zₖ, which is central of exponent 2 in Q_{k+1}. Shifting a slot by a central z therefore multiplies the relator value by z to the slot's exponent sum; both relator words have even exponent sums (r₀ = A²S⁴[S,Y]: (2, 4, 0); r₂: (0, −4, 2)), so every shift cancels. The generic commP/conjP steps live in H; the layer facts specialize them.

theorem GQ2.Roe.Labute.commP_central_left {H : Type u_1} [Group H] {z : H} (hz : ∀ (w : H), Commute z w) (a b : H) : commP (z * a) b = commP a b

A central factor in the first slot of a commP cancels.

theorem GQ2.Roe.Labute.commP_central_right {H : Type u_1} [Group H] {z : H} (hz : ∀ (w : H), Commute z w) (a b : H) : commP a (z * b) = commP a b

A central factor in the second slot of a commP cancels.

theorem GQ2.Roe.Labute.conjP_central_left {H : Type u_1} [Group H] {z : H} (hz : ∀ (w : H), Commute z w) (a b : H) : conjP (z * a) b = z * conjP a b

A central factor in the conjugated slot passes through the conjugation.

theorem GQ2.Roe.Labute.conjP_central_right {H : Type u_1} [Group H] {z : H} (hz : ∀ (w : H), Commute z w) (a b : H) : conjP a (z * b) = conjP a b

A central factor in the conjugator cancels.

theorem GQ2.Roe.Labute.inv_mul_inv_central {H : Type u_1} [Group H] {z : H} (hz : ∀ (w : H), Commute z w) (hz2 : z * z = 1) (u v : H) : (z * u)⁻¹ * (z * v)⁻¹ = u⁻¹ * v⁻¹

Two central involutive factors cancel across a product of inverses (the r₂ shape (conjP x s)⁻¹ · (x³)⁻¹, where both slots carry the same shift).

theorem GQ2.Roe.Labute.zLayer_commute {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {z : levelQuot G (k + 1)} (hz : z ∈ zLayer G k) (w : levelQuot G (k + 1)) : Commute z w

Zₖ-elements commute with everything in Q_{k+1} (zLayer_le_center).

theorem GQ2.Roe.Labute.zLayer_inv_self {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {z : levelQuot G (k + 1)} (hz : z ∈ zLayer G k) : z⁻¹ = z

Zₖ has exponent 2, so its elements are their own inverses.

theorem GQ2.Roe.Labute.exists_zLayer_mul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {x y : levelQuot G (k + 1)} (h : (levelProj G k) x = (levelProj G k) y) : ∃ z ∈ zLayer G k, x = z * y

Two lifts of the same level-k class differ by a left Zₖ-factor.

theorem GQ2.Roe.Labute.closure_range_levelProj {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {ι : Type u_2} {T : ι → levelQuot G (k + 1)} (hgen : Subgroup.closure (Set.range T) = ⊤) : Subgroup.closure (Set.range fun (i : ι) => (levelProj G k) (T i)) = ⊤

Generation is inherited along the tower: levelProj is surjective, so it carries a generating family of Q_{k+1} to a generating family of Qₖ.

theorem GQ2.Roe.Labute.d0Word_zLayer_shift {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {z₀ z₁ z₂ : levelQuot G (k + 1)} (h₀ : z₀ ∈ zLayer G k) (h₁ : z₁ ∈ zLayer G k) (h₂ : z₂ ∈ zLayer G k) (a s y : levelQuot G (k + 1)) : d0Word (z₀ * a) (z₁ * s) (z₂ * y) = d0Word a s y

r₀ is insensitive to Zₖ-shifts: exponent sums (2, 4, 0) are even and the commutator absorbs central factors in both slots.

theorem GQ2.Roe.Labute.drWord_zLayer_shift {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {z₀ z₁ z₂ : levelQuot G (k + 1)} (h₀ : z₀ ∈ zLayer G k) (h₁ : z₁ ∈ zLayer G k) (h₂ : z₂ ∈ zLayer G k) (s x y : levelQuot G (k + 1)) : drWord (z₀ * s) (z₁ * x) (z₂ * y) = drWord s x y

r₂ is insensitive to Zₖ-shifts: exponent sums (0, −4, 2) are even; the x-slot shift survives conjugation and cubing but appears twice, and the s- and y-slot shifts are absorbed by the conjugation and the commutator.

The defect (plan §2.2; spike §2.1)

noncomputable def GQ2.Roe.Labute.defectR0 (k : ℕ) (T : Fin 3 → levelQuot (↑DR.toProfinite.toTop) k) : levelQuot (↑DR.toProfinite.toTop) (k + 1)

The defect δ(T) ∈ Q_{k+1}(D_R), direction 1: the r₀-relator value of the canonical lift of T. For T ∈ S⁰ₖ it lands in Zₖ (defectR0_mem_zLayer) and is independent of the choice of lift (defectR0_eq_of_lift) — the q = 2 pathology makes it a genuinely second-order obstruction (plan §2.2).

Equations

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

theorem GQ2.Roe.Labute.defectR0_eq_of_lift (k : ℕ) (T : Fin 3 → levelQuot (↑DR.toProfinite.toTop) k) (T' : Fin 3 → levelQuot (↑DR.toProfinite.toTop) (k + 1)) (hT' : ∀ (i : Fin 3), (levelProj (↑DR.toProfinite.toTop) k) (T' i) = T i) : d0Word (T' 0) (T' 1) (T' 2) = defectR0 k T

Lift-independence of the defect, direction 1 (plan §2.2: all relator exponent sums are even and commutators absorb central factors; no relator-kill hypothesis and no k-threshold is needed). Any coordinatewise lift computes δ(T). Fill: L4a.

theorem GQ2.Roe.Labute.defectR0_mem_zLayer (k : ℕ) {T : Fin 3 → levelQuot (↑DR.toProfinite.toTop) k} (hrel : d0Word (T 0) (T 1) (T 2) = 1) : defectR0 k T ∈ zLayer (↑DR.toProfinite.toTop) k

The defect of a relator-killing triple lies in the graded layer Zₖ (minimal hypothesis: only the relator clause of S⁰ₖ is consumed). Fill: L4a.

noncomputable def GQ2.Roe.Labute.defectR2 (k : ℕ) (T : Fin 3 → levelQuot (↑D0.toProfinite.toTop) k) : levelQuot (↑D0.toProfinite.toTop) (k + 1)

The defect, direction 2 (r₂-relator value of the canonical lift in the D₀-tower).

Equations

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

theorem GQ2.Roe.Labute.defectR2_eq_of_lift (k : ℕ) (T : Fin 3 → levelQuot (↑D0.toProfinite.toTop) k) (T' : Fin 3 → levelQuot (↑D0.toProfinite.toTop) (k + 1)) (hT' : ∀ (i : Fin 3), (levelProj (↑D0.toProfinite.toTop) k) (T' i) = T i) : drWord (T' 0) (T' 1) (T' 2) = defectR2 k T

Lift-independence of the defect, direction 2 (r₂ exponent sums (0, −4, 2) are even; same central-kernel calculus). Fill: L4a.

theorem GQ2.Roe.Labute.defectR2_mem_zLayer (k : ℕ) {T : Fin 3 → levelQuot (↑D0.toProfinite.toTop) k} (hrel : drWord (T 0) (T 1) (T 2) = 1) : defectR2 k T ∈ zLayer (↑D0.toProfinite.toTop) k

The direction-2 defect of a relator-killing triple lies in Zₖ. Fill: L4a.

Restriction maps (plan §2.1 item 2: all three clauses weaken)

theorem GQ2.Roe.Labute.sPR0_levelProj {k : ℕ} {T : Fin 3 → levelQuot (↑DR.toProfinite.toTop) (k + 1)} (hT : T ∈ sPR0 (k + 1)) : (fun (i : Fin 3) => (levelProj (↑DR.toProfinite.toTop) k) (T i)) ∈ sPR0 k

Restriction S^P_{k+1} → S^P_ₖ, direction 1: projecting a level-(k+1) triple along the tower lands in the level-k set (relator: hom-push; generation: surjectivity of levelProj; χ-clause: chiLevel_levelProj + chiTargetR0_castHom). Fill: L4a.

theorem GQ2.Roe.Labute.sPR2_levelProj {k : ℕ} {T : Fin 3 → levelQuot (↑D0.toProfinite.toTop) (k + 1)} (hT : T ∈ sPR2 (k + 1)) : (fun (i : Fin 3) => (levelProj (↑D0.toProfinite.toTop) k) (T i)) ∈ sPR2 k

Restriction S^P_{k+1} → S^P_ₖ, direction 2. Fill: L4a.

Base-case calculus (level-2 λ-calculus in Q₃, and generation transfer)

The base-case memberships are discharged structurally — plan §2.3's sanctioned route ("the witness's relator value traced through the λ-quotient presentation"), not by enumerating a 256-element model, and with no native_decide. Everything reduces to inputs frozen upstream:

• Z₂ = λ₂/λ₃ is central in Q₃ (zLayer_le_center) and has exponent 2 (zLayer_sq);
• squares and commP-commutators of G land in Z₂ (sq_mem_twoCentralSucc, commP_mem_twoCentralSucc, both proven in TwoCentralTower.lean);
• λₖ is open (isOpen_twoCentralSeries), which converts the presentations' topological generation into the plain-closure clause of S⁰ₖ.

Consequently the relator clause is exactly the spike's §2.2 first-order bookkeeping: fourth powers die, the S⁴/[y,yˢ] blocks are inert, and the surviving cross term is pinned against the source relator one layer down.

Class-2 calculus in Q₃

Every commP and every square of Q₃ lands in the central exponent-2 layer Z₂, so Q₃ has class ≤ 2: commP is bimultiplicative and squaring is quadratic. These are the two facts that cut Z₂ down from the Q₃ × Q₃-worth of generators supplied by λ₂ = cl(λ₁²[λ₁, λ₁]) to the squares and pairwise brackets of a generating triple.

theorem GQ2.Roe.Labute.commP_mem_zLayer_two {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (p q : levelQuot G 3) : commP p q ∈ zLayer G 2

Every commP in Q₃ lands in Z₂.

theorem GQ2.Roe.Labute.sq_mem_zLayer_two {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (p : levelQuot G 3) : p ^ 2 ∈ zLayer G 2

Every square in Q₃ lands in Z₂.

theorem GQ2.Roe.Labute.commP_mul_left_of_three {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (p q r : levelQuot G 3) : commP (p * q) r = commP p r * commP q r

commP is multiplicative in the left slot (class 2: the conjugation in commP_mul_left acts on a central element).

theorem GQ2.Roe.Labute.commP_mul_right_of_three {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (p q r : levelQuot G 3) : commP p (q * r) = commP p r * commP p q

commP is multiplicative in the right slot (class 2).

theorem GQ2.Roe.Labute.commP_inv_left_of_three {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (p r : levelQuot G 3) : commP p⁻¹ r = (commP p r)⁻¹

commP inverts in the left slot.

theorem GQ2.Roe.Labute.commP_inv_right_of_three {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (p r : levelQuot G 3) : commP p r⁻¹ = (commP p r)⁻¹

commP inverts in the right slot.

theorem GQ2.Roe.Labute.sq_mul_of_three {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (p q : levelQuot G 3) : (p * q) ^ 2 = p ^ 2 * q ^ 2 * (commP p q)⁻¹

Squaring is quadratic in Q₃: (pq)² = p²q²[p, q]⁻¹.

theorem GQ2.Roe.Labute.commP_mem_of_gens {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {a b c : levelQuot G 3} (hgen : Subgroup.closure {a, b, c} = ⊤) {K : Subgroup (levelQuot G 3)} (hab : commP a b ∈ K) (hac : commP a c ∈ K) (hbc : commP b c ∈ K) (p q : levelQuot G 3) : commP p q ∈ K

Every bracket of Q₃ lies in a subgroup holding the six generator brackets. Bimultiplicativity in both slots turns the closure induction on each argument into bookkeeping over the nine generator pairs.

theorem GQ2.Roe.Labute.sq_mem_of_gens {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {a b c : levelQuot G 3} (hgen : Subgroup.closure {a, b, c} = ⊤) {K : Subgroup (levelQuot G 3)} (ha : a ^ 2 ∈ K) (hb : b ^ 2 ∈ K) (hc : c ^ 2 ∈ K) (hab : commP a b ∈ K) (hac : commP a c ∈ K) (hbc : commP b c ∈ K) (p : levelQuot G 3) : p ^ 2 ∈ K

Every square of Q₃ lies in a subgroup holding the three generator squares and the six generator brackets (sq_mul_of_three for the product step).

theorem GQ2.Roe.Labute.zLayer_two_le_of_gens {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hopen : IsOpen ↑(twoCentralSeries G 3)) {a b c : levelQuot G 3} (hgen : Subgroup.closure {a, b, c} = ⊤) {K : Subgroup (levelQuot G 3)} (ha : a ^ 2 ∈ K) (hb : b ^ 2 ∈ K) (hc : c ^ 2 ∈ K) (hab : commP a b ∈ K) (hac : commP a c ∈ K) (hbc : commP b c ∈ K) : zLayer G 2 ≤ K

Layer generation at level 3. A subgroup K of Q₃ containing the squares and the pairwise brackets of a topologically generating triple contains the whole layer Z₂. λ₂ = cl(λ₁²[λ₁, λ₁]) offers one generator of Z₂ per square and per commutator of Q₃; the class-2 calculus reduces those to the three squares and three brackets, and the openness of λ₃ makes the preimage of K closed, so it absorbs the topological closure.

Base cases at k₀ = 3 (spike §2.4, §3.1, §3.4)

The level-3 witnesses live in Q₃ of order 2^8 = 256; L3 discharges membership by transport to a concrete 256-element model and decide/structured verification (plan §2.3), checking the χ-clause mod 8 against chiTargetR0_three/chiTargetR2_three.

Level-4 stress vectors (spike §3.4, NOT frozen as statements — optional extra greens for L3, words recorded for reproducibility; repo convention [s,y] = s⁻¹y⁻¹sy):

• direction 1, level 4: t₁ = y·s·x⁻¹·s·x·s⁻¹·y⁻¹·s·y·x⁻¹·y⁻¹·x·y, t₂ = s·x·[s,y], t₃ = x·[s,y] (χ-depths (6, 5, 5)).
• direction 2, level 4: the spike's witness_words.txt triple of lengths (12, 7, 11) with χ-depths (4, 5, 6).

theorem GQ2.Roe.Labute.levelMk_drY_sq : (levelMk (↑DR.toProfinite.toTop) 3) drY ^ 2 = commP ((levelMk (↑DR.toProfinite.toTop) 3) drX) ((levelMk (↑DR.toProfinite.toTop) 3) drS)

The D_R relator read in Q₃: it collapses to y² = [x, s] (repo commP). The [y, yˢ] block is inert (a commP against the Z₂-element [y, s]), x⁴ = 1 in Q₃ (λ₂² ⊆ λ₃), and conjP x s = x · [x, s], so the two surviving terms are y² and the cross term [x, s]. This is the single linear relation that cuts dim Z₂ from 6 to 5; it is what makes |Q₃| = 2⁸ rather than 2⁹.

noncomputable def GQ2.Roe.Labute.witnessR0 : Fin 3 → levelQuot (↑DR.toProfinite.toTop) 3

The direction-1 base witness in Q₃(D_R) (spike §3.1/§3.4): the (A,S,Y)-slot triple (y, s·x, x) — mod-8 χ-values (7, 1, 5), matching chiTargetR0_three.

Equations

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

theorem GQ2.Roe.Labute.witnessR0_mem : witnessR0 ∈ sPR0 3

Base case, direction 1 (spike §2.4: S^P₃ ≠ ∅ by explicit witness). Fill: L3 (decide/structured verification in a 256-element model of Q₃).

theorem GQ2.Roe.Labute.sPR0_three_nonempty : (sPR0 3).Nonempty

S^P₃ ≠ ∅, direction 1 (packaging; not a fill target).

noncomputable def GQ2.Roe.Labute.witnessR2 : Fin 3 → levelQuot (↑D0.toProfinite.toTop) 3

The direction-2 base witness in Q₃(D₀) (spike §3.1/§3.4): the (s,x,y)-slot triple (S·Y, Y, A) — mod-8 χ₀-values (5, 5, 7), matching chiTargetR2_three.

Equations

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

theorem GQ2.Roe.Labute.witnessR2_mem : witnessR2 ∈ sPR2 3

Base case, direction 2. Fill: L3.

theorem GQ2.Roe.Labute.sPR2_three_nonempty : (sPR2 3).Nonempty

S^P₃ ≠ ∅, direction 2 (packaging; not a fill target).

Tower-size regression pins (spike §1 table; L1 stress contract for L3)

log₂|Q₂| = 3, log₂|Q₃| = 8, dim Z₁ = 3 — identical for both towers (f-blind, spike §1), so pinned on the D_R-side only.

Q₂ is the Frattini quotient of D_R: squares and commutators lie in λ₂, so Q₂ is abelian of exponent 2, and it is generated by the three marked generators — whence |Q₂| ≤ 2³. The elementary-abelian marking (s, x, y) ↦ standard basis of (ℤ/2)³ — a drLiftHom at a concrete finite 2-group with the relator killed by the house decide pattern (DRPresentation.lean's drWord_zmod8/drWord_d4) — gives the matching lower bound.

theorem GQ2.Roe.Labute.card_levelQuot_two : Nat.card (levelQuot (↑DR.toProfinite.toTop) 2) = 8

|Q₂(D_R)| = 8 (spike §1, k = 1 row). Fill: L3.

Q₃ sits in the extension 1 → Z₂ → Q₃ → Q₂ → 1. The layer Z₂ is spanned by the five classes s², x², [s,x], [s,y], [x,y]: zLayer_two_le_of_gens offers the three generator squares and the three generator brackets, and the relator relation y² = [x,s] (levelMk_drY_sq) deletes one of the six. Hence |Z₂| ≤ 2⁵, and |Q₃| = |Q₂| · |Z₂| ≤ 8 · 32 = 256.

The order-256 model (spike §2.3, plan §2.3)

Q₃ is realised on the nose by the central extension M = 𝔽₂³ ×_f 𝔽₂⁵ with the bilinear cocycle f a b = (a₀b₀, a₁b₁, a₀b₁ + a₂b₂, a₀b₂, a₁b₂). Bilinearity is the whole design: the cocycle identity f a b + f (a+b) c = f b c + f a (b+c) is then a polynomial identity, so associativity is ring on each coordinate rather than a 256³-case decide.

The five z-coordinates are the five spanning classes of Z₂: s², x², [s,x], [s,y], [x,y]. The a₀b₁ + a₂b₂ entry in the third slot is exactly the relator relation y² = [s,x] (levelMk_drY_sq) built into the model, which is why drWord dies at the standard basis.

@[implicit_reducible]

instance GQ2.Roe.Labute.instDecidableEqMR : DecidableEq GQ2.Roe.Labute.MR✝

Equations

• GQ2.Roe.Labute.instDecidableEqMR = GQ2.Roe.Labute.instDecidableEqMR.decEq

def GQ2.Roe.Labute.instDecidableEqMR.decEq (x✝ x✝¹ : GQ2.Roe.Labute.MR✝) : Decidable (x✝ = x✝¹)

Equations

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

theorem GQ2.Roe.Labute.card_levelQuot_three : Nat.card (levelQuot (↑DR.toProfinite.toTop) 3) = 256

|Q₃(D_R)| = 256 — the base-case budget (spike §1, k₀ = 3 lives here). Fill: L3.

theorem GQ2.Roe.Labute.card_zLayer_one : Nat.card ↥(zLayer (↑DR.toProfinite.toTop) 1) = 8

|Z₁(D_R)| = 2³ (spike §1: dim Z₁ = 3). Fill: L3.

Z₁ = λ₁λ₂/λ₂ is the image of λ₁ = ⊤, i.e. all of Q₂, so this is card_levelQuot_two read through Subgroup.topEquiv.

theorem GQ2.Roe.Labute.sPR0_one_nonempty : (sPR0 1).Nonempty

Smoke: the level-1 set is inhabited by the trivial triple (Q₁ = 1; every clause degenerates — validates that the three-clause definition elaborates and composes).