§10 tame-frame exhaustion, de-axiomatized (tameFrameExhaustion_proven)

This file replaces the axiom Q2Presentation.Induction.tameFrameExhaustion (Induction/CountsEqual.lean, manuscript lem:tameframeexhaustion + eq:allcounts, l.4555–4595) by a theorem tameFrameExhaustion_proven with the exact same statement. The §10 disjoint-union bookkeeping — Sur(Γ, G) decomposes, over a source-independent index of tame boundary frames, into the fixed-frame boundary-framed surjection sets, and this turns into a Cardinal.sum — is proved here in full. Only the single genuinely-irreducible local input survives, isolated as a minimal documented axiom.

The decomposition (manuscript lem:tameframeexhaustion)

Fix a finite group G and put L = O₂(G) = twoCore G (the characteristic wild subgroup). The manuscript decomposition is:

• the canonical framed target 𝒴_G (tameTarget G): target G, marked 2-kernel L, tame quotient π_Y = (G ↠ G/L), trivial decoration E = ℤ/2, θ_Y = 1;
• the frame index Frames G = Sur(T_A, G/L), the surjections of the fixed profinite tame group T_A = Ttame onto G/L. This depends on G only — the manuscript's "the induced quotient map T_A → G/L is a tame frame, and the frame index is the same set for both sources";
• every epimorphism f : Γ ↠ G induces a unique tame frame: its quotient map Γ ↠ G/L (the characteristic wild subgroup maps into L) factors through the tame quotient T_A as a surjection α_f : T_A ↠ G/L (manuscript prop:tamequotient). With decoration E = 0 the boundary-framed condition q_Y ∘ f = β ∘ b_Γ records exactly "f induces the frame α", so Sur(Γ, G) is the disjoint union, over Frames G, of the fixed-frame boundary-framed sets.

Taking Cardinal.mk and using Cardinal.mk_sigma turns the disjoint union into Cardinal.sum. The two sources Γ_A (boundaryPackage_GammaA) and G_{ℚ₂} (boundaryPackage_GQ2) share the same Frames G and per-frame target 𝒴_G, so the two equalities eq:allcounts hold with one common index — exactly the existential shape of the axiom.

What is proved vs. the isolated axiom

• PROVEN (this file). frame_decomposition: for any boundary package B on a profinite Γ equipped with the tame-frame factorization, |Sur(Γ, G)| equals the Cardinal.sum over Frames G of the fixed-frame boundary-framed counts. This is the entire §10 bookkeeping: the Equiv.sigmaFiberEquiv fibre decomposition, the reduction of the boundary-framed condition (trivial decoration ⇒ only the tame coordinate constrains), uniqueness of the induced frame (T_A-surjectivity + morphism extensionality), automatic surjectivity of the induced frame, and the Cardinal.mk_sigma passage. tameFrameExhaustion_proven is then immediate.

