The terminal and recursive regimes of the Section 9 induction

The terminal count, κ⁰ base class, recursion frame, and recursion solver.

See GQ2.SectionNine for the paper-facing overview, source citations, and deviations.

The terminal regime

theorem GQ2.SectionNine.terminal_count_eq {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] (B : BoundaryMaps) (F : BoundaryFrame H E) [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (T : MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1) (hstack : SectionSeven.IsScalarStack T.LY) : exactImageCount B.bA F T = exactImageCount B.bF F T

The terminal case (§9.1): if every chief factor of L_Y is scalar (a trivial H-module — IsScalarStack), the two exact-image problems are identical: Lemma 9.2 splits Y ≅ H ×_{H₂} Q off the odd part of H (Schur–Zassenhaus, GQ2.FiniteGroup.oddOrder_twoQuotient_split), the boundary data descend to the finite 2-group Q (θ kills the odd complement since E has exponent 2), and the (144) correspondence + coprime_fiber_product identify boundary-framed maps from either source with marked maps Π → Q — the same set for both sources by the marked pro-2 isomorphisms.

The κ⁰ base class

Reusable structural core (the Lemma 6.3 skeleton)

The paper's existence proof for the base class κ⁰_q is Lemma 6.3, not Lemma 6.1 (Lemma 6.1 only records the equivalence "(59)+(60) ⟺ E_f carries a lifted C-action" and assumes a lift is chosen). Lemma 6.3 builds the datum for a simple self-dual tame module V by three structural moves, each of which is a self-contained, source-generic fact proved here; see docs/orchestration/p17e-kappa0-scoping.md for why the general kappa0_exists below is not a paper theorem (the lift obstruction in H²(C, V^∨) need not vanish for an arbitrary module) and for the honest restatement these lemmas assemble into.

• isEquivariantFactorSet_of_invariant — an invariant normalized factor set needs no corrections (m = 0): the paper's orbit factor sets (75)/(76).
• IsEquivariantFactorSet.add — the datum of a sum q + q' is the sum of the data: the "sum of the cocycles corresponding to the orbit polynomials occurring in q_W" step.
• IsEquivariantFactorSet.comap — pullback along an equivariant additive map (eq. (77)), packaged as kappa0_exists_of_split (the Lemma 6.3 reduction to a split embedding).

theorem GQ2.SectionNine.IsEquivariantFactorSet.comap {C : Type u_1} {V : Type u_2} {W : Type u_3} [Group C] [AddCommGroup V] [AddCommGroup W] [DistribMulAction C V] [DistribMulAction C W] {q : W → ZMod 2} {dat : FactorSet C W} (hdat : IsEquivariantFactorSet q dat) (i : V →+ W) (hi : ∀ (c : C) (v : V), i (c • v) = c • i v) : IsEquivariantFactorSet (fun (v : V) => q (i v)) (dat.comap i)

Pullback of an equivariant factor-set datum along an equivariant additive map i : V →+ W (eq. (77), datum level): if i is C-equivariant, then dat.comap i is an equivariant factor-set datum for the pulled-back form q ∘ i.

theorem GQ2.SectionNine.IsEquivariantFactorSet.comapHom {C : Type u_1} {D : Type u_2} {V : Type u_3} [Group C] [Group D] [AddCommGroup V] [DistribMulAction C V] [DistribMulAction D V] {q : V → ZMod 2} {dat : FactorSet D V} (hdat : IsEquivariantFactorSet q dat) (π : C →* D) (hπ : ∀ (c : C) (v : V), c • v = π c • v) : IsEquivariantFactorSet q { f := dat.f, m := fun (c : C) (v : V) => dat.m (π c) v }

Pullback of an equivariant factor-set datum along a group homomorphism π : C →* D compatible with the actions (c • v = π c • v): f is unchanged, m_c := m_{π c}. This is the reduction of the κ⁰ existence problem to any group the action factors through — e.g. the faithful tame image of ActsThroughTame below (existence over the image gives existence over C), which is how Lemma 6.3's "let H = H_V be the faithful tame image" step enters.

def GQ2.SectionNine.ActsThroughTame (C : Type u_1) [Group C] (V : Type u_2) [AddCommGroup V] [DistribMulAction C V] : Prop

The C-action on V factors through a finite tame group: a finite H acting on V, generated by a pair s, t with the tame relation s⁻¹ t s = t² (the finite avatar of a Ttame-quotient, the same interface as tame_two_nilpotent), and a surjective π : C →* H with c • v = π c • v. Surjectivity makes H-data (invariance of q, submodule lattice) agree with C-data, so an equivariant factor-set datum over H pulls back along IsEquivariantFactorSet.comapHom. At the §9 induction call site this is discharged with H := the frame head: K acts trivially on V = P/S by [K,P] ≤ [P,P] ≤ S, and the rest of L_Y acts trivially by FoxH.lemma_5_12 (normal 2-subgroup on a chief factor), so the C = Y/K action descends to Y/L_Y ≅ H, whose marked generators satisfy the tame relation.

Equations

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

The orbit factor sets are equivariant (Lemma 6.3's (75)/(76))

The concrete m = 0 orbit data from GQ2/OrbitData.lean are IsEquivariantFactorSet for their square maps: biadditive in the coordinates, and G/N-invariant because the left-regular action merely permutes coordinates (finsum_comp_equiv along Equiv.mulLeft). Entry point: isEquivariantFactorSet_of_biadditive_invariant (now polar-free).

theorem GQ2.SectionNine.kappa0_exists {C : Type} [Group C] [Finite C] {V : Type} [AddCommGroup V] [Finite V] [DistribMulAction C V] (q : V → ZMod 2) (hq : QuadraticFp2.IsQuadraticFp2 q) (hns : QuadraticFp2.Nonsingular q) (hinv : QuadraticFp2.IsInvariant C q) (hsimple : FoxH.IsSimpleModTwo C V) (htame : ActsThroughTame C V) : ∃ (dat : FactorSet C V), IsEquivariantFactorSet q dat

Existence of the equivariant factor-set datum (the base determinant class κ⁰_q) — the paper's Lemma 6.3, p. 26: a C-invariant nonsingular quadratic form on a simple tame 𝔽₂[C]-module admits a normalized equivariant factor-set datum. (Self-duality is implied: hns + hinv make v ↦ polar q v · a C-isomorphism V ≅ V^∨.)

Encoding correction (documented deviation: docs/orchestration/p17e-kappa0-scoping.md). The earlier form omitted hsimple/htame, making the statement stronger than the paper's and in fact false — Lemma 6.1 only proves the equivalence "(59)+(60) ⟺ E_f carries a lifted C-action" and assumes the lift exists; a datum is exactly a splitting of 1 → V^∨ → Aut_Z(E_f) → O(q) → 1 pulled back along ρ : C → O(q), and for C = O(q) itself that extension is non-split for large extraspecial E_f (Griess, Pacific J. Math. 48 (1973)). The added hypotheses are Lemma 6.3's own, are dischargeable at the sole call site (the §9 induction, see ActsThroughTame's docstring), and restore truth via the paper's construction: reduce to the faithful tame image (comapHom), split-embed V into a permutation module (Lemma 6.11 / Maschke — projectivity is where simplicity+tameness are consumed), decompose the extended form into orbit polynomials, and sum their explicit data ((75)/(76)/Lemma 6.2) — the proved lemmas above are exactly these assembly steps. The proof unpacks htame, transports invariance and simplicity along the surjection, applies GQ2.kappa0_exists_tame (GQ2/KappaNormalForm.lean — faithful-image reduction, the odd/unramified averaging branch, and the ramified branch through lemma_6_11_of_tame_pair + the permutation-module normal form), and pulls back with comapHom.

The concrete block frame and enrichment

The §7 block Blk on a target T determines the recursion frame of §8 concretely: B = Y/R, C = Y/K with the boundary data descended through lemma_7_3 (this is where hE2 enters), D_R = the kernel-encoded scalar characters (card_DR's subtype itself), and the scalar covers p_λ = Y/R' ↠ Y/R. The enrichment fields are the §7.4 outputs: q_λ via prop_7_4 + mForm_of_qbar (the Prop. 8.9 assembly), quadraticity/nonsingularity of q̄_λ derived from the block (design routes in docs/section9-extraction.md), the descended module from GQ2/BlockModule.lean's blockAction, and the κ⁰ datum from kappa0_exists. Spec and size lemmas about these constructions (the (145)/(148)/(153) bounds, Lemma 9.4) are the §9 induction, stated per the design note.

noncomputable def GQ2.SectionNine.blockFrame {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) : SectionEight.RecursionFrame T Blk

The concrete recursion frame of the block (the §9 induction). R = ⊥ is allowed (the frame is then degenerate; the induction's R = ⊥ lane uses mStage_partition instead of prop_8_9).

Equations

• GQ2.SectionNine.blockFrame T Blk hE2 = GQ2.blockFrameImpl T Blk hE2

The elementary M-stage partition

theorem GQ2.SectionNine.mStage_partition {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : SectionEight.RecursionFrame T Blk) {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (hhead : Function.Surjective fun (γ : Γ) => (F.frameMap (b γ)).1) (mult : ℕ) (hmult : ∀ (ρ : BoundaryLifts b F RF.TC), Nat.card (RF.LiftsOver b F ρ) = mult) : mult * exactImageCount b F RF.TC = ∑ᶠ (J : Subgroup RF.YB) (_ : J ∈ {J : Subgroup RF.YB | Subgroup.map RF.piBC J = ⊤}), SectionEight.exactImageCountOn b F RF.TB J

The M-stage partition (§9.2): the unrestricted B-lifts of the lower exact-image maps, all with the same multiplicity mult over each lower map (hmult — the |Z¹_{Γ,ρ}(M)| = 2^{2·dim M} numerics of props 5.15/5.16, source-discharged at the §9 induction), partition by exact image into the C-onto strata of T_B: mult · e_Γ(C) = Σ_{J ↠ C} e_Γ(stratum J). Machinery: the LiftsOver-fibration of the Prop. 8.9 assembly + the image-stratification of partition137_of/lemma_8_3. [the §9 induction statement; proof the §9 induction.]

The recursion solver

theorem GQ2.SectionNine.count_eq_of_closedRecursion {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : SectionEight.RecursionFrame T Blk) {Γ₁ : Type} [Group Γ₁] [TopologicalSpace Γ₁] {Γ₂ : Type} [Group Γ₂] [TopologicalSpace Γ₂] (b₁ : Γ₁ →ₜ* ↥boundarySubgroup) (b₂ : Γ₂ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (μ : ℕ) (G0 : ℤ) (DT : Type) [Fintype DT] (phase : (l : RF.DR) → l ≠ RF.zeroDR → DT → SectionEight.CentralCover RF.YC) (h₁ : SectionEight.ClosedRecursion RF b₁ F μ G0 DT phase) (h₂ : SectionEight.ClosedRecursion RF b₂ F μ G0 DT phase) (hDT : Nat.card DT ≠ 0) (hTB : exactImageCount b₁ F RF.TB = exactImageCount b₂ F RF.TB) (hTC : exactImageCount b₁ F RF.TC = exactImageCount b₂ F RF.TC) (hpull : ∀ (l : RF.DR) (h : l ≠ RF.zeroDR) (J' : Subgroup (RF.scalarCover l h).cover), Subgroup.map (RF.scalarCover l h).p J' ≠ ⊤ → Subgroup.map RF.piBC (Subgroup.map (RF.scalarCover l h).p J') = ⊤ → SectionEight.exactImageCountOn b₁ F ((RF.scalarCover l h).pullTarget RF.TB) J' = SectionEight.exactImageCountOn b₂ F ((RF.scalarCover l h).pullTarget RF.TB) J') (hphase : ∀ (l : RF.DR) (h : l ≠ RF.zeroDR) (ζ : DT), RF.nPhase b₁ F (phase l h ζ) = RF.nPhase b₂ F (phase l h ζ)) : exactImageCount b₁ F T = exactImageCount b₂ F T

Solving the closed recursion (the §9.3 bookkeeping): two sources satisfying the boxed system (136)–(140) for the same frame and the same shared data (μ, G⁰, D_T, phase) have equal exact-image counts at the top, provided the strictly-smaller ingredient counts agree — the atoms the induction hypothesis supplies:

• hTB/hTC — the quotient-stage counts (|L_B|, |L_C| < |L_Y|);
• hpull — the (138) pullback-stratum counts at every scalar cover, restricted to the strata over proper C-onto images (the only ones (137) consumes; exactly the (148) regime, kernels ≤ 2|J ∩ L_B| ≤ |L_B| < |L_Y| — for an improper image the pulled kernel can equal |L_Y| at |R| = 2, so an unrestricted atom would be un-suppliable by the induction) [restriction added the §9 induction, documented];
• hphase — the phase-cover liftable counts (derived at the §9 induction from lemma_8_3 at the phase covers + the (153) bound 2|L_C| < |L_Y|; here taken as an atom).

Derivation: (138) + hpull give the m_J agreement (cancel 8); (139)/(140) + hTC + hphase give the Z_{B/C} agreement (cancel 2, resp. 2·#D_T ≠ 0); (137) then gives the m_B agreement; (136) + #D_R ≠ 0 gives the top count. Pure ℤ-arithmetic. [the §9 induction statement; proof the §9 induction.]