The Roe-candidate words, wild relation, and admissibleCountR (Roe note §1)

Transcribes eqs. (1.1)–(1.2) and Definition 1.1 of the verification note paper/roe-presentation-verification.tex (the "Roe note") for finite groups: the auxiliary words of David Roe's candidate presentation

Γ_R = ⟨σ, τ, x₀, x₁ ∣ τ^σ = τ², r_R = (x₀^σ)⁻¹ · (x₀⁻³τ)^ω₂ · x₁² · [x₁, x₁^{σ₂}]⟩

evaluated at a marking t = (σ, τ, x₀, x₁), the Roe wild relation Marking.WildRelR, the R-admissibility predicate Marking.AdmissibleR, and the count admissibleCountR G of R-admissible markings — the Roe-candidate counterparts of GQ2.Words' Marking.WildRel/Admissible/admissibleCount.

Conventions match the note (and the paper) exactly:

• x ^ g = g⁻¹ * x * g (conjP)
• [x, y] = x⁻¹ * y⁻¹ * x * y (commP)
• x ^ ω₂ = the 2-primary part of x (powOmega2)

The note's eq. (1.1) ⟦eq:defwords⟧, verbatim:

\sigma_2=\sigma^{\omegaTwo},\qquad
a=(x_0^{-3}\tau)^{\omegaTwo},\qquad
y_1=x_1^{\sigma_2},\qquad
c=[x_1,y_1].

σ₂ already exists (Marking.sigma2, shared with Γ_A); the note's a, y₁, c are named aR, y1R, cR here. The two relators, eq. (1.2) ⟦eq:relators⟧, verbatim:

\rt=(\tau^\sigma)^{-1}\tau^2,\qquad
\rR=(x_0^\sigma)^{-1}a\,x_1^2c.

r_t is the tame relator shared with Γ_A (Marking.TameRel/tameValue); only r_R is new.

Alongside the definitions this file supplies (plan rules 8–9, stress-test discipline):

• naturality: Marking.map_aR/map_y1R/map_cR/map_wildValueR/map_wildRelR for a finite source (mirroring Marking.map_wildValue; the full map_admissibleR clone is ticket R3);
• the finite-exponent form wildValueExpR (the two ω₂-powers — in aR and in sigma2 inside cR — replaced by (·)^e) with the independence lemmas wildValueExpR_eq_wildValueR(_of_dvd) and the unconditional naturality wildValueExpR_map, mirroring GQ2.FoxH.wildValueExp (GQ2/FoxHeisenberg/Traced.lean);
• stress tests: the abelian collapse Marking.wildValueR_comm/wildValueExpR_comm and decide-checked concrete evaluations in Multiplicative (ZMod 8) (wildValueExpR_zmod8, wildValueExpR_zmod8_cube, wildValueR_zmod8) pinning the factor order, the −3 exponent, the inverted first factor, and the x₁² of r_R.

The Roe auxiliary words and relator (note eqs. (1.1)–(1.2))

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

a = (x₀⁻³ τ)^ω₂ — note eq. (1.1) ⟦eq:defwords⟧, verbatim a=(x_0^{-3}\tau)^{\omegaTwo}. Here x₀⁻³ = (x₀³)⁻¹. (The R suffix avoids clashing with variables named a.)

Equations

• t.aR = GQ2.powOmega2 ((t.x₀ ^ 3)⁻¹ * t.τ)

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

y₁ = x₁ ^ σ₂ — note eq. (1.1) ⟦eq:defwords⟧, verbatim y_1=x_1^{\sigma_2}, with σ₂ = σ^ω₂ = Marking.sigma2 (shared with Γ_A) and the conjugation convention x ^c g = g⁻¹xg.

Equations

• t.y1R = GQ2.conjP t.x₁ t.sigma2

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

c = [x₁, y₁] — note eq. (1.1) ⟦eq:defwords⟧, verbatim c=[x_1,y_1], with the commutator convention [x, y] = x⁻¹y⁻¹xy.

Equations

• t.cR = GQ2.commP t.x₁ t.y1R