• THEOREMS gammaA_tameQuotientFactor / gq2_tameQuotientFactor — the manuscript prop:tamequotient (lem:tameframeexhaustion's sole non-bookkeeping input), one per source: every epimorphism f : Γ ↠ G has its induced quotient map Γ ↠ G/O₂(G) factor through the tame quotient Γ ↠ T_A. Equivalently the characteristic wild subgroup ker(Γ ↠ T_A) maps into O₂(G) under f. This is the universal property of the tame quotient — that T_A is the maximal quotient seeing no wild 2-part — which is not available in the codebase: the candidate side's kernel characterisation ker(gammaTameMap) = W_A is explicitly left unproved (Boundary/CandidateTame.lean); on the local side this maximality/factorization is now folded into the already-cited local tame datum gq2_tame_quotient, because it is a direct component of Prop tamequotient plus lem:o2tame. Classification: local/structural (prop:tamequotient, local class field theory on the G_{ℚ₂} side; lem:o2tame O₂(Γ_A) = W_A on the candidate side), in the same family as the already-isolated local-CFT inputs. They assume nothing about surjection counts: each describes a single f's factorization, and the equality of counts is derived downstream by boundaryFramed_counts_equal (Theorem 4.2).

Surjectivity of the induced frame α_f and uniqueness of the frame are derived, so the axiom is the minimal factorization statement.

The canonical tame-quotient framed target of a finite group G

noncomputable def Q2Presentation.Induction.tameTarget (G : Type) [Group G] [Finite G] : BoundaryFramedTarget

The canonical boundary-framed marked target 𝒴_G attached to a finite group G (manuscript lem:tameframeexhaustion, the E = 0 framed target): the target is G, the marked 2-kernel is the 2-core O₂(G) = twoCore G (a 2-group by twoCore_isPGroup, the wild part), the tame quotient is the canonical projection π_Y : G ↠ G/O₂(G) (kernel exactly O₂(G) by QuotientGroup.ker_mk'), and the decoration is trivial (E = ℤ/2, θ_Y = 1).

Equations

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

@[simp]

theorem Q2Presentation.Induction.tameTarget_Y (G : Type) [Group G] [Finite G] : (tameTarget G).Y = G

@[simp]

theorem Q2Presentation.Induction.tameTarget_H (G : Type) [Group G] [Finite G] : (tameTarget G).H = (G ⧸ twoCore G)

@[simp]

theorem Q2Presentation.Induction.tameTarget_E (G : Type) [Group G] [Finite G] : (tameTarget G).E = ZMod 2

@[simp]

theorem Q2Presentation.Induction.tameTarget_piY (G : Type) [Group G] [Finite G] : (tameTarget G).piY = QuotientGroup.mk' (twoCore G)

@[simp]

theorem Q2Presentation.Induction.tameTarget_thetaY (G : Type) [Group G] [Finite G] : (tameTarget G).thetaY = 1

The trivial elementary marking ψ and the frame attached to a tame quotient

noncomputable def Q2Presentation.Induction.trivPsi : PiGrp ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Multiplicative (ZMod 2)))

The trivial elementary marking ψ : Π → Multiplicative (ℤ/2), the constant map to 1. Continuous (constant), so a genuine morphism of profinite groups. With the trivial decoration E = ℤ/2, θ_Y = 1, this is all the ψ data a frame needs: the boundary-framed condition then constrains only the tame coordinate.

Equations

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

@[simp]

theorem Q2Presentation.Induction.trivPsi_apply (x : ↑PiGrp.toProfinite.toTop) : (ProfiniteGrp.Hom.hom trivPsi) x = 1

noncomputable def Q2Presentation.Induction.frameOf (G : Type) [Group G] [Finite G] (α : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ twoCore G))) (hα : Function.Surjective ⇑(ProfiniteGrp.Hom.hom α)) : BoundaryFrame (tameTarget G)

The boundary frame attached to a tame frame α : T_A ↠ G/O₂(G) (manuscript eq:beta with trivial elementary marking): (α, ψ = 1, β = boundaryBeta α 1). The frame index Frames G is exactly the surjections α.

Equations

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

@[simp]

theorem Q2Presentation.Induction.frameOf_alpha (G : Type) [Group G] [Finite G] (α : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ twoCore G))) (hα : Function.Surjective ⇑(ProfiniteGrp.Hom.hom α)) : (frameOf G α hα).alpha = α

@[simp]

theorem Q2Presentation.Induction.frameOf_beta (G : Type) [Group G] [Finite G] (α : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ twoCore G))) (hα : Function.Surjective ⇑(ProfiniteGrp.Hom.hom α)) : (frameOf G α hα).beta = boundaryBeta α trivPsi

The source-independent frame index and the per-frame framed pair

def Q2Presentation.Induction.Frames (G : Type) [Group G] [Finite G] : Type

