12. The square-commutator presentation🔗

Definition12.1

Group: The square-commutator presentation (10)

Group member previews

Preview

Theorem 12.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Definition C.1 of the paper (The square-commutator candidate).

Let F be the free profinite group on \sigma,\tau,x_0,x_1. Call an epimorphism \varphi:F\twoheadrightarrow G to a finite group square-commutator admissible if the distinguished tuple generates G, satisfies (5) and

(x_0^{\sigma})^{-1}\,a\,x_1^2\,c=1,

and the normal closure of \varphi(x_0),\varphi(x_1) is a 2-group. Let \mathcal Q_R be the class of all such quotients and set

N_R=\bigcap_{\varphi\in\mathcal Q_R}\ker\varphi, \qquad \Gamma_R=F/N_R.

For a finite group G write \mathrm{ac}_R(G) for the number of square-commutator admissible markings of G, that is, of generating quadruples in G^4 satisfying (5) and (199) whose last two entries lie in the 2-core, as in Proposition 3.1.

Lean code for Definition12.1●4 definitions

defdefined in GQ2/Roe/Words.lean

complete

def GQ2.Marking.wildValueR.{u_1} {G : Type u_1} [Group G]
  (t : GQ2.Marking G) : G

def GQ2.Marking.wildValueR.{u_1}
  {G : Type u_1} [Group G]
  (t : GQ2.Marking G) : G

The **Roe wild relator value** `r_R` at a marking — note eq. (1.2) ⟦eq:relators⟧, verbatim
`\rR=(x_0^\sigma)^{-1}a\,x_1^2c`, i.e.

  `r_R = (x₀ ^c σ)⁻¹ · a · x₁² · c`   **in exactly this order**,

with `a = Marking.aR` and `c = Marking.cR`.  The `Γ_A` analogue is `Marking.wildValue`.  The two
`ω₂`-powers sit inside `aR` and inside `cR`'s `sigma2`; the finite-exponent form (for a concrete
integer representative of `ω₂`) is `wildValueExpR`.

defdefined in GQ2/Roe/Words.lean

complete

def GQ2.Marking.WildRelR.{u_1} {G : Type u_1} [Group G]
  (t : GQ2.Marking G) : Prop

def GQ2.Marking.WildRelR.{u_1} {G : Type u_1}
  [Group G] (t : GQ2.Marking G) : Prop

The **Roe wild relation** `r_R = 1` (note eq. (1.2) ⟦eq:relators⟧ / Definition 1.1
⟦def:GammaR⟧) — the Roe-candidate counterpart of `Marking.WildRel`.

defdefined in GQ2/Roe/GammaR.lean

complete

def GQ2.GammaR : ProfiniteGrp.{0}

def GQ2.GammaR : ProfiniteGrp.{0}

**`Γ_R`** (note Definition 1.1 ⟦def:GammaR⟧): the marked quotient `F₄ ⧸ N_R` — the largest
quotient of `F₄` all of whose finite quotients are `R`-admissible, constructed exactly as `Γ_A`
but with the Roe wild relation.  Roe counterpart of `GQ2.GammaA`.

defdefined in GQ2/Roe/Words.lean

complete

def GQ2.admissibleCountR.{u_1} (G : Type u_1) [Group G] : ℕ

def GQ2.admissibleCountR.{u_1} (G : Type u_1)
  [Group G] : ℕ

