Generic positional chunk extraction

def Q2Presentation.Induction.splitByLengths {β : Type u_1} : List ℕ → List β → List (List β)

Split a list into consecutive chunks of the given lengths.

Equations

• Q2Presentation.Induction.splitByLengths [] x✝ = []
• Q2Presentation.Induction.splitByLengths (n :: ns) x✝ = List.take n x✝ :: Q2Presentation.Induction.splitByLengths ns (List.drop n x✝)

theorem Q2Presentation.Induction.splitByLengths_flatMap_getD {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : α → List β) (F : β → γ) (l : List α) (i : ℕ) (hi : i < l.length) : (splitByLengths (List.map (fun (a : α) => (g a).length) l) (List.flatMap (fun (a : α) => List.map F (g a)) l)).getD i [] = List.map F (g l[i])

Chunk readout of a mapped flatMap: splitting the concatenation of the mapped blocks (g a).map F by the raw block lengths (g a).length and reading the i-th chunk returns exactly the i-th mapped block. (The F baked into the statement keeps the length profile F-free, so the counting formula's chunk lengths need no transport when the counts list is mapped.)

The parent/child measure factorization at the Frattini layer

def Q2Presentation.Induction.xrChildLYProj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ↥p.fst.LY →* p.fst.Y ⧸ XRZero.NR chief K

The marked-kernel comparison hom L_Y →* Y ⧸ Φ(K) (top-level def so its applications are defeq-unfoldable — the stratumLYProj idiom).

Equations

• Q2Presentation.Induction.xrChildLYProj chief K = (QuotientGroup.mk' (Q2Presentation.Induction.XRZero.NR chief K)).comp p.fst.LY.subtype

theorem Q2Presentation.Induction.xrChild_measure_factor {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : framedMeasure p = Nat.card ↥(kernelFrattini K) * framedMeasure (XRZero.xrChild chief K)

Exact factorization of the induction measure: |L_Y| = |Φ(K)| · |L_Y/Φ(K)| — first-isomorphism count for xrChildLYProj (kernel ≅ Φ(K) since Φ(K) ≤ L_Y, range = the child marked kernel).

theorem Q2Presentation.Induction.xrChild_measure_pos {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : 0 < framedMeasure (XRZero.xrChild chief K)

The child measure is positive (the child marked kernel is a nonempty finite subgroup).

theorem Q2Presentation.Induction.xrChild_double_measure_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (h4 : 4 ≤ Nat.card ↥(kernelFrattini K)) : 2 * framedMeasure (XRZero.xrChild chief K) < framedMeasure p

Strict decrease for doubled child measures at |Φ(K)| ≥ 4: 2·|L_B| < |L_Y| (eq:properweighteddescent at the top-level scalar cover; combined with scalarCoverStratumPair_measure_le_child this makes EVERY stratum of EVERY nonzero-λ cover a strictly smaller engine child).

theorem Q2Presentation.Induction.card_kernelFrattini_eq_two {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : 1 < Nat.card ↥(kernelFrattini K)) (h4 : ¬4 ≤ Nat.card ↥(kernelFrattini K)) : Nat.card ↥(kernelFrattini K) = 2

The residual case is exactly |Φ(K)| = 2: Φ(K) ≤ L_Y is a 2-group (LY_isTwoGroup), so a Frattini layer with 1 < |Φ(K)| < 4 has order exactly 2 — the complement of the 4 ≤ |Φ(K)| strata-children branch, and the hypothesis of the weakened keep.

The strata of one scalar cover as an engine children block

def Q2Presentation.Induction.scalarStrataChildren {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) : List FramedPair

The exact-image strata of the λ-cover as a list of framed pairs — one engine children block (lem:covertransform sum index, canonically enumerated through the global Fintype (coverStrata …) instance).

Equations

• Q2Presentation.Induction.scalarStrataChildren chief K lam hinv = List.map (Q2Presentation.Induction.scalarCoverStratumPair chief K lam hinv) Finset.univ.toList

theorem Q2Presentation.Induction.scalarStrataChildren_sum_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) : (List.map (⇑Cardinal.toNat ∘ framedCountA) (scalarStrataChildren chief K lam hinv)).sum = 8 * Nat.card { g : boundaryFramedSurj boundaryPackage_GammaA (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) lam hinv boundaryPackage_GammaA p.snd g) }

The block sum is the candidate partition total: the summed ℕ-valued A-counts of the strata block equal 8 · m_{A,λ}(B) — the exit theorem sec7_scalarCoverPartition_gammaA in list form.

theorem Q2Presentation.Induction.scalarStrataChildren_sum_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) : (List.map (⇑Cardinal.toNat ∘ framedCountQ) (scalarStrataChildren chief K lam hinv)).sum = 8 * Nat.card { g : boundaryFramedSurj boundaryPackage_GQ2 (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) lam hinv boundaryPackage_GQ2 p.snd g) }

The block sum is the local partition total: mirror of scalarStrataChildren_sum_gammaA for G_{ℚ₂} (sec7_scalarCoverPartition_gq2 in list form).

theorem Q2Presentation.Induction.scalarStrataChildren_measure_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (h4 : 4 ≤ Nat.card ↥(kernelFrattini K)) (c : FramedPair) : c ∈ scalarStrataChildren chief K lam hinv → framedMeasure c < framedMeasure p

Every member of a strata block is a strictly smaller framed pair once 4 ≤ |Φ(K)|: stratum measure ≤ 2·(xrChild measure) < parent measure. This is the per-child witness the engine's small field consumes — no stratum (including the top stratum J̃ = ⊤) is assumed smaller; all are proven so through the uniform bound.