noncomputable def GQ2.Marking.wildValueR {G : Type u_1} [Group G] (t : 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.

Equations

• t.wildValueR = (GQ2.conjP t.x₀ t.σ)⁻¹ * t.aR * t.x₁ ^ 2 * t.cR

def GQ2.Marking.WildRelR {G : Type u_1} [Group G] (t : 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.

Equations

• t.WildRelR = (t.wildValueR = 1)

@[simp]

theorem GQ2.Marking.wildValueR_eq_one_iff {G : Type u_1} [Group G] (t : Marking G) : t.wildValueR = 1 ↔ t.WildRelR

The Roe wild relator dies iff the Roe wild relation holds.

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

A marking is R-admissible if it generates, satisfies the tame relation and the Roe wild relation, and its wild generators have 2-group normal closure — note Definition 1.1 ⟦def:GammaR⟧: "the distinguished tuple generates the quotient, the two words in eq. (1.2) vanish, and the normal closure of the images of x₀, x₁ is a 2-group". Generates, TameRel and Pro2Core are reused verbatim from the Γ_A development (GQ2.Words); only the wild relation differs.

Equations

• t.AdmissibleR = (t.Generates ∧ t.TameRel ∧ t.WildRelR ∧ t.Pro2Core)

noncomputable def GQ2.admissibleCountR (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⁴.

Equations

• GQ2.admissibleCountR G = Nat.card { t : GQ2.Marking G // t.AdmissibleR }

Naturality of the Roe words (mirroring GQ2.Subdirect)

The ω₂-powers push through a group homomorphism via powOmega2_map, which needs the source finite — exactly as for the Γ_A word ledger. The full admissibility-preservation statement (map_admissible analogue) is ticket R3's, alongside GammaR/AdmissibleLimit.

@[simp]

theorem GQ2.Marking.map_aR {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).aR = f t.aR

@[simp]

theorem GQ2.Marking.map_y1R {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).y1R = f t.y1R

@[simp]

theorem GQ2.Marking.map_cR {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).cR = f t.cR

theorem GQ2.Marking.map_wildValueR {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).wildValueR = f t.wildValueR

Naturality of the Roe wild relator value under a group homomorphism (finite source) — the Γ_R counterpart of Marking.map_wildValue.

theorem GQ2.Marking.map_wildRelR {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) (h : t.WildRelR) : (map f t).WildRelR

The Roe wild relation transfers along any group hom (of a finite source).

The finite-exponent form (mirroring GQ2.FoxH.wildValueExp, Traced.lean)

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

The Roe wild relator word with the ω₂-powers replaced by an explicit integer exponent e (the note's ω₂ becomes (·)^e for a concrete e = omega2Exp N, a multiple of the relevant orders). Mirrors Marking.wildValueR's ledger exactly; only sigma2 and aR carry the exponent — two ω₂-subwords, versus three (sigma2, u0, u1) for Γ_A's wildValueExp.

Equations

• GQ2.wildValueExpR t e = (GQ2.conjP t.x₀ t.σ)⁻¹ * ((t.x₀ ^ 3)⁻¹ * t.τ) ^ e * t.x₁ ^ 2 * GQ2.commP t.x₁ (GQ2.conjP t.x₁ (t.σ ^ e))

theorem GQ2.wildValueExpR_map {G : Type u_1} {H : Type u_2} [Group G] [Group H] (φ : G →* H) (t : Marking G) (e : ℕ) : φ (wildValueExpR t e) = wildValueExpR (Marking.map φ t) e

wildValueExpR is natural in group homomorphisms — it uses only mul, inv, pow, conjP, commP (no ω₂), so no finiteness is needed.

theorem GQ2.wildValueExpR_eq_wildValueR {G : Type u_1} [Group G] [Finite G] (t : Marking G) : t.wildValueR = wildValueExpR t (omega2Exp (Monoid.exponent G))

For finite G, wildValueExpR at omega2Exp (Monoid.exponent G) is Marking.wildValueR: only sigma2 and aR carry ω₂, and each such element's order divides the exponent, so powOmega2_pow_eq rewrites the two ω₂-powers to the explicit omega2Exp-power.

theorem GQ2.wildValueExpR_eq_wildValueR_of_dvd {G : Type u_1} [Group G] {N : ℕ} (hN : N ≠ 0) (t : Marking G) (h0 : orderOf t.σ ∣ N) (h1 : orderOf ((t.x₀ ^ 3)⁻¹ * t.τ) ∣ N) : t.wildValueR = wildValueExpR t (omega2Exp N)

Divisibility form of wildValueExpR_eq_wildValueR: wildValueExpR t (omega2Exp N) = t.wildValueR for any N ≠ 0 that is a multiple of the two ω₂-subword orders (σ and x₀⁻³τ) — the exact analogue of GQ2.FoxH.wildValueExp_eq_wildValue_of_dvd, with one fewer hypothesis (no u1-subword).

Stress tests (plan rule 9)

Cheap sanity lemmas shipped with the definitions, chosen to catch transcription slips in r_R early (the Γ_A campaign's h₀ erratum, docs/erratum-h0-transcription.md, was exactly such a slip): the abelian collapse pins the conjugation/commutator conventions and the factor list; the ZMod 8 evaluations pin the signs and exponents numerically.

theorem GQ2.conjP_eq_self {G : Type u_1} [CommGroup G] (x g : G) : conjP x g = x

In a commutative group the paper's conjugation collapses: x ^c g = x.

theorem GQ2.commP_eq_one {G : Type u_1} [CommGroup G] (x y : G) : commP x y = 1

In a commutative group the paper's commutator collapses: [x, y] = 1.

theorem GQ2.Marking.wildValueR_comm {G : Type u_1} [CommGroup G] (t : Marking G) : t.wildValueR = t.x₀⁻¹ * t.aR * t.x₁ ^ 2

Stress test (abelian collapse). In a commutative group the commutator cR dies and the conjugations collapse, so the Roe wild relator reduces to x₀⁻¹ · a · x₁² — the abelianization of note eq. (1.2), with exponent vector (0, 1, −1−3, 2) in (σ, τ, x₀, x₁) once a is expanded at an odd ω₂-representative (cf. the note's Lemma 5.1 ⟦lem:stokes⟧ mod-2 vector (0,1,0,0)).

theorem GQ2.wildValueExpR_comm {G : Type u_1} [CommGroup G] (t : Marking G) (e : ℕ) : wildValueExpR t e = t.x₀⁻¹ * ((t.x₀ ^ 3)⁻¹ * t.τ) ^ e * t.x₁ ^ 2

Abelian collapse of the finite-exponent form: wildValueExpR reduces to x₀⁻¹ · (x₀⁻³τ)^e · x₁² in a commutative group.

def GQ2.zmod8MarkingR : Marking (Multiplicative (ZMod 8))

A concrete test marking (σ, τ, x₀, x₁) = (5, 1, 1, 1) (additive notation) in Multiplicative (ZMod 8), for the decide-checked evaluations below.

Equations

• GQ2.zmod8MarkingR = { σ := Multiplicative.ofAdd 5, τ := Multiplicative.ofAdd 1, x₀ := Multiplicative.ofAdd 1, x₁ := Multiplicative.ofAdd 1 }

theorem GQ2.wildValueExpR_zmod8 : wildValueExpR zmod8MarkingR 1 = Multiplicative.ofAdd 7

Stress test (concrete evaluation, e = 1). Additively in ZMod 8: −x₀ + (−3·x₀ + τ)·1 + 2·x₁ = −1 − 2 + 2 = −1 ≡ 7. Pins the inverted first factor (un-inverted x₀^σ would give 1), the −3 (a +3 would give 5), and the square x₁² (a bare x₁ would give 6).

theorem GQ2.wildValueExpR_zmod8_cube : wildValueExpR zmod8MarkingR 3 = Multiplicative.ofAdd 3

Stress test (concrete evaluation, e = 3). Same marking at the odd exponent 3 (every ω₂-representative is odd): −1 + 3·(−2) + 2 = −5 ≡ 3 (mod 8) — pins the placement of the exponent on the aR-subword.

theorem GQ2.omega2Exp_eight : omega2Exp 8 = 1

omega2Exp 8 = 1: on a group of exponent 8 (a 2-group) the concrete ω₂-representative is 1, i.e. ω₂ acts as the identity — the elementwise face of "ω₂ ≡ 1 on the 2-part".

theorem GQ2.wildValueR_zmod8 : zmod8MarkingR.wildValueR = Multiplicative.ofAdd 7

Stress test (the genuine ω₂-word, end-to-end). Multiplicative (ZMod 8) has exponent dividing 8 and omega2Exp 8 = 1, so the noncomputable wildValueR itself agrees with the e = 1 evaluation above — exercising wildValueExpR_eq_wildValueR_of_dvd on a concrete instance.

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

• eq. (1.1) = ⟦eq:defwords⟧
• eq. (1.2) = ⟦eq:relators⟧
• Definition 1.1 = ⟦def:GammaR⟧
• Lemma 5.1 = ⟦lem:stokes⟧