The finite count `N_R(G)` of `R`-admissible markings — the Roe-candidate analogue of
`GQ2.admissibleCount` and the right-hand side of the surjection-count semantics of the note's
Definition 1.1 ⟦def:GammaR⟧ (`|Sur(Γ_R, G)| = admissibleCountR G` is ticket R4's `prop_2_3_R`).
Well-defined (finite) for any finite group since `Marking G ≃ G⁴`.

Theorem12.2

Group: The square-commutator presentation (10)

Group member previews

Preview

Definition 12.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Theorem C.3 of the paper (Replacement theorem).

\Gamma_R\cong\GQ. Equivalently,

|\Sur(\Gamma_R,G)|=|\Sur(\GQ,G)|

for every finite group G; equivalently again, \mathrm{ac}_R(G)=|\Sur(\GQ,G)| for every finite group G. Consequently the two candidates present the same group, and their marking counts agree: \mathrm{ac}_R(G)=\mathrm{ac}(G) for every finite G.

Lean code for Theorem12.2●4 theorems

theoremdefined in GQ2/Roe/Main.lean

complete

theorem GQ2.main_presentation_literal_roe_unconditional :
  Nonempty (↑GQ2.GammaR.toProfinite.toTop ≃ₜ* GQ2.AbsGalQ2)

theorem GQ2.main_presentation_literal_roe_unconditional :
  Nonempty
    (↑GQ2.GammaR.toProfinite.toTop ≃ₜ*
      GQ2.AbsGalQ2)

**The Replacement theorem, unconditionally** (note ⟦thm:main⟧; the campaign's terminal
statement): the Roe candidate `Γ_R` (Definition 1.1 ⟦def:GammaR⟧) is continuously isomorphic
to `G_{ℚ₂}` — no hypotheses, no instance binders.

The single input of `main_presentation_literal_roe`, the Labute classification instance
`BLabHypothesis` (note Cor. 3.4 ⟦cor:abstractD0⟧, `D_R ≅ D₀` as marked Demushkin groups), was
**declined as an axiom** by the owner (2026-07-25) and **discharged as a theorem** by the
L-campaign (2026-07-26): `GQ2.Roe.Labute.bLab` (`GQ2/Roe/Labute/Assembly.lean`) proves it from
the λ-tower stage lemma, the levelwise sets and the profinite Hopfian endgame, at the standard
three axioms and with no `sorry` anywhere in its chain.

Consequently this theorem prints exactly the frozen literature census of the `Γ_A` capstones
(std-3 + the axioms of `GQ2/Foundations/Axioms.lean`) — the Roe route adds **nothing** to the
trust base, which `scripts/check_axioms.sh` (check 5) enforces.

theoremdefined in GQ2/Roe/Main.lean

complete

theorem GQ2.main_surjection_count_R [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] (hBLab : GQ2.BLabHypothesis)
  (G : Type) [Group G] [Finite G] [TopologicalSpace G]
  [DiscreteTopology G] : GQ2.contSurjCount G = GQ2.admissibleCountR G

theorem GQ2.main_surjection_count_R
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (hBLab : GQ2.BLabHypothesis) (G : Type)
  [Group G] [Finite G]
  [TopologicalSpace G]
  [DiscreteTopology G] :
  GQ2.contSurjCount G =
    GQ2.admissibleCountR G

**The `Γ_R` surjection-count capstone** (⟦thm:main⟧, counting layer, mirroring
`SectionTen.main_surjection_count'`): the number of continuous surjections `G_{ℚ₂} ↠ G`
equals the number of admissible **Roe**-marked generating quadruples of `G`
(eq. (154) at `Γ_R` + Prop 2.3 for the Roe words, `prop_2_3_R`).

theoremdefined in GQ2/Roe/Main.lean

complete

theorem GQ2.eq_154_R [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] (hBLab : GQ2.BLabHypothesis)
  (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G]
  [Finite G] :
  Nat.card (GQ2.ContSurj (↑GQ2.GammaR.toProfinite.toTop) G) =
    Nat.card (GQ2.ContSurj GQ2.AbsGalQ2 G)

theorem GQ2.eq_154_R [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (hBLab : GQ2.BLabHypothesis) (G : Type)
  [Group G] [TopologicalSpace G]
  [DiscreteTopology G] [Finite G] :
  Nat.card
      (GQ2.ContSurj
        (↑GQ2.GammaR.toProfinite.toTop)
        G) =
    Nat.card (GQ2.ContSurj GQ2.AbsGalQ2 G)

**Eq. (154) at `Γ_R`** (⟦thm:main⟧, counting layer): the Roe candidate and `G_{ℚ₂}` have
identical continuous-surjection counts onto every finite group.  `card_contSurj_eq` at
`(sourceR hBLab).b` / `boundaryMapsWitness.bF` rewrites each count as the sum of fixed-frame
exact-image counts; `thm_4_2_of_sources` equates them frame by frame — the "R32 path" pinned
by R30.  Stated `calc`-style because the `Γ_R` side enters through `(sourceR hBLab).b`
(definitionally, not syntactically, a `Γ_R`-boundary map).

theoremdefined in GQ2/Roe/Main.lean

complete

theorem GQ2.admissibleCountR_eq_admissibleCount [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] (hBLab : GQ2.BLabHypothesis)
  (G : Type) [Group G] [Finite G] [TopologicalSpace G]
  [DiscreteTopology G] : GQ2.admissibleCountR G = GQ2.admissibleCount G

theorem GQ2.admissibleCountR_eq_admissibleCount
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (hBLab : GQ2.BLabHypothesis) (G : Type)
  [Group G] [Finite G]
  [TopologicalSpace G]
  [DiscreteTopology G] :
  GQ2.admissibleCountR G =
    GQ2.admissibleCount G

**The two admissible-marking semantics agree** on every finite group (the numerical
content R5 verified four ways on `C₂ : 7`, `C₄ : 24`, `V₄ : 42`, `D₄ : 144`, `Q₈ : 144` —
Lean word-level pins, two independent Python engines, and the June LMFDB-verified counts;
`GQ2/Roe/Sanity.lean`, `scripts/roe_sanity_counts.py`).

Proof for Theorem 12.2

Proof uses 5

Proof dependency previews

Preview

Proposition 3.1

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §C of the paper. Ingredients: Lemma 3.2 Lemma 11.1 Proposition 3.1 Proposition 12.3 Theorem 5.1.

Proposition12.3

Group: The square-commutator presentation (10)

Group member previews

Preview

Definition 12.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Proposition C.5 of the paper (The interface at the square-commutator relator).

The source \Gamma_R satisfies every item of Corollary 7.12, and in addition:

its tame quotient is \TA, with the unramified marking of Proposition 4.2 and Proposition 4.9;
its fully marked maximal pro-2 quotient is (G_{\Qtwo}(2),\nu_{\mathrm{ur}}).

Lean code for Proposition12.3●4 declarations

structure(33 fields)defined in GQ2/SourceData.lean

complete

structure GQ2.SourceData : Type 1

structure GQ2.SourceData : Type 1

**The pluggable source** (the SourceData refactor): everything the two-source assembly
consumes about the candidate slot.  Data fields = the eq. (27) boundary interface of a
presented source (Prop 3.10 / Prop 3.14, pinned by generator values as for `Γ_A`), with
`ker_pro2` **promoted to a field** (the recon's 12 + 1; `Γ_A` derives it as
`SectionNine.ker_pro2A`, `Γ_R` from its max-pro-2 identification).  Prop fields = the seven
supply-obligation families, each in the exact ∀-shape of its `_gammaA` witness, so
`BoundaryMaps.sourceA` is assembled from the untouched lemmas and `sourceR` from R31's.

Fields

Γ : ProfiniteGrp.{0}

The source group, as a bundled profinite group (the R31a carrier decision: all
topology/group instances flow from `ProfiniteGrp`).

sigma : ↑self.Γ.toProfinite.toTop

The marked generator `σ` of the source presentation.

tau : ↑self.Γ.toProfinite.toTop

The marked generator `τ`.

x0 : ↑self.Γ.toProfinite.toTop

The marked generator `x₀`.

x1 : ↑self.Γ.toProfinite.toTop

The marked generator `x₁`.

tame : ↑self.Γ.toProfinite.toTop →ₜ* ↑GQ2.Ttame.toProfinite.toTop

The tame quotient map (eq. (27), tame component; Prop 3.2/Prop 3.14).

pro2 : ↑self.Γ.toProfinite.toTop →ₜ* ↑GQ2.PiBd.toProfinite.toTop

The maximal pro-2 quotient map (eq. (27), pro-2 component; Prop 3.10).

compat : ∀ (g : ↑self.Γ.toProfinite.toTop), GQ2.nuT (self.tame g) = GQ2.nuTwo (self.pro2 g)

Prop 3.14's ν-compatibility: `ν_t ∘ tame = ν₂ ∘ pro2` (what lands `b_Γ` in `∂bd`).

tame_sigma : self.tame self.sigma = GQ2.tameSigma

Generator pinning (Prop 3.14's proof): `tame σ = σ`.

tame_tau : self.tame self.tau = GQ2.tameTau

Generator pinning: `tame τ = τ`.

tame_x0 : self.tame self.x0 = 1

Generator pinning: `tame x₀ = 1`.

tame_x1 : self.tame self.x1 = 1

Generator pinning: `tame x₁ = 1`.

pro2_sigma : self.pro2 self.sigma = GQ2.piSigma

Generator pinning (Prop 3.10): `pro2 σ = σ`.

pro2_tau : self.pro2 self.tau = 1

Generator pinning: `pro2 τ = 1`.

pro2_x0 : self.pro2 self.x0 = GQ2.piX0

Generator pinning: `pro2 x₀ = x₀`.

pro2_x1 : self.pro2 self.x1 = GQ2.piX1

Generator pinning: `pro2 x₁ = x₁`.

surj : Function.Surjective fun g => ⟨(self.tame g, self.pro2 g), ⋯⟩

Eq. (27): joint surjectivity of `b_Γ : Γ ↠ ∂bd`.

ker_pro2 : self.pro2.ker = GQ2.proPKernel 2 ↑self.Γ.toProfinite.toTop

**The promoted field** (recon 12 + 1): `pro2` is *the* maximal pro-2 quotient map —
its kernel is the pro-2 kernel of the maximal pro-p quotient API.  (`Γ_A`:
`SectionNine.ker_pro2A`; consumed by the §9.1 terminal identification.)

smulZmod2 : DistribMulAction (↑self.Γ.toProfinite.toTop) (ZMod 2)

The ambient `ZMod 2`-scalar action of the source (trivial, by `htriv` below) — the
instance the (140)/Gauss-`Z` layers are stated at (`Γ_A`: the global instance of
`GQ2/RStage/GammaA.lean`).

contSMulZmod2 : ContinuousSMul (↑self.Γ.toProfinite.toTop) (ZMod 2)

Continuity of the ambient scalar action.

htriv : ∀ (γ : ↑self.Γ.toProfinite.toTop) (m : ZMod 2), γ • m = m

The ambient scalar action is trivial (`Γ_A`: `RStageGammaA.htriv_gammaA`).

tfg : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤

**(ii.1) topological finite generation** (`Γ_A`:
`gammaA_topologicallyFinitelyGenerated`; `Γ_R`:
`gammaR_topologicallyFinitelyGenerated`, R31a).

hom8 : Nat.card (↑self.Γ.toProfinite.toTop →ₜ* Multiplicative (ZMod 2)) = 8

**(ii.2) Lemma 8.2**: `#Hom_cont(Γ, 𝔽₂) = 8` (`Γ_A`: `lemma_8_2_gammaA`; `Γ_R`:
`lemma_8_2_R`, R31a).

cardH2 : Nat.card (GQ2.ContCoh.H2 (↑self.Γ.toProfinite.toTop) (ZMod 2)) = 2

**(ii.5, leaf) `#H²(Γ, 𝔽₂) = 2`** at the ambient (trivial) action (`Γ_A`:
`CardH2GammaA.card_H2_gammaA`).

liftsOver_card : ∀ {H E : Type} [inst : Group H] [inst_1 : TopologicalSpace H] [inst_2 : DiscreteTopology H] [inst_3 : Finite H]
  [inst_4 : CommGroup E] [inst_5 : TopologicalSpace E] [inst_6 : DiscreteTopology E] [inst_7 : Finite E] {Y : Type}
  [inst_8 : Group Y] [inst_9 : Finite Y] {T : GQ2.MarkedTarget H E Y} {Blk : GQ2.SectionSeven.MinimalBlock T.LY}
  (RF : GQ2.SectionEight.RecursionFrame T Blk) (b : ↑self.Γ.toProfinite.toTop →ₜ* ↥GQ2.boundarySubgroup)
  (F : GQ2.BoundaryFrame H E) (ρ : GQ2.BoundaryLifts b F RF.TC), Nat.card (RF.LiftsOver b F ρ) = Nat.card ↥RF.MB ^ 2

**(ii.3) the `M`-stage multiplicity** (props 5.15/5.16): `#LiftsOver(ρ) = |M_B|²`
over every lower boundary lift (`Γ_A`: `RecursionFrame.liftsOver_card_gammaA`).

lem86 : ∀ {Bg : Type} [inst : Group Bg] [inst_1 : TopologicalSpace Bg] [DiscreteTopology Bg] [inst_3 : Finite Bg]
  (D : GQ2.SectionEight.RadicalCoverData Bg),
  D.NoDescent →
    ∀ (ρ : ↑self.Γ.toProfinite.toTop →ₜ* Bg ⧸ D.M),
      Function.Surjective ⇑ρ →
        2 * Nat.card { f // GQ2.SectionEight.MLifts.Central D f } = Nat.card (GQ2.SectionEight.MLifts D ρ)

**(ii.4) Lemma 8.6 (half-torsor count)** ⟦lem-radicaledge⟧: with a nonzero radical
edge, exactly half of the `M`-lifts of a lower epimorphism satisfy the central relation
(`Γ_A`: `lemma_8_6_gammaA`).

stageR136 : ∀ {H E : Type} [inst : Group H] [inst_1 : TopologicalSpace H] [inst_2 : DiscreteTopology H] [inst_3 : Finite H]
  [inst_4 : CommGroup E] [inst_5 : TopologicalSpace E] [inst_6 : DiscreteTopology E] [inst_7 : Finite E] {Y : Type}
  [inst_8 : Group Y] [inst_9 : TopologicalSpace Y] [DiscreteTopology Y] [inst_11 : Finite Y]
  {T : GQ2.MarkedTarget H E Y} {Blk : GQ2.SectionSeven.MinimalBlock T.LY} (hE2 : ∀ (e : E), e ^ 2 = 1),
  (∀ r ∈ Blk.frattiniK, ∀ k ∈ Blk.K, r * k = k * r) →
    (∀ r ∈ Blk.frattiniK, r * r = 1) →
      ∀ (b : ↑self.Γ.toProfinite.toTop →ₜ* ↥GQ2.boundarySubgroup) (F : GQ2.BoundaryFrame H E),
        ↑(Nat.card (GQ2.blockFrameImpl T Blk hE2).DR) * ↑(GQ2.exactImageCount b F T) =
          ↑(GQ2.blockFrameImpl T Blk hE2).zR *
            ∑ᶠ (l : (GQ2.blockFrameImpl T Blk hE2).DR),
              (2 * ↑((GQ2.blockFrameImpl T Blk hE2).mB b F l) -
                ↑(GQ2.exactImageCount b F (GQ2.blockFrameImpl T Blk hE2).TB))

**(ii.5, assembled) the (136) stage at the block frame** (`Γ_A`:
`CardH2GammaA.stageR136_gammaA`, built from `cardH2` through the generic
`stageR136`-builders).

tcocycle_card : ∀ {H E : Type} [inst : Group H] [inst_1 : TopologicalSpace H] [inst_2 : DiscreteTopology H] [inst_3 : Finite H]
  [inst_4 : CommGroup E] [inst_5 : TopologicalSpace E] [inst_6 : DiscreteTopology E] [inst_7 : Finite E] {Y : Type}
  [inst_8 : Group Y] [inst_9 : Finite Y] {T : GQ2.MarkedTarget H E Y} {Blk : GQ2.SectionSeven.MinimalBlock T.LY}
  {RF : GQ2.SectionEight.RecursionFrame T Blk} (b : ↑self.Γ.toProfinite.toTop →ₜ* ↥GQ2.boundarySubgroup)
  (F : GQ2.BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : GQ2.BoundaryLifts b F RF.TC),
  Nat.card (GQ2.SectionEight.CentralObstruction.TCocycle (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) =
    Nat.card (Additive ↥(En.radData l h).T) ^ 2 *
      Nat.card ↑(GQ2.FoxH.fixedPts (RF.YB ⧸ (En.radData l h).M) (GQ2.FoxH.ElemDual (Additive ↥(En.radData l h).T)))

**(ii.6) the `T`-cocycle count** in the `muZero` closed form (`Γ_A`:
`Phase140GammaA.tcocycle_card_gammaA`).

hsep : ∀ {H E : Type} [inst : Group H] [inst_1 : TopologicalSpace H] [inst_2 : DiscreteTopology H] [inst_3 : Finite H]
  [inst_4 : CommGroup E] [inst_5 : TopologicalSpace E] [inst_6 : DiscreteTopology E] [inst_7 : Finite E] {Y : Type}
  [inst_8 : Group Y] [inst_9 : Finite Y] {T : GQ2.MarkedTarget H E Y} {Blk : GQ2.SectionSeven.MinimalBlock T.LY}
  {RF : GQ2.SectionEight.RecursionFrame T Blk} (b : ↑self.Γ.toProfinite.toTop →ₜ* ↥GQ2.boundarySubgroup)
  (F : GQ2.BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR)
  (Dsc : GQ2.SectionEight.AffineTLift.Descent (En.radData l h)) (ρ : GQ2.BoundaryLifts b F RF.TC)
  (c : GQ2.SectionEight.AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)),
  (∀ (χ : ↥(GQ2.SectionEight.AffineTLift.TCharC (En.radData l h))),
      GQ2.SectionEight.AffineTLift.betaChi (GQ2.SectionEight.descSections En l h Dsc) ⋯ χ c = 0) →
    GQ2.SectionEight.AffineTLift.TLiftable ⋯ c

**(ii.6) the `(T^∨)^C`-separation**: a `V`-coordinate whose `χ`-obstructions all
vanish is `T`-liftable (`Γ_A`: `Phase140GammaA.hsep_gammaA`).

hpartial : ∀ {H E : Type} [inst : Group H] [inst_1 : TopologicalSpace H] [inst_2 : DiscreteTopology H] [inst_3 : Finite H]
  [inst_4 : CommGroup E] [inst_5 : TopologicalSpace E] [inst_6 : DiscreteTopology E] [inst_7 : Finite E] {Y : Type}
  [inst_8 : Group Y] [inst_9 : Finite Y] {T : GQ2.MarkedTarget H E Y} {Blk : GQ2.SectionSeven.MinimalBlock T.LY}
  {RF : GQ2.SectionEight.RecursionFrame T Blk} (b : ↑self.Γ.toProfinite.toTop →ₜ* ↥GQ2.boundarySubgroup)
  (F : GQ2.BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR)
  (Dsc : GQ2.SectionEight.AffineTLift.Descent (En.radData l h)) (ρ : GQ2.BoundaryLifts b F RF.TC)
  (χ : ↥(GQ2.SectionEight.AffineTLift.TCharC (En.radData l h))),
  χ ≠ 0 →
    ∃ c,
      GQ2.SectionEight.AffineTLift.betaChi (GQ2.SectionEight.descSections En l h Dsc) ⋯ χ c ≠
        GQ2.SectionEight.AffineTLift.betaChi (GQ2.SectionEight.descSections En l h Dsc) ⋯ χ 0

**(ii.6) nondegeneracy of the obstruction pairing in the character** (`Γ_A`:
`Phase140GammaA.hpartial_gammaA`).

hZcard : ∀ {H E : Type} [inst : Group H] [inst_1 : TopologicalSpace H] [inst_2 : DiscreteTopology H] [inst_3 : Finite H]
  [inst_4 : CommGroup E] [inst_5 : TopologicalSpace E] [inst_6 : DiscreteTopology E] [inst_7 : Finite E] {Y : Type}
  [inst_8 : Group Y] [inst_9 : Finite Y] {T : GQ2.MarkedTarget H E Y} {Blk : GQ2.SectionSeven.MinimalBlock T.LY}
  {RF : GQ2.SectionEight.RecursionFrame T Blk} (b : ↑self.Γ.toProfinite.toTop →ₜ* ↥GQ2.boundarySubgroup)
  (F : GQ2.BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR),
  (∀ (W : AddSubgroup En.Vmod), (∀ (g : RF.YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) →
    (∃ v, v ≠ 0) →
      (∃ g v, g • v ≠ v) →
        ∀ (ρ : GQ2.BoundaryLifts b F RF.TC),
          Nat.card (GQ2.SectionEight.AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) =
            Nat.card En.Vmod * Nat.card En.Vmod

**(ii.6) the `V`-cocycle count** `#Z¹_{Γ,ρ'}(V) = #V²` under the simple nontrivial
`Y_C`-action (`Γ_A`: `Phase140GammaA.hZcard_gammaA`).

gaussZ_unramified : ∀ {H E : Type} [inst : Group H] [inst_1 : TopologicalSpace H] [inst_2 : DiscreteTopology H] [inst_3 : Finite H]
  [inst_4 : CommGroup E] [inst_5 : TopologicalSpace E] [inst_6 : DiscreteTopology E] [inst_7 : Finite E] {Y : Type}
  [inst_8 : Group Y] [inst_9 : TopologicalSpace Y] [inst_10 : DiscreteTopology Y] [inst_11 : Finite Y]
  (T : GQ2.MarkedTarget H E Y) (Blk : GQ2.SectionSeven.MinimalBlock T.LY) [inst_12 : Blk.frattiniK.Normal]
  [inst_13 : (Blk.S.subgroupOf Blk.P).Normal] [inst_14 : Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1)
  (F : GQ2.BoundaryFrame H E),
  (∀ (W : AddSubgroup (GQ2.SectionNine.blockEnrichmentD T Blk hE2 F).Vmod),
      (∀ (g : (GQ2.SectionNine.blockFrame T Blk hE2).YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) →
    (∃ v, v ≠ 0) →
      (∃ g v, g • v ≠ v) →
        ∀ (m : ℕ),
          1 ≤ m →
            Nat.card (GQ2.SectionNine.blockEnrichmentD T Blk hE2 F).Vmod = 2 ^ (2 * m) →
              ∀ (l : (GQ2.SectionNine.blockFrame T Blk hE2).DR) (h : l ≠ (GQ2.SectionNine.blockFrame T Blk hE2).zeroDR),
                (∀ (v : Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P)), F.alpha GQ2.tameTau • v = v) →
                  GQ2.SectionEight.GaussZResidue (GQ2.sourceBoundaryMap self.tame self.pro2 ⋯) F
                    (GQ2.SectionNine.blockEnrichmentD T Blk hE2 F) l h (-2 ^ m)

**(ii.7) the Gauss-`Z` residue, unramified head** (the (83)-evaluation at the
**externally given** `G0 = −2^m` — the recon's shared-`G0` seam): at the head-inflated
enrichment, with the head dichotomy `F.alpha τ`-trivial (`Γ_A`:
`SectionNine.gaussZResidueD_gammaA_unramified`).

gaussZ_ramified : ∀ {H E : Type} [inst : Group H] [inst_1 : TopologicalSpace H] [inst_2 : DiscreteTopology H] [inst_3 : Finite H]
  [inst_4 : CommGroup E] [inst_5 : TopologicalSpace E] [inst_6 : DiscreteTopology E] [inst_7 : Finite E] {Y : Type}
  [inst_8 : Group Y] [inst_9 : TopologicalSpace Y] [inst_10 : DiscreteTopology Y] [inst_11 : Finite Y]
  (T : GQ2.MarkedTarget H E Y) (Blk : GQ2.SectionSeven.MinimalBlock T.LY) [inst_12 : Blk.frattiniK.Normal]
  [inst_13 : (Blk.S.subgroupOf Blk.P).Normal] [inst_14 : Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1)
  (F : GQ2.BoundaryFrame H E),
  (∀ (W : AddSubgroup (GQ2.SectionNine.blockEnrichmentD T Blk hE2 F).Vmod),
      (∀ (g : (GQ2.SectionNine.blockFrame T Blk hE2).YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) →
    (∃ v, v ≠ 0) →
      (∃ g v, g • v ≠ v) →
        ∀ (m : ℕ),
          1 ≤ m →
            Nat.card (GQ2.SectionNine.blockEnrichmentD T Blk hE2 F).Vmod = 2 ^ (2 * m) →
              ∀ (l : (GQ2.SectionNine.blockFrame T Blk hE2).DR) (h : l ≠ (GQ2.SectionNine.blockFrame T Blk hE2).zeroDR),
                (∃ v, F.alpha GQ2.tameTau • v ≠ v) →
                  GQ2.SectionEight.GaussZResidue (GQ2.sourceBoundaryMap self.tame self.pro2 ⋯) F
                    (GQ2.SectionNine.blockEnrichmentD T Blk hE2 F) l h (2 ^ m)

**(ii.7) the Gauss-`Z` residue, ramified head** (`G0 = +2^m`; `Γ_A`:
`SectionNine.gaussZResidueD_gammaA_ramified`).

theoremdefined in GQ2/ThmFourTwo.lean

complete

theorem GQ2.thm_4_2_of_sources {H E : Type} [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E] (S : GQ2.SourceData)
  (B : GQ2.BoundaryMaps) (F : GQ2.BoundaryFrame H E)
  (R : GQ2.LocalReciprocity)
  (horient : GQ2.TameUnitOrientation R B.tameF)
  [CompactSpace GQ2.AbsGalQ2] [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y]
  [Finite Y] (T : GQ2.MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1) :
  GQ2.exactImageCount S.b F T = GQ2.exactImageCount B.bF F T

theorem GQ2.thm_4_2_of_sources {H E : Type}
  [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H]
  [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E]
  (S : GQ2.SourceData)
  (B : GQ2.BoundaryMaps)
  (F : GQ2.BoundaryFrame H E)
  (R : GQ2.LocalReciprocity)
  (horient :
    GQ2.TameUnitOrientation R B.tameF)
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  {Y : Type} [Group Y]
  [TopologicalSpace Y]
  [DiscreteTopology Y] [Finite Y]
  (T : GQ2.MarkedTarget H E Y)
  (hE2 : ∀ (e : E), e ^ 2 = 1) :
  GQ2.exactImageCount S.b F T =
    GQ2.exactImageCount B.bF F T

**Theorem 4.2 over an abstract source** (the SourceData refactor): for every
`S : SourceData`, every boundary frame, and every boundary-framed marked target `𝒴`, the
exact-image lift counts of `S` and `G_ℚ₂` agree: `e^β_S(𝒴) = e^β_{G_ℚ₂}(𝒴)`.  The `Γ_A`
capstone `thm_4_2` below is this statement at `B.sourceA` (definitionally: `B.sourceA.b`
**is** `B.bA`); R32 instantiates it at `sourceR` with zero further refactoring.  Same
strong-induction skeleton as `thm_4_2`, with the terminal lane through
`terminal_count_eq_of_sources`.

theoremdefined in GQ2/Roe/DualityAssembly.lean

complete

theorem GQ2.FoxH.prop_5_15_R.{u_1, u_2} {C : Type u_1} [Group C] [Finite C]
  {A : Type u_2} [AddCommGroup A] [Finite A] [DistribMulAction C A]
  (t : GQ2.Marking C) (ht : t.TameRel) (hw : t.WildRelR)
  (hgen : t.Generates) (hA₂ : ∀ (a : A), a + a = 0)
  (hcore : t.Pro2Core) : GQ2.FoxH.IsSelfDual_R t A

theorem GQ2.FoxH.prop_5_15_R.{u_1, u_2}
  {C : Type u_1} [Group C] [Finite C]
  {A : Type u_2} [AddCommGroup A]
  [Finite A] [DistribMulAction C A]
  (t : GQ2.Marking C) (ht : t.TameRel)
  (hw : t.WildRelR) (hgen : t.Generates)
  (hA₂ : ∀ (a : A), a + a = 0)
  (hcore : t.Pro2Core) :
  GQ2.FoxH.IsSelfDual_R t A

**⟦prop:duality⟧ (Candidate deformation duality), word half:** the Roe word complex is
self-dual for every finite elementary module — packaged: the display-(56) numerics hold on the
`r_R` complex and the descended `B_R`-pairing is perfect.

The composition: the dévissage strong induction `prop_5_15_of_simple_R`
(`GQ2/Roe/DevissageInduction.lean`, via `lemma_5_11_R` along `0 → W → A → A/W → 0` for a proper
`C`-stable `W`) reduces to the simple case, which `selfDual_of_simple_R` closes by the
`tau_split_or_ramified` dichotomy — split (`split_shapes_of_wild_R` + the tame
representation-theory providers) or ramified (`lemma_5_13_ramified_R` + `hTodd` derived + the
unipotent pairing operator).  `Γ_R` twin of `GQ2.FoxH.prop_5_15`.

defdefined in GQ2/Roe/Gauss.lean

complete

def GQ2.FoxH.QZeroR.{u_1, u_2} {C : Type u_1} [Group C] {V : Type u_2}
  [AddCommGroup V] [DistribMulAction C V] (q : V → ZMod 2) (U : C)
  (d : V) : ZMod 2

def GQ2.FoxH.QZeroR.{u_1, u_2} {C : Type u_1}
  [Group C] {V : Type u_2}
  [AddCommGroup V] [DistribMulAction C V]
  (q : V → ZMod 2) (U : C) (d : V) :
  ZMod 2

**The Roe base determinant form** `Q_R⁰` (⟦eq:QR⟧, ramified two-term shape): on the normalized
`x₁`-supported class, the diagonal `q(d)` (from `x₁²`, R24's `heisMarking_x1_sq_z`) plus the
symplectic `b_q(d, U⁻¹d) = polar q d (U⁻¹•d)` (from `cR = [x₁, x₁^{σ₂}]`, R24's `heisMarking_cR_z`),
`U = σ₂`.  This is the exact `Γ_A` base form `κ_q⁰` (`SectionSix` §6.2) with the wild coordinate
renamed `c ↦ d`.

Proof for Proposition 12.3

Proof uses 3

Proof dependency previews

Preview

Proposition 4.2

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §C of the paper. Ingredients: Corollary 7.12 Proposition 12.8 Proposition 4.2.

Lemma12.4

Group: The square-commutator presentation (10)

Group member previews

Preview

Definition 12.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Lemma C.8 of the paper (Pro-2 quotient of the square-commutator candidate).

The maximal pro-2 quotient of \Gamma_R is

D_R=\angles{s,x,y\;\middle|\;(x^s)^{-1}x^{-3}y^2[y,y^s]}_{\mathrm{pro}-2},

where s,x,y are the images of \sigma,x_0,x_1.

Lean code for Lemma12.4●1 definition

defdefined in GQ2/Roe/MaxPro2Bridge.lean

complete

def GQ2.maxPro2Bridge :
  ↑(GQ2.maxProPQuotient 2
            (↑(GQ2.FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸
              GQ2.NR)).toProfinite.toTop ≃ₜ*
    ↑GQ2.DR.toProfinite.toTop

def GQ2.maxPro2Bridge :
  ↑(GQ2.maxProPQuotient 2
            (↑(GQ2.FreeProfiniteGroup
                      (Fin
                        4)).toProfinite.toTop ⧸
              GQ2.NR)).toProfinite.toTop ≃ₜ*
    ↑GQ2.DR.toProfinite.toTop

**The maximal pro-2 quotient of `Γ_R` is `D_R`** ⟦lem:pro2word⟧ (the `Γ_R` half of the note's
Lemma 3.1): a continuous isomorphism `Γ_R(2) ≅ D_R` matching the marked generators
`σ ↦ s, τ ↦ 1, x₀ ↦ x, x₁ ↦ y`.  Roe counterpart of `GQ2.SectionThree.maxAEquiv`; the pro-2 leg of
the boundary bundle that R15's `markedPro2_R` and R32 consume.

Proof for Lemma 12.4

uses 1

Proved in §C of the paper. Ingredients: Lemma 4.1.

Lemma12.5

Group: The square-commutator presentation (10)

Group member previews

Preview

Definition 12.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Lemma C.9 of the paper (Demushkin invariants of D_R).

D_R is a Demushkin pro-2 group of rank 3 with q(D_R)=2. In the basis of H^1(D_R,\F_2) dual to (s,x,y), the Gram matrix of the cup–Bockstein form is

\begin{pmatrix}0&1&0\\1&0&0\\0&0&1\end{pmatrix},

which is nonsingular.

Lean code for Lemma12.5●3 theorems

theoremdefined in GQ2/Roe/DRDemushkin.lean

complete

theorem GQ2.isDemushkin_DR : GQ2.IsDemushkin 2 ↑GQ2.DR.toProfinite.toTop

theorem GQ2.isDemushkin_DR :
  GQ2.IsDemushkin 2
    ↑GQ2.DR.toProfinite.toTop

**`D_R` is a Demushkin pro-2 group** ⟦lem:initial⟧ — "this is exactly the defining
cohomological condition".  The first load-bearing use of the abstract `IsDemushkin` predicate.
Nondegeneracy fill (R13, after the Gram entries): a class `a·s* + b·x* + c·y*` cups with `x*`
to `a`, with `s*` to `b`, and with `y*` to `c` — the matrix `[[0,1,0],[1,0,0],[0,0,1]]` is
nonsingular — using `drH1_bijective` to write an arbitrary nonzero class in coordinates.

theoremdefined in GQ2/Roe/DRDemushkin.lean

complete

theorem GQ2.demushkinRank_DR : GQ2.demushkinRank 2 ↑GQ2.DR.toProfinite.toTop = 3

theorem GQ2.demushkinRank_DR :
  GQ2.demushkinRank 2
      ↑GQ2.DR.toProfinite.toTop =
    3

**`D_R` has Demushkin rank 3** ⟦lem:initial⟧ (`8 = 2³`; proved from `card_H1_DR`).

theoremdefined in GQ2/Roe/DRDemushkin.lean

complete

theorem GQ2.demushkinQ_DR : GQ2.demushkinQ ↑GQ2.DR.toProfinite.toTop = 2

theorem GQ2.demushkinQ_DR :
  GQ2.demushkinQ
      ↑GQ2.DR.toProfinite.toTop =
    2

**`D_R` has `q`-invariant 2** ⟦eq:BR⟧/⟦eq:BRsplit⟧ (note (3.4)–(3.6)): the topological
abelianization is `B_R = ⟨s̄, x̄, ȳ | −4x̄ + 2ȳ = 0⟩ = C₂·t ⊕ ℤ₂·s̄ ⊕ ℤ₂·x̄` with
`t = ȳ − 2x̄`, whose torsion subgroup has order 2.  Fill: from ticket R8's `BRDecomposition`
(the `BDecomposition` clone; see the R7 design memo §R8).

Proposition12.6

Group: The square-commutator presentation (10)

Group member previews

Preview

Definition 12.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Proposition C.10 of the paper (The orientation of D_R).

D_R carries a unique continuous character \chi_R:D_R\to\mathbb{Z}_2^\times describing its action on the dualizing module. Its values on the generators are

\chi_R(s)=S,\qquad \chi_R(x)=X,\qquad \chi_R(y)=Y=-X^2,

where X\in\mathbb{Z}_2 is the unique root of Z^3+2Z^2+1 with X\equiv1\pmod2, and S=-X^3/(X^2+X+1); numerically X\equiv5 and S\equiv13\pmod{16}. Moreover \chi_R is surjective, with image \{\pm1\}\times(1+4\mathbb{Z}_2)=\mathbb{Z}_2^\times.

Lean code for Proposition12.6●3 declarations

defdefined in GQ2/Roe/ChiR.lean

complete

def GQ2.Roe.chiR : ↑GQ2.DR.toProfinite.toTop →ₜ* ℤ_[2]ˣ

def GQ2.Roe.chiR :
  ↑GQ2.DR.toProfinite.toTop →ₜ* ℤ_[2]ˣ

**The canonical orientation `χ_R : D_R → ℤ₂ˣ`** ⟦prop:orientation⟧, built by the
universal property of `D_R` (`drLiftHom`) at the triple
`(S, X, Y) = (SvalUnit, rootXUnit, YvalUnit)`.  The relator `r₂` dies because `ℤ₂ˣ` is
abelian: `drWord` collapses to `(X⁴)⁻¹Y²` (`drWord_comm`) and `Y² = X⁴` (`YvalUnit_sq_eq`).

theoremdefined in GQ2/Roe/ChiR.lean

complete

theorem GQ2.Roe.isLabuteOrientation_chiR :
  GQ2.IsLabuteOrientation GQ2.Roe.chiR.toMonoidHom

theorem GQ2.Roe.isLabuteOrientation_chiR :
  GQ2.IsLabuteOrientation
    GQ2.Roe.chiR.toMonoidHom

**`χ_R` is Labute's canonical orientation** ⟦prop:orientation⟧: its generator values
`(S, X, Y)` form a Labute orientation datum.  Discharged from `isLabuteOrientationDatum_of_root`
with R10's cubic root facts.

theoremdefined in GQ2/Roe/ChiR.lean

complete

theorem GQ2.Roe.chiR_surjective : Function.Surjective ⇑GQ2.Roe.chiR

theorem GQ2.Roe.chiR_surjective :
  Function.Surjective ⇑GQ2.Roe.chiR

**Surjectivity of `χ_R`** ⟦prop:orientation⟧, the image statement `im χ_R = ℤ₂ˣ`.
Because every `2`-adic unit is `≡ ±1 (mod 4)`, the note's `{±1}×(1+4ℤ₂)` is all of `ℤ₂ˣ`,
so this is the same encoding as B3c's `surjective_chiTwo`.

Proof by the pro-`2` Burnside/Frattini criterion (`surjective_of_forall_not_le_index_p`):
fix an index-`2` open normal `M ≤ ℤ₂ˣ`.  Its quotient has order `2`, so `M` contains every
square.  The range of `χ_R` contains `χ_R(x) = X` and `χ_R(y·x⁻²) = -1`; if `M` also
contained the range then, by `mod8_sq` (every unit is `s·w²` with `s ∈ {1,-1,±(-3)}` and
`-3 ≡ 5 ≡ X (mod 8)` is `X` times a square), `M` would be all of `ℤ₂ˣ`, contradicting
index `2`.

Proposition12.7

Group: The square-commutator presentation (10)

Group member previews

Preview

Definition 12.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Proposition C.11 of the paper (Demushkin classification at rank 3 and q=2).

Let D be a Demushkin pro-2 group of rank 3 with q(D)=2, carrying a continuous surjective character \chi:D\to\mathbb{Z}_2^\times that is an orientation of D. Then D\cong D_0 as topological groups.

Lean code for Proposition12.7●4 declarations

defdefined in GQ2/Roe/MarkedPro2.lean

complete

def GQ2.BLabHypothesis : Prop

def GQ2.BLabHypothesis : Prop

**B-Lab (hypothesis form — never an axiom: proved as `GQ2.Roe.Labute.bLab`).**

Labute's classification of Demushkin groups of odd rank with `q = 2`
([Labute], *Classification of Demushkin groups*, Canad. J. Math. **19** (1967), Théorème 4
(uniqueness and image classification of the canonical orientation in the `q = 2` case) and
Théorème 8 (the classification by `(rank, q, im χ)`); note Cor. 3.4 ⟦cor:abstractD0⟧),
specialized to **the single instance consumed by the Roe verification**:

> a pro-2 group that is Demushkin of rank `3` with `q = 2`, and whose canonical orientation —
> characterized à la Labute by the descent of crossed derivations through the relation
> (`IsLabuteOrientation`) — is surjective onto `ℤ₂ˣ = {±1} × (1 + 4ℤ₂)` (the secondary depth
> `f = 2`), is continuously isomorphic to `D₀ = ⟨A, S, Y | A²S⁴[S,Y]⟩_pro-2`.

Conventions (per the ground rules of `docs/orchestration/formalization-plan.md`):
* `IsDemushkin`/`demushkinRank`/`demushkinQ` are the repo's `Nat.card`-encoded predicates
  (`GQ2/Demushkin.lean`; rank 3 ⟺ `#H¹ = 8`, `q = 2` ⟺ torsion count 2 in the topological
  abelianization).
* The orientation clause is stated against the **descent characterization**
  (`GQ2/Roe/CrossedDerivation.lean`), which is Labute's own definition of the canonical
  orientation for the presented group — *not* the deferred abstract dualizing-module route
  (the `GQ2/Orientation.lean` deviation note); `Continuous χ` is carried separately per the
  `ℤ₂ˣ`-character house style.
* The image invariant `{±1} × (1 + 4ℤ₂)` is the **full** unit group `ℤ₂ˣ` (the `f = 2` case),
  so it is encoded as `Function.Surjective χ` — the same encoding as B3c's
  `DyadicOrientation.surjective_chiTwo`.
* Specializing to `G := D_R` (rather than quantifying over abstract `G`) is deliberate: it
  quarantines exactly the instance used, and the descent-characterized orientation is
  concretely available for `D_R` through its presentation.  See the R7 design memo for the
  abstract-`G` alternative and its cost.

All four antecedents are discharged by R10–R13 (`isDemushkin_DR`, `demushkinRank_DR`,
`demushkinQ_DR`, and R11's `χ_R`), so consuming code applies this to obtain the abstract
isomorphism of the note's Cor. 3.4.

theoremdefined in GQ2/Roe/Labute/Assembly.lean

complete

theorem GQ2.Roe.Labute.bLab : GQ2.BLabHypothesis

theorem GQ2.Roe.Labute.bLab : GQ2.BLabHypothesis

**The B-Lab classification instance, as a theorem** — the L-campaign deliverable
(plan §1: the exact interface of `GQ2/Roe/MarkedPro2.lean` `section Draft`, verbatim).

The proof is **complete here** modulo the upstream skeleton sorries: the four antecedents
are discarded (the pinned orientation data enters through the levelwise χ-clauses instead
— plan §1), the two epis come from the levelwise assembly above, and the endgame is
byte-for-byte the `reconstruction_of_equinum` endgame (`GQ2/Reconstruction.lean:350–354`):
`φ ∘ ψ : D_R ↠ D_R` is a continuous surjective endomorphism of a topologically f.g.
profinite group, hence injective (`profinite_hopfian`), so `ψ` is a continuous bijective
homomorphism, so a topological isomorphism (`continuousMulEquivOfBijective`).

theoremdefined in GQ2/Reconstruction.lean

complete

theorem GQ2.exists_contSurj_of_levelwise_nonempty {S R : Type} [Group S]
  [TopologicalSpace S] [IsTopologicalGroup S] [CompactSpace S]
  [TotallyDisconnectedSpace S] [Group R] [TopologicalSpace R]
  [IsTopologicalGroup R] [CompactSpace R] [TotallyDisconnectedSpace R]
  (hne :
    ∀ (U : OpenNormalSubgroup ↑(ProfiniteGrp.of R).toProfinite.toTop),
      Nonempty (GQ2.ContSurj S (R ⧸ ↑U.toOpenSubgroup)))
  (hfin :
    ∀ (U : OpenNormalSubgroup ↑(ProfiniteGrp.of R).toProfinite.toTop),
      Finite (GQ2.ContSurj S (R ⧸ ↑U.toOpenSubgroup))) :
  Nonempty (GQ2.ContSurj S R)

theorem GQ2.exists_contSurj_of_levelwise_nonempty
  {S R : Type} [Group S]
  [TopologicalSpace S]
  [IsTopologicalGroup S] [CompactSpace S]
  [TotallyDisconnectedSpace S] [Group R]
  [TopologicalSpace R]
  [IsTopologicalGroup R] [CompactSpace R]
  [TotallyDisconnectedSpace R]
  (hne :
    ∀
      (U :
        OpenNormalSubgroup
          ↑(ProfiniteGrp.of
                  R).toProfinite.toTop),
      Nonempty
        (GQ2.ContSurj S
          (R ⧸ ↑U.toOpenSubgroup)))
  (hfin :
    ∀
      (U :
        OpenNormalSubgroup
          ↑(ProfiniteGrp.of
                  R).toProfinite.toTop),
      Finite
        (GQ2.ContSurj S
          (R ⧸ ↑U.toOpenSubgroup))) :
  Nonempty (GQ2.ContSurj S R)

**Surjection assembly from levelwise nonemptiness** (the compactness core of
`exists_contSurj_of_card_le`, isolated): if `S` continuously surjects onto every finite quotient
`R ⧸ U` of `R` in at least one (`hne`) and at most finitely many (`hfin`) ways, then `S`
continuously surjects onto `R`.

This is `exists_contSurj_of_card_le` with the two `konigFunctor`-level inputs taken as hypotheses
instead of being derived from surjection counts; that lemma is now the special case in which
`contSurj_quotient_nonempty_finite` supplies them.  Consumers that produce the level sets by
other means (the Labute assembly, `GQ2/Roe/Labute/Assembly.lean`) apply this form directly.

Proof: `hne`/`hfin` make `konigFunctor : OpenNormalSubgroup R ⥤ Type` a cofiltered system of
nonempty finite sets, so `nonempty_sections_of_finite_cofiltered_system` (König) supplies a
compatible family `σ U : S ↠ R/U`.  `R` embeds into `Q := ∏_U R/U` via `e = (mk_U)_U` (injective
since the open normal subgroups meet in `1`; a closed embedding as `R` is compact and `Q` is
Hausdorff).  Cantor's intersection theorem in the compact `R` realizes each compatible family
`(σ U s)_U` as `e r`, so `ψ := e⁻¹ ∘ Φ` (`Φ = (σ U)_U`) is a continuous homomorphism with
`mk_U ∘ ψ = σ U`; a second Cantor intersection, in the compact `S`, shows `ψ` surjective.

theoremdefined in GQ2/Reconstruction.lean

complete

theorem GQ2.profinite_hopfian.{u_1} {P : Type u_1} [Group P]
  [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P]
  [TotallyDisconnectedSpace P]
  (hPfg : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (φ : P →ₜ* P) (hφ : Function.Surjective ⇑φ) : Function.Injective ⇑φ

theorem GQ2.profinite_hopfian.{u_1} {P : Type u_1}
  [Group P] [TopologicalSpace P]
  [IsTopologicalGroup P] [CompactSpace P]
  [TotallyDisconnectedSpace P]
  (hPfg :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (φ : P →ₜ* P)
  (hφ : Function.Surjective ⇑φ) :
  Function.Injective ⇑φ

**Profinite Hopfian property** (paper Lemma 2.5, key input): a continuous surjective
endomorphism of a *topologically finitely generated* profinite group is injective.  Non-standard;
absent from Mathlib.  Proof idea: a topologically f.g. profinite group has only finitely many open
subgroups of each index, so a surjective endomorphism acts as a surjection — hence a bijection — on
each finite quotient level, forcing injectivity in the limit.

Proof for Proposition 12.7

uses 1

Proved in §C of the paper. Ingredients: Lemma 12.11.

Proposition12.8

Group: The square-commutator presentation (10)

Group member previews

Preview

Definition 12.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Proposition C.12 of the paper (Marked identification of the pro-2 quotient).

Let \nu_R:D_R\twoheadrightarrow\mathbb{Z}_2 be defined by \nu_R(s)=1 and \nu_R(x)=\nu_R(y)=0. Then the marked pairs (G_{\Qtwo}(2),\nu_{\mathrm{ur}}) and (D_R,\nu_R) are isomorphic.

Lean code for Proposition12.8●1 theorem

theoremdefined in GQ2/Roe/MarkedPro2.lean

complete

theorem GQ2.markedPro2_R [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] (R : GQ2.LocalReciprocity)
  (hBLab : GQ2.BLabHypothesis) :
  ∃ ι,
    ι GQ2.ztwoOne = Multiplicative.ofAdd ↑1 ∧
      ∃ e,
        ∀ (g : GQ2.AbsGalQ2),
          R.nu_ur (GQ2.toAb g) =
            ι (GQ2.nuDR (e ((GQ2.maxProPMk 2 GQ2.AbsGalQ2) g)))

theorem GQ2.markedPro2_R
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (R : GQ2.LocalReciprocity)
  (hBLab : GQ2.BLabHypothesis) :
  ∃ ι,
    ι GQ2.ztwoOne =
        Multiplicative.ofAdd ↑1 ∧
      ∃ e,
        ∀ (g : GQ2.AbsGalQ2),
          R.nu_ur (GQ2.toAb g) =
            ι
              (GQ2.nuDR
                (e
                  ((GQ2.maxProPMk 2
                      GQ2.AbsGalQ2)
                    g)))

**The marked pro-2 identification** ⟦prop:markedpro2⟧ (note Prop. 3.6), in the marked
vocabulary of `prop_3_10_local_marked` (`GQ2/SectionThreeMarked.lean:60`), which the
boundary-frame layer consumes: given the B-Lab hypothesis, there is a continuous isomorphism
`e : G_{ℚ₂}(2) ≅ D_R` matching the unramified markings — the `ℤ₂`-identification `ι` between
the two `ν`-targets is quantified explicitly and pinned by `ι(1) = ofAdd 1`, and the
`ν_ur`-values are read through arbitrary lifts, as in `prop_1_1`.

Fill (R15): the three-step route of the module docstring — B-Lab abstract isomorphism,
`φ_ab`-correction via `prop_3_8_classification`/`prop_3_8_lift` (both on the `D₀` side, reused
as-is), and the `prop_1_1`/`prop_3_10_local_marked` assembly pattern for the `ι`-bridge.

Proof for Proposition 12.8

Proof uses 4

Proof dependency previews

Preview

Proposition 2.1

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §C of the paper. Ingredients: Lemma 12.5 Proposition 12.7 Proposition 2.1 Proposition 12.6.

Definition12.9

Group: The square-commutator presentation (10)

Group member previews

Preview

Definition 12.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Definition C.13 of the paper (Defect and defect homomorphism).

Let k\ge3, let D be the group in which we work, and let T be a triple of elements of Q_k that generates Q_k and at which the tested relator evaluates to 1. Lift T to Q_{k+1} and evaluate the relator there; the result lies in Z_k and is independent of the lift, because all three exponent sums of each relator are even. Call it the defect \delta_k(T)\in Z_k. Modifying T slotwise by w\in(\lambda_{k-1})^3 preserves both clauses and shifts the defect by the defect homomorphism, given in additive notation on Z_k by

\bar d_k(w_1,w_2,w_3)=w_1^2+[w_1,A]+[w_2,Y]+[w_3,S]

for r_0, and by

\bar d_k(u,v,w)=w^2+[w,y]+[u,x]+[v,s]

for r_2.

Lean code for Definition12.9●3 definitions

defdefined in GQ2/Roe/Labute/TwoCentralTower.lean

complete

def GQ2.Roe.Labute.twoCentralSeries.{u_1} (G : Type u_1) [Group G]
  [TopologicalSpace G] [IsTopologicalGroup G] : ℕ → Subgroup G

def GQ2.Roe.Labute.twoCentralSeries.{u_1}
  (G : Type u_1) [Group G]
  [TopologicalSpace G]
  [IsTopologicalGroup G] : ℕ → Subgroup G

The **lower 2-central series** `λₖ` of `G`, 1-based as in the memos:
`λ₁ = G`, `λ_{k+1} = cl(λₖ²[λₖ, G])` (`twoCentralSucc`).  Index `0` is a junk value
(`λ₀ := ⊤ = λ₁`); the recursion genuinely starts at `k = 1`, so `twoCentralSeries_succ`
below carries the hypothesis `1 ≤ k`.

defdefined in GQ2/Roe/Labute/Levelwise.lean

complete

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

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

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

defdefined in GQ2/Roe/Labute/SpanFoundation.lean

complete

def GQ2.Roe.Labute.dbarWordR2.{u_1} {G : Type u_1} [Group G] (s x y : G)
  (w : Fin 3 → G) : G

def GQ2.Roe.Labute.dbarWordR2.{u_1}
  {G : Type u_1} [Group G] (s x y : G)
  (w : Fin 3 → G) : G

The **`r₂`-side defect-shift word** `d̄(u,v,w) = w²·[w,y]·[u,x]·[v,s]` at the triple
`(s, x, y)` (spike §2.2 — note the r₂-tails/cross-terms pair `(u,x), (v,s)`, *not* the
draft's `(x, y)` pairing).

Theorem12.10

Group: The square-commutator presentation (10)

Group member previews

Preview

Definition 12.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Theorem C.15 of the paper (Span theorem).

Let F be the free pro-2 group on three generators, filtered by (206), and let \bar d_k be either (207) or (208) evaluated at the generators. For every k\ge3,

Z_k(F)=\im\bar d_k +\angles{g_i^{2^{k-1}},\,g_j^{2^{k-1}}},

where g_i,g_j are the two untwisted generators: S,Y for r_0 and s,x for r_2. The corresponding power of the twisted generator already lies in \im\bar d_k. The same identity holds in Z_k(D) for any quotient D of F and any generating triple, because the filtration (206) is verbal.

Lean code for Theorem12.10●3 theorems

theoremdefined in GQ2/Roe/Labute/StageLemma/Defect.lean

complete

theorem GQ2.Roe.Labute.span_free_r0 (k : ℕ) (hk : 3 ≤ k) :
  GQ2.Roe.Labute.zLayer (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
      k ≤
    Subgroup.closure
      ((fun w =>
            GQ2.Roe.Labute.dbarWordR0
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen 0))
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen 1))
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen 2))
              w) ''
          {w |
            ∀ (i : Fin 3),
              w i ∈
                GQ2.Roe.Labute.lambdaImage
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop) (k - 1)
                  (k + 1)} ∪
        {(GQ2.Roe.Labute.levelMk
                (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop) (k + 1))
              (GQ2.Roe.Labute.freeGen 1) ^
            2 ^ (k - 1),
          (GQ2.Roe.Labute.levelMk
                (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop) (k + 1))
              (GQ2.Roe.Labute.freeGen 2) ^
            2 ^ (k - 1)})

theorem GQ2.Roe.Labute.span_free_r0 (k : ℕ)
  (hk : 3 ≤ k) :
  GQ2.Roe.Labute.zLayer
      (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
      k ≤
    Subgroup.closure
      ((fun w =>
            GQ2.Roe.Labute.dbarWordR0
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen
                  0))
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen
                  1))
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen
                  2))
              w) ''
          {w |
            ∀ (i : Fin 3),
              w i ∈
                GQ2.Roe.Labute.lambdaImage
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k - 1) (k + 1)} ∪
        {(GQ2.Roe.Labute.levelMk
                (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                (k + 1))
              (GQ2.Roe.Labute.freeGen 1) ^
            2 ^ (k - 1),
          (GQ2.Roe.Labute.levelMk
                (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                (k + 1))
              (GQ2.Roe.Labute.freeGen 2) ^
            2 ^ (k - 1)})

**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).

theoremdefined in GQ2/Roe/Labute/StageLemma/Defect.lean

complete

theorem GQ2.Roe.Labute.span_free_r2 (k : ℕ) (hk : 3 ≤ k) :
  GQ2.Roe.Labute.zLayer (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
      k ≤
    Subgroup.closure
      ((fun w =>
            GQ2.Roe.Labute.dbarWordR2
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen 0))
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen 1))
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen 2))
              w) ''
          {w |
            ∀ (i : Fin 3),
              w i ∈
                GQ2.Roe.Labute.lambdaImage
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop) (k - 1)
                  (k + 1)} ∪
        {(GQ2.Roe.Labute.levelMk
                (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop) (k + 1))
              (GQ2.Roe.Labute.freeGen 0) ^
            2 ^ (k - 1),
          (GQ2.Roe.Labute.levelMk
                (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop) (k + 1))
              (GQ2.Roe.Labute.freeGen 1) ^
            2 ^ (k - 1)})

