Documentation

GQ2.Roe.Main

The Γ_R assembly: sourceR, eq. (154), and the Replacement theorem (R32) #

The R-campaign capstone file: the Roe candidate Γ_R (note Definition 1.1 ⟦def:GammaR⟧) is plugged into the two-source machine as a GQ2.SourceData instance, and the note's ⟦thm:main⟧ (Replacement theorem, Γ_R ≅ G_{ℚ₂}) is derived in the exact statement shape of the Γ_A capstones:

The B-Lab hypothesis (owner decision 2026-07-25: no new axiom; DISCHARGED 2026-07-26) #

Labute's classification instance (note Cor. 3.4 ⟦cor:abstractD0⟧) enters exactly once, as the explicit binder hBLab : BLabHypothesis threaded from R15's markedPro2_R (⟦prop:markedpro2⟧) — it is not an axiom. The L-campaign has since proved the instance (GQ2.Roe.Labute.bLab, GQ2/Roe/Labute/Assembly.lean, at the standard three axioms), so every hBLab argument discharges by the one-liner bLab; the unconditional corollary at the end of this file does exactly that. The hypothesis-parametrized forms are kept as the frozen statements the R-campaign gates audit. Everything else in this file is unconditional.

The pro-2 boundary coordinate (the construction this file adds) #

SourceData asks for pro2 : Γ_R → Π (Π = PiBd, eq. (20)) with ν-compatibility, joint surjectivity with the tame coordinate, and kernel = proPKernel 2 Γ_R. Unlike Γ_A — whose pro-2 quotient is Π with matching generators (Prop 3.10) — the pro-2 quotient of Γ_R is the differently presented D_R (⟦lem:pro2word⟧, R15a maxPro2Bridge), and its identification with Π is the abstract, ν-marked one of B-Lab. We therefore compose

pro2R := eA ∘ e⁻¹ ∘ maxPro2Bridge ∘ maxProPMk,

with e : G_{ℚ₂}(2) ≅ D_R from markedPro2_R (hBLab) and eA : G_{ℚ₂}(2) ≅ Π from prop_3_10_local_marked. Both come with ℤ₂-identifications ι pinned at the topological generator (ι(1) = ofAdd 1), so the two ν-composites agree (ztwoOne topologically generates Ztwo), which yields the ν-compatibility of pro2R with φ_R by density over the four marked generators (nuDR_maxPro2Bridge_comp). Joint surjectivity then follows from the generic fibred-product kit (SectionThree.fiberProductExists + hker_uniform), exactly as for boundaryMapsWitness.

Design finding (generator pinning). The SourceData fields pro2_sigma/x0/x1 pin pro2 to piSigma/piX0/piX1 at the structure's own generators. For Γ_R this is unsatisfiable at the honest generators gammaSigmaR/X0R/X1R: their pro2R-images are the eA∘e⁻¹-images of drS/drX/drY, and no continuous hom D_R → Π matches generators literally (the tuple (piSigma, piX0, piX1) satisfies the Π-relator, not the Roe relator). Since the eight pinning fields are consumed nowhere (they are interface documentation; thm_4_2_of_sources and all its lanes touch only b/tame/pro2/compat/surj/ ker_pro2/the action layer/the obligations), sourceR takes tau := gammaTauR (honest — τ dies pro-2) and marked-pinned choice elements sigmaMarkR/x0MarkR/x1MarkR obtained from joint surjectivity for the other three. The GaussZ obligations are unaffected: the R31g twins pin the tame coordinate at the honest generators (phiR_gammaSigma etc.), which sourceR supplies on the nose.

Import discipline #

Plain-import (non-module): this file sits atop the non-module §2/§8 stack (SourceData, SectionTenSources, PresentationLiteral, Roe/Prop23, Roe/Supply, Roe/MarkedPro2). Importing the module-style suppliers (Roe/Tame, Roe/MaxPro2Bridge, via Roe/MarkedPro2) is fine — the restriction is one-directional. sourceR cannot live in GQ2/SourceData.lean: GQ2/MStageCountGammaR.lean and GQ2/GaussZ/GammaRD.lean import GQ2.SourceData, so this file is a new leaf importing both sides.

Axioms: no new axiom, no sorry. The obligations are std-3 (R31a–g); the capstones inherit the Γ_A-mirror census of eq. (154) through the shared G_{ℚ₂}-side machinery, plus nothing — BLabHypothesis is a binder, not an axiom.

Numerical anchor (R5, GQ2/Roe/Sanity.lean + scripts/roe_sanity_counts.py) #

main_surjection_count_R + main_surjection_count' give admissibleCountR G = admissibleCount G for every finite G (admissibleCountR_eq_admissibleCount below). R5 verified exactly this agreement numerically, four ways (Lean word-level pins + two independent Python engines + the June LMFDB-verified counts): C₂ : 7, C₄ : 24, V₄ : 42, D₄ : 144, Q₈ : 144 — with the archive convention g^h = hgh⁻¹ reconciled to Lean's g⁻¹xg by the σ ↦ σ⁻¹ bijection.