The frame index of G (manuscript: the tame frames T_A ↠ G/O₂(G)): the surjective continuous homomorphisms of the fixed profinite tame group Ttame onto G/O₂(G). This is source-independent — a function of G alone — so it indexes the decomposition of both sources simultaneously, exactly as the axiom's existential demands.

Equations

• Q2Presentation.Induction.Frames G = Q2Presentation.Profinite.SurjContHom Q2Presentation.Ttame (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ Q2Presentation.twoCore G)))

noncomputable def Q2Presentation.Induction.framePairOf (G : Type) [Group G] [Finite G] (φ : Frames G) : FramedPair

The per-frame framed pair (𝒴_G, F_α) of the decomposition (the value Y φ fed to the axiom's existential): the canonical framed target with the frame attached to φ.

Equations

• Q2Presentation.Induction.framePairOf G φ = ⟨Q2Presentation.Induction.tameTarget G, Q2Presentation.Induction.frameOf G φ.hom ⋯⟩

The isolated irreducible input: the tame-quotient factorization (prop:tamequotient)

theorem Q2Presentation.Induction.gammaA_tameQuotientFactor (G : Type) [Group G] [Finite G] [Nonempty G] (f : Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) : ∃ (α : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ twoCore G))), ∀ (γ : ↑GammaA.toProfinite.toTop), (QuotientGroup.mk' (twoCore G)) ((ProfiniteGrp.Hom.hom f.hom) γ) = (ProfiniteGrp.Hom.hom α) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) γ)

Tame-quotient factorization, candidate side (manuscript prop:tamequotient for Γ_A, the sole non-bookkeeping content of lem:tameframeexhaustion). Every continuous epimorphism f : Γ_A ↠ G onto a finite group induces a quotient map Γ_A ↠ G/O₂(G) that factors through the candidate tame quotient gammaTameMap : Γ_A ↠ T_A: there is α : T_A ⟶ G/O₂(G) with mk ∘ f = α ∘ gammaTameMap. Equivalently the characteristic wild subgroup ker(gammaTameMap) = W_A maps into O₂(G) under f.

This is the universal property of the tame quotient T_A (the maximal quotient seeing no wild 2-part), i.e. lem:o2tame O₂(Γ_A) = W_A together with functoriality of the 2-core. It is genuinely irreducible and absent from the codebase: the candidate kernel characterisation ker(gammaTameMap) = W_A is explicitly left unproved (Boundary/CandidateTame.lean module docstring), so the factorization cannot be derived from GammaA_epi_equiv_admissible (admissibility only places the generators x₀, x₁ in O₂, not the whole closed wild kernel). It assumes nothing about surjection counts — only a single f's factorization. Surjectivity of α is derived (alpha_surjective_of_factor).

theorem Q2Presentation.Induction.gq2_tameQuotientFactor (G : Type) [Group G] [Finite G] [Nonempty G] (f : Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) : ∃ (α : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ twoCore G))), ∀ (γ : ↑GQ2Profinite.toProfinite.toTop), (QuotientGroup.mk' (twoCore G)) ((ProfiniteGrp.Hom.hom f.hom) γ) = (ProfiniteGrp.Hom.hom α) ((ProfiniteGrp.Hom.hom boundaryPackage_GQ2.tameMap) γ)

Tame-quotient factorization, local side (manuscript prop:tamequotient for G_{ℚ₂}). Every continuous epimorphism f : G_{ℚ₂} ↠ G onto a finite group induces a quotient map G_{ℚ₂} ↠ G/O₂(G) factoring through the local tame quotient G_{ℚ₂} ↠ T_A: there is α : T_A ⟶ G/O₂(G) with mk ∘ f = α ∘ tameMap_loc.

This is genuine local class field theory (the maximal tame quotient G_{ℚ₂}/W_F ≅ T_A absorbs every map to a trivial-2-core finite group), and is now exposed as a theorem projecting the maximality/factorization field of the already-cited local tame datum gq2_tame_quotient. It likewise concerns a single f, not surjection counts, so #print axioms tameFrameExhaustion_proven should contain gq2_tame_quotient rather than a separate gq2_tameQuotientFactor axiom.

Derived facts: surjectivity and uniqueness of the induced frame

theorem Q2Presentation.Induction.alpha_surjective_of_factor {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) {G : Type} [Group G] [Finite G] {f : Profinite.SurjContHom Γ (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))} {α : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ twoCore G))} (hfα : ∀ (γ : ↑Γ.toProfinite.toTop), (QuotientGroup.mk' (twoCore G)) ((ProfiniteGrp.Hom.hom f.hom) γ) = (ProfiniteGrp.Hom.hom α) ((ProfiniteGrp.Hom.hom B.tameMap) γ)) : Function.Surjective ⇑(ProfiniteGrp.Hom.hom α)

The induced frame is surjective (derived, not assumed). If mk ∘ f = α ∘ tameMap with f and mk surjective, then α is surjective: every t = mk (f γ) equals α (tameMap γ).

The §10 decomposition (PROVEN)

theorem Q2Presentation.Induction.frame_decomposition {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (G : Type) [Group G] [Finite G] [Nonempty G] (hfac : ∀ (f : Profinite.SurjContHom Γ (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))), ∃ (α : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ twoCore G))), ∀ (γ : ↑Γ.toProfinite.toTop), (QuotientGroup.mk' (twoCore G)) ((ProfiniteGrp.Hom.hom f.hom) γ) = (ProfiniteGrp.Hom.hom α) ((ProfiniteGrp.Hom.hom B.tameMap) γ)) : Cardinal.mk (Profinite.SurjContHom Γ (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.sum fun (φ : Frames G) => Cardinal.mk (boundaryFramedSurj B (tameTarget G) (frameOf G φ.hom ⋯))

The §10 tame-frame decomposition (manuscript lem:tameframeexhaustion, the bookkeeping, PROVEN). For a boundary package B on Γ equipped with the tame-quotient factorization hfac, the surjection count |Sur(Γ, G)| is the Cardinal.sum, over the source-independent frame index Frames G, of the fixed-frame boundary-framed surjection counts of the canonical framed target 𝒴_G.

The proof: each f : Sur(Γ, G) chooses (via hfac) its induced tame frame α_f, giving a map g : Sur(Γ, G) → Frames G. The fibre g⁻¹(φ) is exactly the fixed-frame boundary-framed set boundaryFramedSurj B 𝒴_G F_φ (the boundary-framed condition reduces, since E = 0, to "f induces the frame φ", and φ is the unique such frame by T_A-surjectivity). Equiv.sigmaFiberEquiv then gives Sur(Γ, G) ≃ Σ φ, g⁻¹(φ), and Cardinal.mk_sigma turns the fibre decomposition into the Cardinal.sum.

The exact axiom statement, now a theorem

theorem Q2Presentation.Induction.tameFrameExhaustion_proven (G : Type) [Group G] [Finite G] [Nonempty G] : ∃ (Frames : Type) (Y : Frames → FramedPair), (Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.sum fun (φ : Frames) => framedCountA (Y φ)) ∧ Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.sum fun (φ : Frames) => framedCountQ (Y φ)

Tame-frame exhaustion (manuscript lem:tameframeexhaustion, eq:allcounts), the EXACT statement of the axiom tameFrameExhaustion, now proved as a theorem.

For every finite group G there is a source-independent frame index Frames and a per-frame framed pair Y such that both |Sur(Γ_A, G)| and |Sur(G_{ℚ₂}, G)| decompose, over this common index, into the fixed-frame boundary-framed counts. Provided by Frames G = Sur(T_A, G/O₂(G)) and Y φ = (𝒴_G, F_φ); the two decompositions are the two applications of the proven frame_decomposition with the tame-quotient factorizations gammaA_tameQuotientFactor / gq2_tameQuotientFactor.

Acceptance checks