theorem GQ2.Roe.Labute.span_free_r2 (k : ℕ)
  (hk : 3 ≤ k) :
  GQ2.Roe.Labute.zLayer
      (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
      k ≤
    Subgroup.closure
      ((fun w =>
            GQ2.Roe.Labute.dbarWordR2
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen
                  0))
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen
                  1))
              ((GQ2.Roe.Labute.levelMk
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k + 1))
                (GQ2.Roe.Labute.freeGen
                  2))
              w) ''
          {w |
            ∀ (i : Fin 3),
              w i ∈
                GQ2.Roe.Labute.lambdaImage
                  (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                  (k - 1) (k + 1)} ∪
        {(GQ2.Roe.Labute.levelMk
                (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                (k + 1))
              (GQ2.Roe.Labute.freeGen 0) ^
            2 ^ (k - 1),
          (GQ2.Roe.Labute.levelMk
                (↑GQ2.Roe.Labute.freeProTwo.toProfinite.toTop)
                (k + 1))
              (GQ2.Roe.Labute.freeGen 1) ^
            2 ^ (k - 1)})

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.

theoremdefined in GQ2/Roe/Labute/StageLemma/Defect.lean

complete

theorem GQ2.Roe.Labute.span_descent_r2 (k : ℕ) (hk : 3 ≤ k)
  (T' :
    Fin 3 →
      GQ2.Roe.Labute.levelQuot (↑GQ2.D0.toProfinite.toTop) (k + 1))
  (hgen : Subgroup.closure (Set.range T') = ⊤) :
  GQ2.Roe.Labute.zLayer (↑GQ2.D0.toProfinite.toTop) k ≤
    Subgroup.closure
      ((fun w => GQ2.Roe.Labute.dbarWordR2 (T' 0) (T' 1) (T' 2) w) ''
          {w |
            ∀ (i : Fin 3),
              w i ∈
                GQ2.Roe.Labute.lambdaImage (↑GQ2.D0.toProfinite.toTop)
                  (k - 1) (k + 1)} ∪
        {T' 0 ^ 2 ^ (k - 1), T' 1 ^ 2 ^ (k - 1)})

theorem GQ2.Roe.Labute.span_descent_r2 (k : ℕ)
  (hk : 3 ≤ k)
  (T' :
    Fin 3 →
      GQ2.Roe.Labute.levelQuot
        (↑GQ2.D0.toProfinite.toTop)
        (k + 1))
  (hgen :
    Subgroup.closure (Set.range T') = ⊤) :
  GQ2.Roe.Labute.zLayer
      (↑GQ2.D0.toProfinite.toTop) k ≤
    Subgroup.closure
      ((fun w =>
            GQ2.Roe.Labute.dbarWordR2
              (T' 0) (T' 1) (T' 2) w) ''
          {w |
            ∀ (i : Fin 3),
              w i ∈
                GQ2.Roe.Labute.lambdaImage
                  (↑GQ2.D0.toProfinite.toTop)
                  (k - 1) (k + 1)} ∪
        {T' 0 ^ 2 ^ (k - 1),
          T' 1 ^ 2 ^ (k - 1)})

Span descent, direction 2 (tails at the `(s, x)`-slots).  Fill: L4b.

Lemma12.11

Group: The square-commutator presentation (10)

Group member previews

Preview

Definition 12.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Lemma C.17 of the paper (Stage lemma).

Let k\ge3 and T\in S_k. Then

reachability: \delta_k(T)\in\im\bar d_k;
digit adjustment: the map from \ker\bar d_k to (\mathbb{Z}/2)^2 recording the two fresh orientation digits of the corrected triple is surjective.

Consequently some modification of T lifts into S_{k+1}, and S_k\neq\emptyset for every k\ge3.

Lean code for Lemma12.11●4 declarations

theoremdefined in GQ2/Roe/Labute/StageLemma/StageOne.lean

complete

theorem GQ2.Roe.Labute.stageSL1R2 (k : ℕ) (hk : 3 ≤ k)
  {T : Fin 3 → GQ2.Roe.Labute.levelQuot (↑GQ2.D0.toProfinite.toTop) k}
  (hT : T ∈ GQ2.Roe.Labute.sPR2 k) :
  ∃ w,
    (∀ (i : Fin 3),
        w i ∈
          GQ2.Roe.Labute.lambdaImage (↑GQ2.D0.toProfinite.toTop) (k - 1)
            (k + 1)) ∧
      GQ2.Roe.Labute.dbarWordR2
          (GQ2.Roe.Labute.canonLift (↑GQ2.D0.toProfinite.toTop) k (T 0))
          (GQ2.Roe.Labute.canonLift (↑GQ2.D0.toProfinite.toTop) k (T 1))
          (GQ2.Roe.Labute.canonLift (↑GQ2.D0.toProfinite.toTop) k (T 2))
          w =
        (GQ2.Roe.Labute.defectR2 k T)⁻¹

theorem GQ2.Roe.Labute.stageSL1R2 (k : ℕ)
  (hk : 3 ≤ k)
  {T :
    Fin 3 →
      GQ2.Roe.Labute.levelQuot
        (↑GQ2.D0.toProfinite.toTop) k}
  (hT : T ∈ GQ2.Roe.Labute.sPR2 k) :
  ∃ w,
    (∀ (i : Fin 3),
        w i ∈
          GQ2.Roe.Labute.lambdaImage
            (↑GQ2.D0.toProfinite.toTop)
            (k - 1) (k + 1)) ∧
      GQ2.Roe.Labute.dbarWordR2
          (GQ2.Roe.Labute.canonLift
            (↑GQ2.D0.toProfinite.toTop) k
            (T 0))
          (GQ2.Roe.Labute.canonLift
            (↑GQ2.D0.toProfinite.toTop) k
            (T 1))
          (GQ2.Roe.Labute.canonLift
            (↑GQ2.D0.toProfinite.toTop) k
            (T 2))
          w =
        (GQ2.Roe.Labute.defectR2 k T)⁻¹

SL1 (reachability), direction 2.  Fill: L4b.

theoremdefined in GQ2/Roe/Labute/StageLemma/StageTwo.lean

complete

theorem GQ2.Roe.Labute.stageSL2R2 (k : ℕ) (hk : 3 ≤ k)
  {T : Fin 3 → GQ2.Roe.Labute.levelQuot (↑GQ2.D0.toProfinite.toTop) k}
  (hT : T ∈ GQ2.Roe.Labute.sPR2 k)
  (hδ : GQ2.Roe.Labute.defectR2 k T = 1) :
  ∃ w,
    (∀ (i : Fin 3),
        w i ∈
          GQ2.Roe.Labute.lambdaImage (↑GQ2.D0.toProfinite.toTop) (k - 1)
            (k + 1)) ∧
      GQ2.Roe.Labute.dbarWordR2
            (GQ2.Roe.Labute.canonLift (↑GQ2.D0.toProfinite.toTop) k
              (T 0))
            (GQ2.Roe.Labute.canonLift (↑GQ2.D0.toProfinite.toTop) k
              (T 1))
            (GQ2.Roe.Labute.canonLift (↑GQ2.D0.toProfinite.toTop) k
              (T 2))
            w =
          1 ∧
        (fun i =>
            GQ2.Roe.Labute.canonLift (↑GQ2.D0.toProfinite.toTop) k
                (T i) *
              w i) ∈
          GQ2.Roe.Labute.sPR2 (k + 1)

theorem GQ2.Roe.Labute.stageSL2R2 (k : ℕ)
  (hk : 3 ≤ k)
  {T :
    Fin 3 →
      GQ2.Roe.Labute.levelQuot
        (↑GQ2.D0.toProfinite.toTop) k}
  (hT : T ∈ GQ2.Roe.Labute.sPR2 k)
  (hδ : GQ2.Roe.Labute.defectR2 k T = 1) :
  ∃ w,
    (∀ (i : Fin 3),
        w i ∈
          GQ2.Roe.Labute.lambdaImage
            (↑GQ2.D0.toProfinite.toTop)
            (k - 1) (k + 1)) ∧
      GQ2.Roe.Labute.dbarWordR2
            (GQ2.Roe.Labute.canonLift
              (↑GQ2.D0.toProfinite.toTop)
              k (T 0))
            (GQ2.Roe.Labute.canonLift
              (↑GQ2.D0.toProfinite.toTop)
              k (T 1))
            (GQ2.Roe.Labute.canonLift
              (↑GQ2.D0.toProfinite.toTop)
              k (T 2))
            w =
          1 ∧
        (fun i =>
            GQ2.Roe.Labute.canonLift
                (↑GQ2.D0.toProfinite.toTop)
                k (T i) *
              w i) ∈
          GQ2.Roe.Labute.sPR2 (k + 1)

SL2 (digit adjustment), direction 2.  Fill: L4a.

theoremdefined in GQ2/Roe/Labute/StageLemma/StageTwo.lean

complete

theorem GQ2.Roe.Labute.stageStepR2 (k : ℕ) (hk : 3 ≤ k)
  (h : (GQ2.Roe.Labute.sPR2 k).Nonempty) :
  (GQ2.Roe.Labute.sPR2 (k + 1)).Nonempty

theorem GQ2.Roe.Labute.stageStepR2 (k : ℕ)
  (hk : 3 ≤ k)
  (h : (GQ2.Roe.Labute.sPR2 k).Nonempty) :
  (GQ2.Roe.Labute.sPR2 (k + 1)).Nonempty

The stage step, direction 2 (proved from the frozen statements; composability
certificate).

defdefined in GQ2/Roe/Labute/Levelwise.lean

complete

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

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

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

Proof for Lemma 12.11

uses 1

Proved in §C of the paper. Ingredients: Theorem 12.10.