noncomputable def Q2Presentation.Induction.properStrataChildren {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)) (J : mImageStrata chief K) : List FramedPair

The R3 strata of one image stratum as a list of framed pairs — one engine children block (canonically enumerated through the global Fintype (coverStrata …) instance).

Equations

• Q2Presentation.Induction.properStrataChildren chief K lam hinv J = List.map (Q2Presentation.Induction.properStratumPair chief K lam hinv J) Finset.univ.toList

theorem Q2Presentation.Induction.properStrataChildren_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) (J : mImageStrata chief K) : (List.map (⇑Cardinal.toNat ∘ framedCountA) (properStrataChildren chief K lam hinv J)).sum = 8 * mCount chief K lam hinv J boundaryPackage_GammaA

The block sum is the candidate R3 total: the summed ℕ-valued A-counts of the block equal 8·m_{A,λ}(J) (V4's exit in list form).

theorem Q2Presentation.Induction.properStrataChildren_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) (J : mImageStrata chief K) : (List.map (⇑Cardinal.toNat ∘ framedCountQ) (properStrataChildren chief K lam hinv J)).sum = 8 * mCount chief K lam hinv J boundaryPackage_GQ2

The block sum is the local R3 total (G_{ℚ₂} mirror).

theorem Q2Presentation.Induction.properStrataChildren_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) (J : mImageStrata chief K) (hJ : ↑J ≠ ⊤) (hR : 1 < Nat.card ↥(kernelFrattini K)) (q : FramedPair) : q ∈ properStrataChildren chief K lam hinv J → framedMeasure q < framedMeasure p

Every member of a proper block is a strictly smaller framed pair, on BOTH |Φ(K)|-branches (eq:properweighteddescent; the engine's small witness).

noncomputable def Q2Presentation.Induction.properIdx {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : { J : mImageStrata chief K // ↑J ≠ ⊤ } ≃ Fin (Nat.card { J : mImageStrata chief K // ↑J ≠ ⊤ })

The proper-image enumeration for P8's positional chunks.

Equations

• Q2Presentation.Induction.properIdx chief K = Finite.equivFin { J : Q2Presentation.Induction.mImageStrata chief K // ↑J ≠ ⊤ }