Admissible markings (Stage A)

A marking q : Marking G of a finite group is admissible when it generates G, satisfies the two displayed relators (the tame relator τ^σ τ⁻² and the wild relator h₀ u₁⁻¹ x₁^σ c₀, evaluated through the word language GExpr.eval, never by hand), and sends the two wild generators x₀, x₁ into the 2-core O₂(G).

This is the formal kernel of the Q₂ presentation (plan §1; manuscript §2, Proposition 2.3). The two structural theorems are:

• admissible_map_surjective — admissibility transports along a surjection;
• (in Subdirect.lean) admissible_subdirect — admissibility is closed under finite subdirect products (manuscript Lemma 2.1).

The relator preservation is uniform: it is GExpr.eval_map applied to the two relator words, so the wild word h₀ is never unfolded by hand.

def Q2Presentation.generates {G : Type u_1} [Group G] (q : Marking G) : Prop

q generates G: the marked generators close up to the whole group.

Equations

• Q2Presentation.generates q = (Subgroup.closure (Set.range q) = ⊤)

def Q2Presentation.tameRel {G : Type u_1} [Group G] [Finite G] (q : Marking G) : Prop

The tame relator holds at q: τ^σ = τ², evaluated through the word language (no hand rewriting).

Equations

• Q2Presentation.tameRel q = (Q2Presentation.Q2Word.tameRelator.eval q = 1)

def Q2Presentation.wildRel {G : Type u_1} [Group G] [Finite G] (q : Marking G) : Prop

The wild relator holds at q: h₀ u₁⁻¹ x₁^σ c₀ = 1, evaluated through the word language (the wild word h₀ is never unfolded by hand).

Equations

• Q2Presentation.wildRel q = (Q2Presentation.Q2Word.wildRelator.eval q = 1)

def Q2Presentation.Admissible {G : Type u_1} [Group G] [Finite G] (q : Marking G) : Prop

A marking is admissible when it generates, satisfies the tame and wild relators, and sends x₀, x₁ into the 2-core.

Equations

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

theorem Q2Presentation.admissible_map_surjective {G : Type u_1} {H : Type u_2} [Group G] [Finite G] [Group H] [Finite H] (φ : G →* H) (hφ : Function.Surjective ⇑φ) {q : Marking G} (hq : Admissible q) : Admissible fun (a : Gen) => φ (q a)

Admissibility transports along a surjection. If q is admissible and φ : G ↠ H is a surjective homomorphism of finite groups, then the pushed marking φ ∘ q is admissible. Generation comes from surjectivity, the two relators from GExpr.eval_map, and the 2-core conditions from hom_image_twoCore_le_twoCore.