Instances for the raw carrier Γ_R = F₄ ⧸ N_R #

As in GQ2/Roe/MaxPro2Bridge.lean: T2Space/TotallyDisconnectedSpace on the raw quotient are guarded by [IsClosed N_R], discharged once here via NR_isClosed.

source
theorem GQ2.instT2SpaceQuotientCarrierToTopTotallyDisconnectedSpaceToProfiniteFreeProfiniteGroupFinOfNatNatSubgroupNR_1 :
T2Space (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)
source
theorem GQ2.instTotallyDisconnectedSpaceQuotientCarrierToTopToProfiniteFreeProfiniteGroupFinOfNatNatSubgroupNR_1 :
TotallyDisconnectedSpace (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)

ℤ̂/Z₂ glue: ztwoOne topologically generates, so pinned ιs agree #

source
theorem GQ2.Zhat.ofInt_zpow (n : ℤ) :
ofInt n = ofInt 1 ^ n

ofInt is the ℤ-power of ofInt 1 — the multiplicative reading of ℤ ⊆ ℤ̂ being generated by 1.

Topological generation of Γ_R by the four marked generators #

source
theorem GQ2.topGen_gammaR :
(Subgroup.closure {gammaSigmaR, gammaTauR, gammaX0R, gammaX1R}).topologicalClosure = ⊤

Γ_R is topologically generated by its four marked generators — the Γ_R mirror of GQ2.SectionThree.topGen_gammaA (glue lemma; the Γ_A original is stated at N_A).

source
theorem GQ2.nuDR_maxPro2Bridge_comp (g : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR) :
nuDR (maxPro2Bridge ((maxProPMk 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)) g)) = nuR g

