§8: Lemma 8.2 — the common scalar character group

The exponent-2 abelian ledger collapse and the two character counts it yields: |Hom_cont(Γ_A, 𝔽₂)| = 8 (lemma_8_2_gammaA) and |Hom_cont(G_ℚ₂, 𝔽₂)| = 8 (lemma_8_2_local), via the Π-side count card_char_piBd.

Lemma 8.2: the common scalar character group

The Γ_A-side proof runs entirely over the admissible-limit proof/Prop. 2.3 layer: continuous characters of Γ_A are F₄-generator values killing N_A; killing N_A forces c(τ) = 1 (tameRelator_mem_NA), and conversely c(τ) = 1 makes ker c admissible — because in an exponent-2 abelian quotient the whole ω₂-word ledger collapses and the wild relation (6) follows from τ = 1 (wildRel_of_comm2 below, the §8 counterpart of the AppendixB ledger evaluations; with the paper's h₀ — eq. (3), including the bare d₀ — the wild value at τ ≠ 1 is τ, so the relation is not unconditional).

theorem GQ2.SectionEight.powOmega2_eq_self_of_sq {A : Type u_1} [Group A] (h2 : ∀ (a : A), a * a = 1) (a : A) : powOmega2 a = a

powOmega2 is the identity on involutions (orderOf ∣ 2 means order 2^0 or 2^1).

theorem GQ2.SectionEight.conjP_of_comm {A : Type u_1} [Group A] (hcomm : ∀ (a b : A), a * b = b * a) (x g : A) : conjP x g = x

In an abelian group, the paper's conjugation is trivial.

theorem GQ2.SectionEight.commP_of_comm {A : Type u_1} [Group A] (hcomm : ∀ (a b : A), a * b = b * a) (x y : A) : commP x y = 1

In an abelian group, the paper's commutator is trivial.

theorem GQ2.SectionEight.Marking.wildRel_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.WildRel

The wild relation follows from τ = 1 in an exponent-2 abelian group (the ω₂-ledger collapse at τ = 1: uᵢ = xᵢ, d₀ = 1, c₀ = h_c = 1, h₀ = x₀² = 1, and (6) telescopes to 1). For scalar characters the hypothesis is free — the tame relation already forces τ = 1 (tameRel_iff_of_comm2), so they see no additional wild obstruction. (Without τ = 1 the wild value is τ: the paper's h₀ — eq. (3), with the bare d₀ — evaluates to 1, not τ.)

theorem GQ2.SectionEight.Marking.tameRel_iff_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) : t.TameRel ↔ t.τ = 1

In an exponent-2 abelian group, the tame relation says exactly τ = 1.

theorem GQ2.SectionEight.mul_comm_of_exp_two {A : Type u_1} [Group A] (h2 : ∀ (a : A), a * a = 1) (a b : A) : a * b = b * a

Exponent 2 forces commutativity (ab = (ab)⁻¹ = b⁻¹a⁻¹ = ba).

The Γ_A-side character count

noncomputable def GQ2.SectionEight.charEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : (G ⧸ N →ₜ* Multiplicative (ZMod 2)) ≃ { c : G →ₜ* Multiplicative (ZMod 2) // N ≤ c.ker }

Characters of a topological quotient group G ⧸ N are characters of G killing N (the Prop. 2.3 push/descend mechanics, without surjectivity; instantiated at N_A for the Γ_A-count and at the relator subgroup for the Π-count).

Equations

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

noncomputable def GQ2.SectionEight.cmhEquivFun {X : Type} : (↑(FreeProfiniteGroup X).toProfinite.toTop →ₜ* Multiplicative (ZMod 2)) ≃ (X → Multiplicative (ZMod 2))

Characters of a free profinite group are their generator values (the universal property, in ContinuousMonoidHom form via the Prop. 2.3 uniqueness lemma).

Equations

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

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

The kills-N_A criterion: a character of F₄ kills N_A iff it kills τ. Forward: N_A contains the tame relator (the admissible-limit proof), whose 𝔽₂-image is c(τ). Backward: ker c is then an admissible open normal subgroup (generation is automatic, the tame relation is the τ-kill, and the wild relation and 2-core are unconditional in an exponent-2 abelian quotient), so N_A ≤ ker c by the admissible-limit proof characterization.

def GQ2.SectionEight.vecEquiv : { v : Fin 4 → Multiplicative (ZMod 2) // v 1 = 1 } ≃ Multiplicative (ZMod 2) × Multiplicative (ZMod 2) × Multiplicative (ZMod 2)

Splitting off the τ-coordinate.

Equations

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

theorem GQ2.SectionEight.lemma_8_2_gammaA : Nat.card (↑GammaA.toProfinite.toTop →ₜ* Multiplicative (ZMod 2)) = 8

Lemma 8.2, candidate source: |Hom_cont(Γ_A, 𝔽₂)| = 8. Proved over the the admissible-limit proof/Prop. 2.3 layer: characters of Γ_A are F₄-generator values killing N_A (charEquiv/cmhEquivFun), and killing N_A is exactly killing τ (ker_char_NA_le_iff — the tame relator forces it, and conversely c(τ) = 1 gives both relations in exponent-2 abelian quotients, Marking.wildRel_of_comm2). That leaves the free 𝔽₂³ of σ, x₀, x₁-values.

The Π-side count and the local source

𝔽₂-characters kill the pro-2 kernel (the maximal pro-p quotient API), so they factor through the maximal pro-2 quotient; BoundaryMaps.ker_pro2F pins that quotient as Π, whose characters are the free 𝔽₂³ of σ, x₀, x₁-values (the piRelator-condition is vacuous by the same exponent-2 ledger collapse).

theorem GQ2.SectionEight.card_char_piBd : Nat.card (↑PiBd.toProfinite.toTop →ₜ* Multiplicative (ZMod 2)) = 8

The Π-character count: |Hom_cont(Π, 𝔽₂)| = 8 — the presentation has three generators and its relator has no mod-2 linear part (paper, proof of Lemma 8.2).

theorem GQ2.SectionEight.lemma_8_2_local (B : BoundaryMaps) [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : Nat.card (AbsGalQ2 →ₜ* Multiplicative (ZMod 2)) = 8

Lemma 8.2, local source: |Hom_cont(G_ℚ₂, 𝔽₂)| = 8 (= |ℚ₂ˣ/(ℚ₂ˣ)²|). Proved via the common marked maximal pro-2 quotient: a BoundaryMaps witness pins pro2F as the maximal pro-2 quotient map (ker_pro2F), every 𝔽₂-character kills the pro-2 kernel (the maximal pro-p quotient API proPKernel_le_ker), so precomposition with pro2F bijects characters of Π with characters of G_ℚ₂, and card_char_piBd finishes. [Statement amendment (F-owner): the BoundaryMaps hypothesis and the CompactSpace/TotallyDisconnectedSpace instance hypotheses on AbsGalQ2 (the main_presentation house pattern) — without the bundle the count is B4/B5-content outside the §8 proof layer axiom budget.]