The M-stage lane of the §9 master induction

thm_4_2's R = ⊥ lane applies mStage_partition (the §9 induction) to the block frame at both sources and solves the two partition identities against the induction hypothesis. This file provides the lane's inputs (design note docs/section9-extraction.md §the §9 induction; handoff docs/orchestration/p17i-handoff.md §5.2):

• target transports — exactImageCount_congr (count invariance along an iso of marked targets), the ⊤-stratum evaluation SectionEight.exactImageCountOn_top, and the R = ⊥ collapse SectionEight.RecursionFrame.exactImageCount_TB_of_R_bot (π_B is then an iso, so e(𝒴_B) = e(𝒴) — the design note's "R = ⊥ ⟹ piB iso" transport);
• the degenerate-head case — exactImageCount_eq_zero_of_not_headSurj: a boundary lift composes to a surjection Γ ↠ H through the frame head, so an uncovered head kills both counts (this discharges mStage_partition's hhead via a case split at the top of the lane, since b_{Γ_A}/b_{G_ℚ₂} are onto ∂bd);
• the stratum bound — card_stratum_mStage_lt: a proper C-onto stratum of 𝒴_B itself (no central cover) has marked kernel < |L_Y|, valid for every R (the cover version card_stratum_LB_lt needs R ≠ ⊥, so the R = ⊥ lane cannot use it);
• the per-source multiplicity counts (mStage_partition's hmult, mult = |M_B|²) — the unrestricted-B-lift count #LiftsOver(ρ) = |M_B|² over every lower map, the Enrichment-free analogue of Half139Local.hMcountM_local (the R = ⊥ lane has no radical edge and blockEnrichment is gated, so the count is stated on RecursionFrame.LiftsOver directly).

Count transport along an iso of marked targets

noncomputable def GQ2.boundaryLiftsCongr {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y₁ Y₂ : Type} [Group Y₁] [TopologicalSpace Y₁] [DiscreteTopology Y₁] [Finite Y₁] [Group Y₂] [TopologicalSpace Y₂] [DiscreteTopology Y₂] [Finite Y₂] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (T₁ : MarkedTarget H E Y₁) (T₂ : MarkedTarget H E Y₂) (e : Y₁ ≃* Y₂) (hhead : ∀ (y : Y₁), T₂.piY (e y) = T₁.piY y) (htheta : ∀ (y : Y₁), T₂.thetaY (e y) = T₁.thetaY y) : BoundaryLifts b F T₁ ≃ BoundaryLifts b F T₂

The boundary-lift bijection along an isomorphism of marked targets (the equiv underlying exactImageCount_congr, exposed so decorated counts can subtype over it — the the §9 induction nPhase/liftableCount bridge below).

Equations

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

theorem GQ2.exactImageCount_congr {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y₁ Y₂ : Type} [Group Y₁] [TopologicalSpace Y₁] [DiscreteTopology Y₁] [Finite Y₁] [Group Y₂] [TopologicalSpace Y₂] [DiscreteTopology Y₂] [Finite Y₂] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (T₁ : MarkedTarget H E Y₁) (T₂ : MarkedTarget H E Y₂) (e : Y₁ ≃* Y₂) (hhead : ∀ (y : Y₁), T₂.piY (e y) = T₁.piY y) (htheta : ∀ (y : Y₁), T₂.thetaY (e y) = T₁.thetaY y) : exactImageCount b F T₁ = exactImageCount b F T₂

Exact-image counts transport along an isomorphism of marked targets: a MulEquiv e : Y₁ ≃* Y₂ intertwining heads and decorations induces a bijection of the boundary-lift sets (continuity is free — the targets are discrete).

theorem GQ2.MarkedTarget.top_head_surjective {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) : Function.Surjective ⇑(T.piY.comp ⊤.subtype)

The ⊤-stratum always carries the full head.

theorem GQ2.SectionEight.exactImageCountOn_top {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (T : MarkedTarget H E Y) : exactImageCountOn b F T ⊤ = exactImageCount b F T

Evaluation of the totalized stratum count at ⊤: the ⊤-stratum is the ambient target (transport along ↥⊤ ≃* Y).

theorem GQ2.SectionEight.RecursionFrame.exactImageCount_TB_of_R_bot {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (hR : Blk.frattiniK = ⊥) : exactImageCount b F RF.TB = exactImageCount b F T

R = ⊥ collapses the B-stage: π_B is then an isomorphism (ker π_B = R = ⊥), so the B-stage target has the ambient exact-image count. The M-stage lane's ⊤-stratum feed (design note: "R = ⊥ ⟹ piB iso ⟹ e(b, TB) = e(b, T)").

theorem GQ2.SectionEight.RecursionFrame.nPhase_eq_liftableCount_top {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (Cζ : CentralCover RF.YC) : RF.nPhase b F Cζ = liftableCount b F RF.TC Cζ ⊤ ⋯

The phase count is the ⊤-stratum liftable count (the §9 induction hphase feed): n_{Γ,0}(ζ) = u^β_Γ(p_ζ, ⊤), so lemma_8_3 at the ⊤ stratum expands 8·nPhase into the pulled-stratum counts of the phase cover. The ⊤-stratum transport is boundaryLiftsCongr at ↥⊤ ≃* Y_C, and the cover-lift decorations agree definitionally (the coercion ↥⊤ → Y_C is the equiv).

The degenerate-head case

theorem GQ2.exactImageCount_eq_zero_of_not_headSurj {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (T : MarkedTarget H E Y) (hns : ¬Function.Surjective fun (x : ↥boundarySubgroup) => (F.frameMap x).1) : exactImageCount b F T = 0

Degenerate head ⟹ zero count (any source): a boundary lift f has π_Y ∘ f = (frameMap ∘ b).1 with π_Y ∘ f onto H, so an uncovered frame head admits no lift at all. Both sources are killed simultaneously, which is how the M-stage lane discharges mStage_partition's hhead hypothesis (a case split on the head's surjectivity).

The M-stage stratum bound

The R = ⊥ lane feeds the IH at the proper C-onto strata of 𝒴_B itself; the (148) bound card_stratum_LB_lt is the cover version and requires R ≠ ⊥, so the lane needs its own bound — which in exchange holds for every R.

theorem GQ2.card_stratum_mStage_lt {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) (J : Subgroup (blockFrameImpl T Blk hE2).YB) (hJtop : J ≠ ⊤) (hJC : Subgroup.map (blockFrameImpl T Blk hE2).piBC J = ⊤) (hJ : Function.Surjective ⇑((blockFrameImpl T Blk hE2).TB.piY.comp J.subtype)) : Nat.card ↥((blockFrameImpl T Blk hE2).TB.stratum J hJ).LY < Nat.card ↥T.LY

M-stage stratum bound: a proper (J ≠ ⊤) C-onto (J.map π_{BC} = ⊤) stratum of the B-stage target has marked kernel < |L_Y|. Properness against C-ontoness forces L_B ⊓ J to have index ≥ 2 in L_B (if L_B ≤ J then M_B ≤ J, and C-ontoness pulls all of B into J), and |L_B| ≤ |L_Y| by (145a).

The per-source multiplicity count, local side

mStage_partition's hmult at mult = |M_B|² for Γ = G_ℚ₂: over every lower boundary lift ρ, the unrestricted B-lift set LiftsOver ρ has exactly |M_B|² elements. This is the Enrichment-free analogue of Half139Local.hMcountM_local — same five-step route (additive M-module with the ρ-conjugation action; Z¹-torsor bridge with nonemptiness from #H² = 1; card_Z1_eq [B7]; #fixedPts = 1 from lemma_7_1_dual) with the quotient Y_B ⧸ M replaced by Y_C itself (π_{BC} has kernel M_B, RecursionFrame.ker_piBC) and the coset section Quotient.out replaced by Function.surjInv π_{BC}. Stated on RecursionFrame.LiftsOver directly because the R = ⊥ lane has no radical datum (and blockEnrichment is gated on the §9 induction).

Axioms: std-3 + B6 + B7 (B6 via card_H2_eq_fixedPts, B7 via card_Z1_eq) — as for hMcountM_local.

The shared M_B module pack

Both halves of liftsOver_card_local (nonemptiness and the Z¹-torsor count) run the same M_B-module setup: M_B ⊴ Y_B is elementary abelian (2-torsion by MB_elem), carries the Y_C-conjugation action through a set-section of π_{BC}, and has no nonzero Y_C-invariant 𝔽₂-functional (lemma_7_1_dual). These private helpers mirror the wave-25b factoring in the Γ_A twin GQ2/MStageCountGammaA.lean (kept file-private, statements identical).

theorem GQ2.SectionEight.RecursionFrame.liftsOver_card_local {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] [IsTopologicalGroup AbsGalQ2] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : AbsGalQ2 →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (ρ : BoundaryLifts b F RF.TC) : Nat.card (RF.LiftsOver b F ρ) = Nat.card ↥RF.MB ^ 2

hmult for G_ℚ₂ (the M-stage multiplicity): #LiftsOver(ρ) = |M_B|² over every lower boundary lift ρ of the C-stage target.