@[reducible, inline]

abbrev Q2Presentation.Induction.mImageStrata {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Type

The proper-image index (eq:recursionR2's sum): exact-image subgroups J ≤ B = Y/Φ(K) mapping onto C (J·M' = B). Includes the top J = B; "proper" is J.1 ≠ ⊤. Fintype is the canonical global coverStrata instance (CoverLiftPartition.lean:54).

Equations

• Q2Presentation.Induction.mImageStrata chief K = Q2Presentation.TorsorProgram.coverStrata (Q2Presentation.Induction.XRZero.xrChild chief K).fst (Q2Presentation.Induction.mChildKernel chief K).N

def Q2Presentation.Induction.mImageSurjWitness {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : mImageStrata chief K) : Function.Surjective ⇑((XRZero.xrChild chief K).fst.piY.comp (↑J).subtype)

The pinned surjectivity witness of a stratum (fixed once as a def so every downstream occurrence is term-identical — design §4.4/§9).

Equations

• ⋯ = ⋯

noncomputable def Q2Presentation.Induction.mImageStratumPair {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : mImageStrata chief K) : FramedPair

The stratum framed pair (J, J ∩ L_B, π|_J, θ|_J; p.2's frame) — manuscript: the exact-image object 𝒥 at the child. Measure |J ∩ L_B|.

Equations

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

noncomputable def Q2Presentation.Induction.mImageTop {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : mImageStrata chief K

The top stratum J = B (the m_{Γ,λ}(B) term of eq:recursionR2).

Equations

• Q2Presentation.Induction.mImageTop chief K = ⟨⊤, ⋯⟩

@[simp]

theorem Q2Presentation.Induction.mImageTop_val {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ↑(mImageTop chief K) = ⊤

theorem Q2Presentation.Induction.mImage_inf_mChild_ne {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : mImageStrata chief K) (hJ : ↑J ≠ ⊤) : ↑J ⊓ (mChildKernel chief K).N ≠ (mChildKernel chief K).N

Properness transfers to the M-layer: a proper image meets M' properly (design §3.3 step 1: M' ≤ J together with J·M' = ⊤ forces J = ⊤).

theorem Q2Presentation.Induction.mImage_inf_mChild_two_mul_card_le {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : mImageStrata chief K) (hJ : ↑J ≠ ⊤) : 2 * Nat.card ↥(↑J ⊓ (mChildKernel chief K).N) ≤ Nat.card ↥(mChildKernel chief K).N

Half bound in the M-layer: 2·|J ∩ M'| ≤ |M'| for proper J (design §3.3 step 2: a proper divisor of a finite group order is at most half — elementary abelianness is not even needed, finiteness suffices).

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

The full-kernel comparison hom ψ : L_B →* B/M' (top-level def so its applications are defeq-unfoldable — the stratumLYProj/xrChildLYProj idiom).

Equations

• Q2Presentation.Induction.mChildLYProj chief K = (QuotientGroup.mk' (Q2Presentation.Induction.mChildKernel chief K).N).comp (Q2Presentation.Induction.XRZero.xrChild chief K).fst.LY.subtype

theorem Q2Presentation.Induction.mImageStratumPair_two_mul_measure_le {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : mImageStrata chief K) (hJ : ↑J ≠ ⊤) : 2 * framedMeasure (mImageStratumPair chief K J) ≤ framedMeasure (XRZero.xrChild chief K)

eq:properweighteddescent, child half (design §3.3 step 3): 2·|J ∩ L_B| ≤ |L_B| = framedMeasure (xrChild) for proper J. Proof: the first-isomorphism counts along stratumLYProj (kernel ≅ J ⊓ M' since M' ≤ L_B) and mChildLYProj (kernel ≅ M'), the range inclusion, and the M-layer half bound.