Proposition 2.3 for Γ_R: |Sur(Γ_R, G)| = admissibleCountR G (Roe note Definition 1.1)

The Roe-candidate twin of GQ2/Prop23.lean (paper Prop. 2.3 ⟦prop-epi-semantics⟧, §2.2): for every finite discrete group G, continuous surjections Γ_R ↠ G correspond bijectively to R-admissible marked generating quadruples in G (note Definition 1.1 ⟦def:GammaR⟧), so

prop_2_3_R : Nat.card (ContSurj GammaR G) = admissibleCountR G.

This is the Γ_R half of the surjection-count semantics; prop_2_3_R is stated in exactly the shape the Roe main-presentation schematic (ticket R32) consumes, mirroring how prop_2_3 feeds main_presentation (GQ2/Statement.lean, via GQ2/PresentationLiteral.lean).

What is cloned and what is reused

Only the parts where the Roe wild relation actually enters are re-derived with an R-suffix; the word-independent round-trip scaffolding is imported and reused verbatim:

• reused (word-independent, from GQ2/GammaA.lean and GQ2/Prop23.lean): univMarking, Marking.toHom, univMarking_map_toHom, Marking.toHom_hom_univMarking_map, quotientMk, quotientLift, surjective_of_map_generates, and — crucially — Marking.classify itself (the classified hom of a marking is toHom-only, no relator enters);
• cloned (the Roe wild relation enters through AdmissibleR/N_R): admissibleR_of_NR_le_ker (converse of R3's NR_le_ker, proved from R3's isAdmissibleUR_of_NR_le + Marking.map_admissibleR), Marking.pushR, Marking.pushR_admissible, Marking.classifyR_ker (via NR_le_ker), Marking.descendR and its round trips, contSurjEquivAdmissibleR, and prop_2_3_R.

§5-duality supply input

The section markC_R / markC_admissible_R (the Roe twin of GQ2.WordCohBridge.markC / markC_admissible, GQ2/WordCohBridge.lean) is colocated here for convenience — it is not a prop_2_3_R dependency, but the input the §5 word-cohomology self-duality (prop_5_15_R, tickets R26/R31) consumes at markC_R θ, in the same adm.1 / adm.2.1 / adm.2.2.1 / adm.2.2.2 projection shape (Generates / TameRel / WildRelR / Pro2Core) as GQ2/MStageCountGammaA.lean.

Everything is at the standard three axioms (Ax = ∅).

The universal property, uniqueness half — REUSED

Marking.toHom_hom_univMarking_map (GQ2/Prop23.lean) is word-independent (it mentions only univMarking/Marking.toHom), so it is imported and reused; no R-suffix twin is needed.

The converse of NR_le_ker