The ν-composite over the whole of Γ_R (glue lemma; the pointwise closure of R15a's generator quadruple nuDR_maxPro2Bridge_*): ν_{D_R} ∘ maxPro2Bridge ∘ maxProPMk = ν_R, by density over the four marked generators.

The pro-2 boundary coordinate of Γ_R #

source
theorem GQ2.exists_pro2R [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
∃ (pro2R : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* ↑PiBd.toProfinite.toTop), (∀ (g : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR), nuT (phiR g) = nuTwo (pro2R g)) ∧ Function.Surjective ⇑pro2R ∧ pro2R.ker = proPKernel 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR) ∧ pro2R gammaTauR = 1

The Γ_R pro-2 boundary coordinate exists (⟦prop:markedpro2⟧ + Prop 3.10, local half): a continuous pro2R : Γ_R → Π that is ν-compatible with φ_R, surjective, has kernel exactly the pro-2 kernel, and kills τ — the composite eA ∘ e⁻¹ ∘ maxPro2Bridge ∘ maxProPMk of the module docstring.

source
noncomputable def GQ2.pro2R [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* ↑PiBd.toProfinite.toTop

The Γ_R pro-2 boundary coordinate pro2R : Γ_R → Π (a choice from exists_pro2R; B-Lab-conditional).

Equations
Instances For
    source
    theorem GQ2.pro2R_compat [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) (g : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR) :
    nuT (phiR g) = nuTwo ((pro2R hBLab) g)

    ν-compatibility: ν_t ∘ φ_R = ν₂ ∘ pro2R (the eq. (27) fibre condition for Γ_R).

    source
    theorem GQ2.pro2R_surjective [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
    Function.Surjective ⇑(pro2R hBLab)
    source
    theorem GQ2.ker_pro2R [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
    (pro2R hBLab).ker = proPKernel 2 (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)

    ker pro2R = proPKernel 2 Γ_R — the promoted SourceData.ker_pro2 field, from the max-pro-2 identification (the recon's "Γ_R from its max-pro-2 identification").

    source
    theorem GQ2.pro2R_gammaTauR [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
    (pro2R hBLab) gammaTauR = 1
    source
    theorem GQ2.bR_joint_surjective [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
    Function.Surjective fun (g : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR) => ⟨(phiR g, (pro2R hBLab) g), ⋯⟩

    Joint surjectivity of the Γ_R boundary pair (eq. (27) for Γ_R): the generic fibred-product kit at (φ_R, pro2R), exactly as boundaryMapsWitness.surjA.

    The marked-pinned generators (the module-docstring design finding) #

    Boundary points to hit: the pinned pairs of the SourceData interface. Membership in ∂bd is the ν-equation, discharged by the generator values of ν_t and ν₂.

    source
    noncomputable def GQ2.sigmaMarkR [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
    ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR

    The marked-pinned σ-generator of sourceR: an element of Γ_R over the boundary point (σ_t, σ_Π) (joint surjectivity). Not the honest gammaSigmaR — see the module docstring's design finding.

    Equations
    Instances For
      source
      theorem GQ2.sigmaMarkR_spec [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
      phiR (sigmaMarkR hBLab) = tameSigma ∧ (pro2R hBLab) (sigmaMarkR hBLab) = piSigma
      source
      noncomputable def GQ2.x0MarkR [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
      ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR

      The marked-pinned x₀-generator of sourceR.

      Equations
      Instances For
        source
        theorem GQ2.x0MarkR_spec [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
        phiR (x0MarkR hBLab) = 1 ∧ (pro2R hBLab) (x0MarkR hBLab) = piX0
        source
        noncomputable def GQ2.x1MarkR [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
        ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR

        The marked-pinned x₁-generator of sourceR.

        Equations
        Instances For
          source
          theorem GQ2.x1MarkR_spec [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
          phiR (x1MarkR hBLab) = 1 ∧ (pro2R hBLab) (x1MarkR hBLab) = piX1

          The Γ_R source instance #

          source
          noncomputable def GQ2.sourceR [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
          SourceData

          The Γ_R instance of the source interface (the R-campaign assembly): carrier GammaR, tame side φ_R/ν_R (⟦lem:tame⟧, R6), pro-2 side pro2R (⟦lem:pro2word⟧ + ⟦prop:markedpro2⟧ + Prop 3.10 local, B-Lab-conditional), and the seven supply-obligation families bound to the landed _gammaR lemmas of R31a–g — each by the same plain lambda BoundaryMaps.sourceA uses for its _gammaA twin.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem GQ2.sourceR_tame [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
            (sourceR hBLab).tame = phiR

            The tame field of sourceR is φ_R on the nose (mirror of BoundaryMaps.sourceA_b's load-bearing rfl).

            source
            theorem GQ2.sourceR_Γ [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
            (sourceR hBLab).Γ = GammaR

            The carrier of sourceR is Γ_R on the nose.

            The tame coordinate of b_{Γ_R} (the per-source Lemma 10.1 hypotheses) #

            source
            theorem GQ2.tameCoord_bR [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
            SectionTen.tameCoord (sourceR hBLab).b = phiR

            The tame coordinate of b_{Γ_R} is φ_R (mirror of SectionTen.tameCoord_bA).

            source
            theorem GQ2.tameCoord_bR_surjective [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
            Function.Surjective ⇑(SectionTen.tameCoord (sourceR hBLab).b)

            htame for Γ_R: φ_R is onto (Prop 3.2, Γ_R side; mirror of SectionTen.tameCoord_bA_surjective).

            source
            theorem GQ2.tameCoord_bR_ker_isProP [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) :
            IsProP 2 ↥(SectionTen.tameCoord (sourceR hBLab).b).ker

            hwild for Γ_R: the wild inertia ker φ_R = W_R is pro-2 (ker_phiR + isProP_wildCoreR; mirror of SectionTen.tameCoord_bA_ker_isProP).

            Eq. (154) at Γ_R and the surjection-count capstones #

            source
            theorem GQ2.eq_154_R [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] :
            Nat.card (ContSurj (↑GammaR.toProfinite.toTop) G) = Nat.card (ContSurj 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).

            source
            theorem GQ2.main_surjection_count_R [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) (G : Type) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] :
            contSurjCount G = 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).

            source
            theorem GQ2.admissibleCountR_eq_admissibleCount [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hBLab : BLabHypothesis) (G : Type) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] :
            admissibleCountR G = 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).

            The Replacement theorem (note ⟦thm:main⟧) #

            The AbsGalQ2 topology instances are file-local, exactly as in GQ2/PresentationLiteral.lean (the Γ_A literal capstone's pattern), so the terminal statement carries no instance binders — its hypothesis surface is exactly BLabHypothesis.

            source
            theorem GQ2.absGalQ2_compactSpace_roe :
            CompactSpace AbsGalQ2
            source
            theorem GQ2.absGalQ2_totallyDisconnectedSpace_roe :
            TotallyDisconnectedSpace AbsGalQ2
            source
            theorem GQ2.main_presentation_literal_roe (hBLab : BLabHypothesis) :
            Nonempty (↑GammaR.toProfinite.toTop ≃ₜ* AbsGalQ2)

            The Replacement theorem (note ⟦thm:main⟧, verbatim Γ_R ≅ G_{ℚ₂}; the R-campaign terminal theorem): granted the single Labute-classification instance hBLab (note Cor. 3.4 ⟦cor:abstractD0⟧ — an explicit hypothesis, not an axiom; discharged by the L-campaign), the Roe candidate Γ_R is continuously isomorphic to G_{ℚ₂}.

            Instantiates the main_presentation schematic at Γ_R, mirroring GQ2.main_presentation_literal: the candidate count hypothesis is eq_154_R ∘ main_surjection_count' (the Γ_R count agrees with admissibleCount through the G_{ℚ₂} bridge), the G_{ℚ₂} count is main_surjection_count', and the finite- generation witnesses are gammaR_topologicallyFinitelyGenerated (R31a) and B1.

            source
            theorem GQ2.main_presentation_literal_roe_unconditional :
            Nonempty (↑GammaR.toProfinite.toTop ≃ₜ* 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.

            Stress tests (plan rule 9) #

            Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; #

            hand-maintained)