Documentation

GQ2.Roe.Supply

Γ_R source-data supply: topological finite generation and the scalar character count #

The two Γ_R source obligations that are independent of the R30 pro-2 coordinate, i.e. rows ii.1 and ii.2 of the SourceData recon memo (docs/orchestration/roe-r30-recon.md). Each is an exact byte-for-byte clone of its Γ_A original, with the same carrier spelling, so that the R30 SourceData structure and R32's main_presentation instantiation can plug Γ_R into the A-slot:

Both declarations become SourceData field values for R30/R32. No new axioms (#print axioms at the standard three throughout); all counting scaffolding is reused, never re-proved.

Module-system note. Unlike its GQ2/Roe/* siblings this file is deliberately not a module (plain import, no @[expose] public section): it depends on GQ2.SectionEight.ScalarCount, and the whole GQ2/SectionEight/ chain is non-module, so a module header here fails to elaborate with cannot import non-moduleGQ2.SectionEight.ScalarCount frommodule``. Same resolution as the sibling GQ2/Roe/Prop23.lean, which reaches into the same non-module §2/§8 stack. Importing the module files GQ2.Roe.AdmissibleLimit / GQ2.FinitelyGenerated from here is fine — the restriction is one-directional. R30's GQ2/SourceData.lean will inherit the same constraint.

(recon row ii.1) Γ_R is topologically finitely generated #

Verbatim clone of GQ2.gammaA_isTopologicallyFinGen / GQ2.gammaA_topologicallyFinitelyGenerated (GQ2/FinitelyGenerated.lean), routed through the Γ_R quotient projection F₄ ↠ Γ_R.

source
theorem GQ2.gammaR_isTopologicallyFinGen :
IsTopologicallyFinGen ↑GammaR.toProfinite.toTop

Γ_R is topologically finitely generated (the predicate form). Clone of GQ2.gammaA_isTopologicallyFinGen: the free profinite group F₄ is topologically finitely generated (isTopologicallyFinGen_freeProfiniteGroup), and this passes along the continuous surjection F₄ ↠ F₄ ⧸ N_R = Γ_R (IsTopologicallyFinGen.of_surjective).

source
theorem GQ2.gammaR_topologicallyFinitelyGenerated :
∃ (s : Finset ↑GammaR.toProfinite.toTop), (Subgroup.closure ↑s).topologicalClosure = ⊤

(recon row ii.1) Γ_R is topologically finitely generated, in exactly the ∃ s : Finset _, … shape consumed as the hfgA/hfg argument of the §8/§9 lanes and by R32's main_presentation instantiation — the same statement shape and carrier spelling (GammaR : Type) as its Γ_A original GQ2.gammaA_topologicallyFinitelyGenerated (GQ2/FinitelyGenerated.lean).

source
theorem GQ2.gammaR_and_gammaA_isTopologicallyFinGen :
IsTopologicallyFinGen ↑GammaR.toProfinite.toTop ∧ IsTopologicallyFinGen ↑GammaA.toProfinite.toTop

Stress test / cross-check: Γ_R and Γ_A are topologically finitely generated by the same mechanism — the image of F₄'s four free generators — so the predicate holds for both candidate groups (the wild relation is irrelevant to finite generation).

(recon row ii.2) The Γ_R scalar character count |Hom_cont(Γ_R, 𝔽₂)| = 8 #

Clone of GQ2.SectionEight.lemma_8_2_gammaA (GQ2/SectionEight/ScalarCount.lean), reusing the generic counting scaffolding charEquiv / cmhEquivFun / vecEquiv and porting the single source-specific lemma ker_char_NA_le_iff to ker_char_NR_le_iff.

source
theorem GQ2.Marking.wildRelR_of_comm2 {A : Type u_1} [Group A] (hcomm : ∀ (a b : A), a * b = b * a) (h2 : ∀ (a : A), a * a = 1) (t : Marking A) (hτ : t.τ = 1) :
t.WildRelR

The Roe wild relation follows from τ = 1 in an exponent-2 abelian group — the Roe counterpart of GQ2.SectionEight.Marking.wildRel_of_comm2. The ω₂-ledger collapses: powOmega2 = id on involutions, conjugations and commutators are trivial, so r_R = (x₀^σ)⁻¹ · (x₀⁻³τ)^{ω₂} · x₁² · [x₁, y₁] reduces to x₀⁻¹ · (x₀⁻³τ) · x₁², and with τ = 1, x₀² = x₁² = 1 this telescopes to 1 (mod 2 the ledger −4·χ(x₀) + χ(τ) is vacuous once χ(τ) = 0; cf. R1 Marking.wildValueR_comm, GQ2/Roe/Words.lean). For scalar characters the hypothesis τ = 1 is free — the tame relation already forces it (GQ2.SectionEight.Marking.tameRel_iff_of_comm2).

source
theorem GQ2.ker_char_NR_le_iff (c : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop →ₜ* Multiplicative (ZMod 2)) :
NR ≤ c.ker ↔ c univMarking.τ = 1

The kills-N_R criterion: a character of F₄ kills N_R iff it kills τ. Port of GQ2.SectionEight.ker_char_NA_le_iff, swapping the tame-relator membership tameRelator_mem_NR (R3 GQ2/Roe/AdmissibleLimit.lean), IsAdmissibleUR, the Roe exponent-2 collapse Marking.wildRelR_of_comm2, and the admissible-opens characterization GQ2.isAdmissibleUR_iff_NR_le. Forward: N_R contains the tame relator, whose 𝔽₂-image is c(τ). Backward: ker c is then R-admissible (generation automatic, tame is the τ-kill, and in an exponent-2 abelian quotient both the Roe wild relation and the 2-core are unconditional), so N_R ≤ ker c.

source
theorem GQ2.lemma_8_2_R :
Nat.card (↑GammaR.toProfinite.toTop →ₜ* Multiplicative (ZMod 2)) = 8

(recon row ii.2) Lemma 8.2, Roe source: |Hom_cont(Γ_R, 𝔽₂)| = 8. Byte-for-byte clone of GQ2.SectionEight.lemma_8_2_gammaA (GQ2/SectionEight/ScalarCount.lean) with N_A replaced by N_R: characters of Γ_R are F₄-generator values killing N_R (GQ2.SectionEight.charEquiv / cmhEquivFun), and killing N_R is exactly killing τ (ker_char_NR_le_iff — the tame relator forces it, and conversely c(τ) = 1 gives both relations in exponent-2 abelian quotients). That leaves the free 𝔽₂³ of σ, x₀, x₁-values. Same carrier spelling GammaR and statement shape as the Γ_A original, as required by R30/R32.

source
theorem GQ2.lemma_8_2_R_eq_gammaA :
Nat.card (↑GammaR.toProfinite.toTop →ₜ* Multiplicative (ZMod 2)) = Nat.card (↑GammaA.toProfinite.toTop →ₜ* Multiplicative (ZMod 2))

Stress test / cross-check: the Roe scalar character count equals the Γ_A count (both 2³ = 8) — the mod-2 abelian ledger sees no difference between the two wild relations.

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