theorem GQ2.admissibleR_of_NR_le_ker {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (f : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop →ₜ* G) (hsurj : Function.Surjective ⇑f) (hker : NR ≤ f.ker) : (Marking.map f.toMonoidHom univMarking).AdmissibleR

Converse of R3's NR_le_ker (Roe twin of GQ2.admissible_of_NA_le_ker): if a continuous homomorphism f : F₄ → G into a finite discrete group is surjective and kills N_R, then the pushed universal marking of G is R-admissible. Proof cloned verbatim from the Γ_A case, swapping isAdmissibleU_of_NA_le → isAdmissibleUR_of_NR_le, IsAdmissibleU → IsAdmissibleUR and Marking.map_admissible → Marking.map_admissibleR: ker f is then an open normal subgroup above N_R, hence R-admissible (isAdmissibleUR_of_NR_le, GQ2/Roe/AdmissibleLimit.lean), and R-admissibility transfers to G along F₄ ⧸ ker f ≃* G (Marking.map_admissibleR, GQ2/Roe/GammaR.lean). Together with NR_le_ker this is the note's "quotients of Γ_R = the R-admissible quotients".

The two directions of the bijection, as named constructions

noncomputable def GQ2.Marking.pushR {G : Type} [Group G] [TopologicalSpace G] (φ : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* G) : Marking G

The marking of G pushed forward from the universal marking along φ : F₄ ⧸ N_R → G. Roe twin of GQ2.Marking.push.

Equations

• GQ2.Marking.pushR φ = GQ2.Marking.map (φ.comp (GQ2.quotientMk GQ2.NR)).toMonoidHom GQ2.univMarking

theorem GQ2.Marking.pushR_admissible {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (φ : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* G) (hφ : Function.Surjective ⇑φ) : (pushR φ).AdmissibleR

The pushed marking of a continuous surjection is R-admissible (forward direction of prop_2_3_R). Roe twin of GQ2.Marking.push_admissible.

noncomputable def GQ2.Marking.descendR {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (t : Marking G) (ht : t.AdmissibleR) : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* G

The descended hom Γ_R → G of an R-admissible marking (backward direction of prop_2_3_R). Roe twin of GQ2.Marking.descend.

Equations

• t.descendR ht = GQ2.quotientLift GQ2.NR t.classify ⋯

theorem GQ2.Marking.descendR_surjective {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (t : Marking G) (ht : t.AdmissibleR) : Function.Surjective ⇑(t.descendR ht)

theorem GQ2.Marking.pushR_descendR {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (t : Marking G) (ht : t.AdmissibleR) : pushR (t.descendR ht) = t

Pushing the descended hom recovers the marking (round-trip 1). Roe twin of GQ2.Marking.push_descend.

theorem GQ2.Marking.descendR_pushR {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (φ : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* G) (hφ : Function.Surjective ⇑φ) : (pushR φ).descendR ⋯ = φ

Descending the pushed marking recovers the surjection (round-trip 2, via the uniqueness half of the universal property Marking.toHom_hom_univMarking_map). Roe twin of GQ2.Marking.descend_push.

Prop 2.3 for Γ_R

noncomputable def GQ2.contSurjEquivAdmissibleR (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] : ContSurj (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR) G ≃ { t : Marking G // t.AdmissibleR }

Prop. 2.3 for Γ_R, bijection form (paper §2.2 ⟦prop-epi-semantics⟧ / note Definition 1.1 ⟦def:GammaR⟧): continuous surjections Γ_R ↠ G correspond to R-admissible markings of G. (Stated on the underlying quotient F₄ ⧸ N_R, to which GammaR is definitionally equal.)

Equations

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

theorem GQ2.prop_2_3_R (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] : Nat.card (ContSurj (↑GammaR.toProfinite.toTop) G) = admissibleCountR G

Proposition 2.3 for Γ_R (paper §2.2 ⟦prop-epi-semantics⟧ / note Definition 1.1 ⟦def:GammaR⟧): the number of continuous surjections Γ_R ↠ G onto a finite discrete group equals admissibleCountR G, the number of R-admissible marked generating quadruples in G. Stated in exactly the hΓR shape the Roe main_presentation schematic (ticket R32) consumes, mirroring how prop_2_3 feeds main_presentation.

§5-duality supply: markC_R and markC_admissible_R

Not a prop_2_3_R dependency — colocated for the §5 word-cohomology self-duality (prop_5_15_R, tickets R26/R31). markC_R is the Roe twin of GQ2.WordCohBridge.markC (there markC q = Marking.push q), and markC_admissible_R wraps Marking.pushR_admissible, matching the adm.1 / adm.2.1 / adm.2.2.1 / adm.2.2.2 projection shape (Generates / TameRel / WildRelR / Pro2Core) that GQ2/MStageCountGammaA.lean feeds to prop_5_15.

noncomputable def GQ2.markC_R {C : Type} [Group C] [TopologicalSpace C] (q : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* C) : Marking C

The pushed marking t_q : Marking C of a continuous surjection q : Γ_R ↠ C — the Roe twin of GQ2.WordCohBridge.markC, against which the §5 word complex is formed.

Equations

• GQ2.markC_R q = GQ2.Marking.pushR q

theorem GQ2.markC_admissible_R {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] (q : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* C) (hq : Function.Surjective ⇑q) : (markC_R q).AdmissibleR

The pushed marking of a continuous surjection q : Γ_R ↠ C is R-admissible — the §5-duality supply input (prop_5_15_R, tickets R26/R31), Roe twin of GQ2.WordCohBridge.markC_admissible.

theorem GQ2.markC_admissible_R_clauses {C : Type} [Group C] [TopologicalSpace C] [DiscreteTopology C] [Finite C] (q : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR →ₜ* C) (hq : Function.Surjective ⇑q) : (markC_R q).Generates ∧ (markC_R q).TameRel ∧ (markC_R q).WildRelR ∧ (markC_R q).Pro2Core

Stress test (consumption shape). The four projections of markC_admissible_R land in the Roe clauses Generates / TameRel / WildRelR / Pro2Core, in the adm.1 / adm.2.1 / adm.2.2.1 / adm.2.2.2 order that GQ2/MStageCountGammaA.lean feeds to prop_5_15 — so prop_5_15_R's callers (R26/R31) reuse markC_admissible_R θ hθs verbatim. Pins the Roe wild relation WildRelR (not the Γ_A WildRel) at the .2.2.1 slot.

Paper-tag ledger (paper §2.2 + Roe note paper/roe-presentation-verification.tex;

hand-maintained)

• Proposition 2.3 = ⟦prop-epi-semantics⟧ (the epi-semantics cloned for Γ_R)
• Definition 1.1 = ⟦def:GammaR⟧