The Lemma 9.4 descent bounds for blockFrame

Displays (145)/(148)/(153) of the paper's §9 induction: the marked-kernel cardinalities of the blockFrame's stage targets and of the pulled-back strata all drop strictly below |L_Y|, which is what lets the master induction (the §9 induction) recurse on n = Nat.card ↥T.LY.

Stated against blockFrameImpl; SectionNine.blockFrame delegates to it, so these apply to blockFrame by definitional unfolding.

• card_LB_mul / card_LB_lt — |L_B|·|R| = |L_Y|, and |L_B| < |L_Y| when R ≠ ⊥.
• card_LC_lt — |L_C| < |L_Y| (from K ≠ ⊥).
• four_le_card_K — 4 ≤ |K| (the dim V ≥ 2 input: |K| = 2 collapses the Y-action mod S).
• card_stratum_LB_lt — (148): a proper C-onto stratum of a central cover of B has |stratum.L| < |L_Y| (double cover ×2 against the index-2 J∩L_B < L_B, ÷|R| via R ≠ ⊥).
• card_stratum_LC_lt — (153): any stratum of a central cover of C has |stratum.L| < |L_Y| (trivial ⊆ p⁻¹(L_C) bound = 2|L_C|, against 4 ≤ |K|).

All bounds are cover-generic (independent of which CentralCover), which is what lets the §9 induction apply them to prop_8_9's ∃-quantified phase family.

General card helpers

theorem GQ2.card_comap_of_surjective {G G' : Type} [Group G] [Group G'] [Finite G] {f : G' →* G} (hf : Function.Surjective ⇑f) (S : Subgroup G) : Nat.card ↥(Subgroup.comap f S) = Nat.card ↥S * Nat.card ↥f.ker

Preimage cardinality under a surjection: |f⁻¹(S)| = |S|·|ker f|.

theorem GQ2.card_map_mk'_mul {G : Type} [Group G] [Finite G] {N Hs : Subgroup G} [N.Normal] (hNH : N ≤ Hs) : Nat.card ↥(Subgroup.map (QuotientGroup.mk' N) Hs) * Nat.card ↥N = Nat.card ↥Hs

Image cardinality under mk': for N ≤ H with N normal, the image of H in G/N has size |H|/|N|, i.e. |H.map (mk' N)| · |N| = |H| (Lagrange on H ↠ H/N).

theorem GQ2.centralCover_card_comap {G : Type} [Group G] [Finite G] (C : SectionEight.CentralCover G) (L : Subgroup G) : Nat.card ↥(Subgroup.comap C.p L) = 2 * Nat.card ↥L

The preimage of a subgroup under a central cover doubles it: |p⁻¹(L)| = 2·|L|.

theorem GQ2.card_subgroupOf_eq_inf {G : Type} [Group G] (A K : Subgroup G) : Nat.card ↥(A.subgroupOf K) = Nat.card ↥(A ⊓ K)

|H.subgroupOf K| = |H ⊓ K| (the intersection viewed inside K, K.subtype injective).

theorem GQ2.centralCover_card_le_two_mul_card_map {G : Type} [Group G] [Finite G] (C : SectionEight.CentralCover G) (W : Subgroup C.cover) : Nat.card ↥W ≤ 2 * Nat.card ↥(Subgroup.map C.p W)

Central covers are at most 2-to-1: for any subgroup W of the cover, |W| ≤ 2·|p(W)|.

Setup

instance GQ2.instNormalFrattiniK {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) : Blk.frattiniK.Normal

R = Φ(K) is normal in Y.

instance GQ2.instNormalK {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) : Blk.K.Normal

K is normal in Y (block field, re-exposed as an instance).

theorem GQ2.blockFrameImpl_K_le_LY {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) : Blk.K ≤ T.LY

theorem GQ2.blockFrameImpl_K_ne_bot {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) : Blk.K ≠ ⊥

K ≠ ⊥: else K ⊔ S = S = P contradicts S < P.

Field-projection reductions

theorem GQ2.blockFrameImpl_MB_le_TB_LY {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) : (blockFrameImpl T Blk hE2).MB ≤ (blockFrameImpl T Blk hE2).TB.LY

M ≤ L_B in B (both images of K ≤ L_Y), stated in projection form so it composes with Cov's (blockFrameImpl …).YB-typed subgroups.

(145) — the stage-target bounds

theorem GQ2.card_LB_mul {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) : Nat.card ↥(blockFrameImpl T Blk hE2).TB.LY * Nat.card ↥Blk.frattiniK = Nat.card ↥T.LY

(145a): |L_B|·|R| = |L_Y|.

theorem GQ2.card_LB_lt {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) (hR : Blk.frattiniK ≠ ⊥) : Nat.card ↥(blockFrameImpl T Blk hE2).TB.LY < Nat.card ↥T.LY

(145b): |L_B| < |L_Y| when R ≠ ⊥.

theorem GQ2.card_LC_lt {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) : Nat.card ↥(blockFrameImpl T Blk hE2).TC.LY < Nat.card ↥T.LY

(145c): |L_C| < |L_Y| (K ≠ ⊥).

4 ≤ |K| — the dim V ≥ 2 input for (153)

theorem GQ2.four_le_card_K {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) : 4 ≤ Nat.card ↥Blk.K

4 ≤ |K| (paper: dim V ≥ 2). If |K| = 2 then K is central (normal of order 2), so [Y, P] ≤ S (extending across P = K·S), contradicting nontrivial_action.

(148)/(153) — the pulled-back stratum bounds

theorem GQ2.card_stratum_LB_lt {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) (hR : Blk.frattiniK ≠ ⊥) (Cov : SectionEight.CentralCover (blockFrameImpl T Blk hE2).YB) (J' : Subgroup Cov.cover) (hJ' : Function.Surjective ⇑((Cov.pullTarget (blockFrameImpl T Blk hE2).TB).piY.comp J'.subtype)) (hJtop : Subgroup.map Cov.p J' ≠ ⊤) (hJC : Subgroup.map Cov.p J' ⊔ (blockFrameImpl T Blk hE2).MB = ⊤) : Nat.card ↥((Cov.pullTarget (blockFrameImpl T Blk hE2).TB).stratum J' hJ').LY < Nat.card ↥T.LY

(148): for a central cover Cov of B, a proper (J ≠ ⊤) C-onto (J ⊔ M = ⊤) stratum has marked kernel < |L_Y|.

theorem GQ2.card_stratum_LC_lt {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) (Cov : SectionEight.CentralCover (blockFrameImpl T Blk hE2).YC) (J' : Subgroup Cov.cover) (hJ' : Function.Surjective ⇑((Cov.pullTarget (blockFrameImpl T Blk hE2).TC).piY.comp J'.subtype)) : Nat.card ↥((Cov.pullTarget (blockFrameImpl T Blk hE2).TC).stratum J' hJ').LY < Nat.card ↥T.LY

(153): for a central cover Cov of C, any stratum has marked kernel < |L_Y| (trivial ⊆ p⁻¹(L_C) bound = 2|L_C|, against 4 ≤ |K|).

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

• Lemma 9.4 = ⟦lem-strictdecrease⟧ (= lemma 8.16 in current tex)