§9: the strong induction proving Theorem 4.2

Theorem 4.2 — equality of the boundary-framed exact-image counts of the two sources for every marked target — by strong induction on the marked 2-kernel size |L_Y| (paper pp. 44–47). This file provides the interfaces and subproofs used by the induction. The design and paper correspondence are recorded in docs/section9-extraction.md.

The two regimes:

• Terminal (IsScalarStack T.LY, i.e. every chief factor of L_Y is a trivial H-module): Lemma 9.2's Schur–Zassenhaus splitting Y ≅ H ×_{H₂} Q (GQ2.FiniteGroup.oddOrder_twoQuotient_split + coprime_fiber_product, proved) reduces both exact-image problems to the common marked maximal pro-2 quotient Π via (144) — the marked pro-2 isomorphisms (prop_3_10_gammaA, prop_3_10_local_marked). → terminal_count_eq (the §9 induction).
• Inductive (a nonscalar chief factor exists): choose the §7 block (SectionSeven.exists_minimalBlock), build the concrete recursion frame and enrichment on it (blockFrame/blockEnrichment; decorations descend by lemma_7_3, whence the standing hE2 hypothesis), obtain the closed system from prop_8_9, and solve it against the induction hypothesis count_eq_of_closedRecursion with Lemma 9.4's strict-decrease bounds). The R = ⊥ degenerate lane instead uses the elementary M-stage partition (mStage_partition, the §9 induction) directly.

Encoding correction (documented in docs/section9-extraction.md §Deviations): thm_4_2 requires (hE2 : ∀ e : E, e ^ 2 = 1). The §9 induction does not apply without it: the θ-decoration descends through the block only because E is elementary abelian 2 (lemma_7_3, whose paper statement carries exactly this hypothesis), and the terminal case kills the odd complement through θ for the same reason. §10 consumes Theorem 4.2 at E = 0 only (paper p. 48), so the correction is harmless downstream.

File organisation. The implementation is split into Terminal (the group-theoretic correspondence) and Induction (the terminal case and recursive solver). This umbrella preserves the original import path and public declaration names.

Theorem 4.2

The statements GQ2.thm_4_2 and GQ2.thm_4_2_stratum live in GQ2/ThmFourTwo.lean: the R-stage lane consumes prop_8_9 (Prop89Close) and SectionNine.blockEnrichment (BlockEnrichment, downstream of this file — it consumes kappa0_exists), so the proof cannot live here. Consumers import GQ2.ThmFourTwo; this file supplies the induction infrastructure without an import cycle.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (143) = ⟦eq-pointwiseconstrained⟧
• eq. (77) = ⟦eq-basepullback⟧
• Lemma 3.1 = ⟦lem-tamefinite⟧
• Lemma 6.1 = ⟦lem-extraspecialconnecting⟧
• Lemma 6.11 = ⟦lem-faithfulprojective⟧
• Lemma 6.2 = ⟦lem-halforbitcocycle⟧
• Lemma 6.3 = ⟦lem-basedetclass⟧
• Lemma 9.1 = ⟦lem-coprimesubdirect⟧
• Lemma 9.2 = ⟦lem-scalarterminal⟧
• Lemma 9.4 = ⟦lem-strictdecrease⟧ (= lemma 8.16 in current tex)
• Theorem 4.2 = ⟦thm-fixedframe⟧