Theorem 4.2 — the §9 sink #
thm_4_2 (the boundary-framed exact-image theorem) and its stratum clause, relocated from
GQ2/SectionNine.lean (second hop of the established relocation pattern; first hop was
BoundaryFrame → SectionNine, the §9 induction). The move is forced by the import DAG: the R-stage
lane consumes prop_8_9 (GQ2/Prop89Close.lean, incomparable with SectionNine) and
SectionNine.blockEnrichment (GQ2/BlockEnrichment.lean, strictly downstream of
SectionNine because it consumes kappa0_exists) — so the proof cannot live inside
SectionNine.lean. A comment-pointer remains there; the fully qualified name GQ2.thm_4_2
is unchanged, so call sites only gain an import.
The proof: strong induction on |L_Y| with three lanes — terminal (terminal_count_eq,
the §9 induction), M-stage (R = ⊥: mStage_partition ×2 at multiplicity |M_B|², the §9 induction +
MStageCount/MStageCountGammaA), and R-stage (R ≠ ⊥: blockEnrichment + prop_8_9
solved by count_eq_of_closedRecursion against the §9 induction bounds).
R-stage helpers #
The C-stage is nontrivial off the scalar-stack regime (discharges prop_8_9's
[Nontrivial YC]): if K = ⊤ then L_Y = ⊤, so Y is a finite 2-group, hence nilpotent —
and its upper central series exhibits L_Y as a scalar stack, contradicting the inductive
branch's ¬IsScalarStack.
C-ontoness of a B-subgroup in sup form: J.map π_{BC} = ⊤ ⟹ J ⊔ M_B = ⊤ (the shape
card_stratum_LB_lt consumes; ker π_{BC} = M_B).
Theorem 4.2 (boundary-framed exact-image theorem). For every boundary frame and
every boundary-framed marked target 𝒴, the exact-image lift counts from the two sources
agree: e^β_{Γ_A}(𝒴) = e^β_{G_ℚ₂}(𝒴).
Stated for any BoundaryMaps witness of the Prop 3.14 data (the choice is fixed "once and
for all" in §4 and only its bundled properties are used).
Encoding correction (documented in docs/section9-extraction.md): the hypothesis
(hE2 : ∀ e : E, e ^ 2 = 1) is required because the §9 induction descends the θ-decoration
through the block via lemma_7_3, whose (paper-stated)
hypothesis is that the decoration target is elementary abelian 2; the terminal case kills
the odd complement through θ for the same reason. §10 consumes the theorem at E = 0
only, so the correction is downstream-harmless. The theorem lives here because its proof
needs §§5–9 machinery, including blockEnrichment and
prop_8_9, both downstream of SectionNine; see the module docstring.
Instance binders: the two AbsGalQ2 topology hypotheses mirror
terminal_count_eq's (the Half139Local/BoundaryMapsWitness tower discipline — they are
deliberately not global instances); the consumer eq_154 already carries exactly
these two. The remaining topology instances the inductive lanes need (GammaA's
compact/t.d./topological-group triple, IsTopologicalGroup AbsGalQ2) are globally inferable
(GammaA : ProfiniteGrp; mathlib's Krull-topology instance), so they are not binders.
The proof combines the induction scaffold, terminal lane, M-stage lane, and the R-stage lane
assembled against prop_8_9 in GQ2/Prop89Close.lean.
Axioms B1/B3c/B6/B7/B8/B9 enter through the ingredients, per App. D (B7′, the dyadic Hilbert
symbol, is now an in-repo theorem, not an axiom).
Theorem 4.2's second clause: "the same equality holds for every exact-image target 𝒥"
— an instance of the first (strata are ordinary objects of the same category), recorded to
fix the consumption shape for §8. [Relocated with thm_4_2; carries the same hE2.]
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Prop 3.14 = ⟦prop-compatiblemarking⟧
- Theorem 4.2 = ⟦thm-fixedframe⟧