theorem Q2Presentation.Induction.MStage.NK_le_LY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : K.Ksub ≤ p.fst.LY

K.Ksub ≤ L_Y.

theorem Q2Presentation.Induction.MStage.NK_theta {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (n : p.fst.Y) : n ∈ K.Ksub → p.fst.thetaY n = 1

The decoration kills K.Ksub.

instance Q2Presentation.Induction.MStage.instNormalYFstBoundaryFramedTargetBoundaryFrameKsub {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : K.Ksub.Normal

theorem Q2Presentation.Induction.MStage.quotient_measure_lt_gen {p : FramedPair} (N : Subgroup p.fst.Y) [hNn : N.Normal] (hNLY : N ≤ p.fst.LY) (hNθ : ∀ n ∈ N, p.fst.thetaY n = 1) (hN : 1 < Nat.card ↥N) : framedMeasure ⟨TorsorProgram.quotientFramedTarget p.fst N hNLY hNθ, TorsorProgram.quotientFrame p.fst N hNLY hNθ p.snd⟩ < framedMeasure p

Generic strict measure decrease of the quotient child.

def Q2Presentation.Induction.MStage.properJs {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Finset (Subgroup p.fst.Y)

The proper exact-image subgroup family: proper J still covering C.

Equations

• Q2Presentation.Induction.MStage.properJs chief K = {J : Subgroup p.fst.Y | J ≠ ⊤ ∧ J ⊔ K.Ksub = ⊤}.toFinset

theorem Q2Presentation.Induction.MStage.mem_properJs {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : Subgroup p.fst.Y) : J ∈ properJs chief K ↔ J ≠ ⊤ ∧ J ⊔ K.Ksub = ⊤

theorem Q2Presentation.Induction.MStage.properJs_piY_surj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : Subgroup p.fst.Y) (hJ : J ⊔ K.Ksub = ⊤) : Function.Surjective ⇑(p.fst.piY.comp J.subtype)

Members of the family surject onto the tame quotient.

theorem Q2Presentation.Induction.MStage.properJs_LY_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : Subgroup p.fst.Y) (hne : J ≠ ⊤) (hJ : J ⊔ K.Ksub = ⊤) : ¬p.fst.LY ≤ J

Proper members meet the wild kernel properly (eq:Mdescent-input).

def Q2Presentation.Induction.MStage.mstageChild {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Sec7FrattiniTrivialElementaryChildData p

The manuscript child data at the M-layer.

Equations

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

Slice 2: the source index data

def Q2Presentation.Induction.MStage.mstageSrc {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Sec7FrattiniTrivialElementaryMStageSourceIndexData (mstageChild chief K) (sec7MStageCanonicalMultiplicityData K (mstageChild chief K))

The realized source indexes: the parent surjection sets themselves.

Equations

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

Slice 3: the exact-image classification of all lifts

@[reducible, inline]

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

The lower child in transparent form (instance-friendly).

Equations

• Q2Presentation.Induction.MStage.mstageLower chief K = ⟨Q2Presentation.TorsorProgram.quotientFramedTarget p.fst K.Ksub ⋯ ⋯, Q2Presentation.TorsorProgram.quotientFrame p.fst K.Ksub ⋯ ⋯ p.snd⟩

theorem Q2Presentation.Induction.MStage.mstageChild_lower_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (mstageChild chief K).lowerChild = mstageLower chief K

def Q2Presentation.Induction.MStage.TotalLift {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) : Type

The total lift space over the M-layer child.

Equations

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

theorem Q2Presentation.Induction.MStage.totalLift_range_sup {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (t : TotalLift chief K B) : (ProfiniteGrp.Hom.hom ↑t.snd).range ⊔ K.Ksub = ⊤

The image subgroup of a lift covers C.

def Q2Presentation.Induction.MStage.rangeOf {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (t : TotalLift chief K B) : Subgroup p.fst.Y

The range subgroup of a lift.

Equations

• Q2Presentation.Induction.MStage.rangeOf chief K B t = (ProfiniteGrp.Hom.hom ↑t.snd).range

def Q2Presentation.Induction.MStage.imgY {p : FramedPair} {J : Subgroup p.fst.Y} {hJ : Function.Surjective ⇑(p.fst.piY.comp J.subtype)} (x : ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (p.fst.exactImageTarget J hJ).Y)).toProfinite.toTop) : p.fst.Y

Carrier cast for exact-image values (direct subtype application).

Equations

• Q2Presentation.Induction.MStage.imgY x = J.subtype x

theorem Q2Presentation.Induction.MStage.imgY_mem {p : FramedPair} {J : Subgroup p.fst.Y} {hJ : Function.Surjective ⇑(p.fst.piY.comp J.subtype)} (x : ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (p.fst.exactImageTarget J hJ).Y)).toProfinite.toTop) : imgY x ∈ J

theorem Q2Presentation.Induction.MStage.imgY_one {p : FramedPair} {J : Subgroup p.fst.Y} {hJ : Function.Surjective ⇑(p.fst.piY.comp J.subtype)} : imgY 1 = 1

theorem Q2Presentation.Induction.MStage.imgY_mul {p : FramedPair} {J : Subgroup p.fst.Y} {hJ : Function.Surjective ⇑(p.fst.piY.comp J.subtype)} (a b : ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (p.fst.exactImageTarget J hJ).Y)).toProfinite.toTop) : imgY (a * b) = imgY a * imgY b

def Q2Presentation.Induction.MStage.corestrict {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (t : TotalLift chief K B) (hJ : rangeOf chief K B t ⊔ K.Ksub = ⊤) : boundaryFramedSurj B (p.fst.exactImageTarget (rangeOf chief K B t) ⋯) (p.fst.exactImageFrame (rangeOf chief K B t) ⋯ p.snd)

Corestriction to the range.

Equations

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

def Q2Presentation.Induction.MStage.ofImageSurj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (J : Subgroup p.fst.Y) (hJ : J ⊔ K.Ksub = ⊤) (fj : boundaryFramedSurj B (p.fst.exactImageTarget J ⋯) (p.fst.exactImageFrame J ⋯ p.snd)) : TotalLift chief K B

Equations

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

theorem Q2Presentation.Induction.MStage.rangeOf_ofImageSurj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (J : Subgroup p.fst.Y) (hJ : J ⊔ K.Ksub = ⊤) (fj : boundaryFramedSurj B (p.fst.exactImageTarget J ⋯) (p.fst.exactImageFrame J ⋯ p.snd)) : rangeOf chief K B (ofImageSurj chief K B J hJ fj) = J

Range of the composed lift is J itself.

def Q2Presentation.Induction.MStage.ClassTarget {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) : Type

The classification target.

Equations

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

noncomputable def Q2Presentation.Induction.MStage.readLift {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (x : ClassTarget chief K B) : ↑Γ.toProfinite.toTop → ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of p.fst.Y)).toProfinite.toTop

Uniform lift-readout from the classification target.

Equations

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

noncomputable def Q2Presentation.Induction.MStage.classifyFun {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (t : TotalLift chief K B) : ClassTarget chief K B

The classification map.

Equations

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

theorem Q2Presentation.Induction.MStage.readLift_classify {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (t : TotalLift chief K B) : readLift chief K B (classifyFun chief K B t) = fun (γ : ↑Γ.toProfinite.toTop) => (ProfiniteGrp.Hom.hom ↑t.snd) γ

The readout retracts the classification onto the underlying lift.

theorem Q2Presentation.Induction.MStage.classTarget_inr_ext {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) {J J' : Subgroup p.fst.Y} (hJJ : J = J') (hne : J ≠ ⊤) (hsup : J ⊔ K.Ksub = ⊤) (hne' : J' ≠ ⊤) (hsup' : J' ⊔ K.Ksub = ⊤) (fj : boundaryFramedSurj B (p.fst.exactImageTarget J ⋯) (p.fst.exactImageFrame J ⋯ p.snd)) (fj' : boundaryFramedSurj B (p.fst.exactImageTarget J' ⋯) (p.fst.exactImageFrame J' ⋯ p.snd)) (hval : ∀ (γ : ↑Γ.toProfinite.toTop), imgY ((ProfiniteGrp.Hom.hom (↑fj).hom) γ) = imgY ((ProfiniteGrp.Hom.hom (↑fj').hom) γ)) : ⟨⟨J, ⋯⟩, fj⟩ = ⟨⟨J', ⋯⟩, fj'⟩

Extensionality across the dependent image-index (subst-legal form).

noncomputable def Q2Presentation.Induction.MStage.classify {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) : TotalLift chief K B ≃ ClassTarget chief K B

The exact-image classification of total lifts.

Equations

• Q2Presentation.Induction.MStage.classify chief K B = Equiv.ofBijective (Q2Presentation.Induction.MStage.classifyFun chief K B) ⋯

Slice 4: the counts

theorem Q2Presentation.Induction.MStage.sec7_mstage_cochainData {p : FramedPair} (h : ¬ScalarTerminal p) (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : (∀ (g : boundaryFramedSurj boundaryPackage_GammaA (mstageLower chief K).fst (mstageLower chief K).snd), Nonempty (TorsorProgram.liftHom p.fst K.Ksub ⋯ ⋯ boundaryPackage_GammaA p.snd g)) ∧ (∀ (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst K.Ksub ⋯ ⋯) (TorsorProgram.quotientFrame p.fst K.Ksub ⋯ ⋯ p.snd)) (f₀ : TorsorProgram.liftHom p.fst K.Ksub ⋯ ⋯ boundaryPackage_GammaA p.snd g), Nat.card (TorsorProgram.Z1 p.fst K.Ksub ⋯ ⋯ boundaryPackage_GammaA p.snd g f₀) = 2 ^ (2 * sec7MStageDim K)) ∧ (∀ (g : boundaryFramedSurj boundaryPackage_GQ2 (mstageLower chief K).fst (mstageLower chief K).snd), Nonempty (TorsorProgram.liftHom p.fst K.Ksub ⋯ ⋯ boundaryPackage_GQ2 p.snd g)) ∧ ∀ (g : boundaryFramedSurj boundaryPackage_GQ2 (TorsorProgram.quotientFramedTarget p.fst K.Ksub ⋯ ⋯) (TorsorProgram.quotientFrame p.fst K.Ksub ⋯ ⋯ p.snd)) (f₀ : TorsorProgram.liftHom p.fst K.Ksub ⋯ ⋯ boundaryPackage_GQ2 p.snd g), Nat.card (TorsorProgram.Z1 p.fst K.Ksub ⋯ ⋯ boundaryPackage_GQ2 p.snd g f₀) = 2 ^ (2 * sec7MStageDim K)

The M-layer cochain keep (lem:elementarystage, manuscript l.4170-4204): per source, every lower-child framed surjection admits a framed lift (H²_{Γ,ρ}(M) = 0) and the twisted cocycle set has the canonical size |Z¹_{Γ,ρ}(M)| = 2^{2·dim M}. Canonical-provenance existence-form.

theorem Q2Presentation.Induction.MStage.totalLift_card_torsor {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) [hfinC : Finite (boundaryFramedSurj B (mstageLower chief K).fst (mstageLower chief K).snd)] [hfinT : ∀ (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget p.fst K.Ksub ⋯ ⋯) (TorsorProgram.quotientFrame p.fst K.Ksub ⋯ ⋯ p.snd)), Finite (TorsorProgram.liftHom p.fst K.Ksub ⋯ ⋯ B p.snd g)] (hne : ∀ (g : boundaryFramedSurj B (mstageLower chief K).fst (mstageLower chief K).snd), Nonempty (TorsorProgram.liftHom p.fst K.Ksub ⋯ ⋯ B p.snd g)) (hcnt : ∀ (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget p.fst K.Ksub ⋯ ⋯) (TorsorProgram.quotientFrame p.fst K.Ksub ⋯ ⋯ p.snd)) (f₀ : TorsorProgram.liftHom p.fst K.Ksub ⋯ ⋯ B p.snd g), Nat.card (TorsorProgram.Z1 p.fst K.Ksub ⋯ ⋯ B p.snd g f₀) = 2 ^ (2 * sec7MStageDim K)) : Nat.card (TotalLift chief K B) = 2 ^ (2 * sec7MStageDim K) * Nat.card (boundaryFramedSurj B (mstageLower chief K).fst (mstageLower chief K).snd)

The torsor count of the total lift space.

theorem Q2Presentation.Induction.MStage.totalLift_card_classified {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) [hfinP : Finite (boundaryFramedSurj B p.fst p.snd)] [hfinS : Finite ((Jc : { J : Subgroup p.fst.Y // J ≠ ⊤ ∧ J ⊔ K.Ksub = ⊤ }) × boundaryFramedSurj B (p.fst.exactImageTarget ↑Jc ⋯) (p.fst.exactImageFrame ↑Jc ⋯ p.snd))] : Nat.card (TotalLift chief K B) = Nat.card (boundaryFramedSurj B p.fst p.snd) + Nat.card ((Jc : { J : Subgroup p.fst.Y // J ≠ ⊤ ∧ J ⊔ K.Ksub = ⊤ }) × boundaryFramedSurj B (p.fst.exactImageTarget ↑Jc ⋯) (p.fst.exactImageFrame ↑Jc ⋯ p.snd))

The classified count of the total lift space.

Slice 4b: the partition packet, proven

theorem Q2Presentation.Induction.MStage.finite_liftHom_A {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (g : boundaryFramedSurj boundaryPackage_GammaA (mstageLower chief K).fst (mstageLower chief K).snd) : Finite (TorsorProgram.liftHom p.fst K.Ksub ⋯ ⋯ boundaryPackage_GammaA p.snd g)

Finiteness of all lift sets for the candidate source.

theorem Q2Presentation.Induction.MStage.finite_liftHom_Q {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (g : boundaryFramedSurj boundaryPackage_GQ2 (mstageLower chief K).fst (mstageLower chief K).snd) : Finite (TorsorProgram.liftHom p.fst K.Ksub ⋯ ⋯ boundaryPackage_GQ2 p.snd g)

Finiteness of all lift sets for the local source.

theorem Q2Presentation.Induction.MStage.proper_sum_tie {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (count : FramedPair → Cardinal.{u_1}) [hfinS : ∀ (Jc : { J : Subgroup p.fst.Y // J ≠ ⊤ ∧ J ⊔ K.Ksub = ⊤ }), Finite (boundaryFramedSurj B (p.fst.exactImageTarget ↑Jc ⋯) (p.fst.exactImageFrame ↑Jc ⋯ p.snd))] (hcount : ∀ (Jc : { J : Subgroup p.fst.Y // J ≠ ⊤ ∧ J ⊔ K.Ksub = ⊤ }), count ⟨p.fst.exactImageTarget ↑Jc ⋯, p.fst.exactImageFrame ↑Jc ⋯ p.snd⟩ = ↑(Nat.card (boundaryFramedSurj B (p.fst.exactImageTarget ↑Jc ⋯) (p.fst.exactImageFrame ↑Jc ⋯ p.snd)))) : (List.map (⇑Cardinal.toNat) (List.map count (mstageChild chief K).properChildren)).sum = Nat.card ((Jc : { J : Subgroup p.fst.Y // J ≠ ⊤ ∧ J ⊔ K.Ksub = ⊤ }) × boundaryFramedSurj B (p.fst.exactImageTarget ↑Jc ⋯) (p.fst.exactImageFrame ↑Jc ⋯ p.snd))

The proper-sum tie: the sigma-count equals the recorded children-list sum.

Slice 4c: the packet, proven; the branch, rewired

theorem Q2Presentation.Induction.MStage.hcountA_bridge {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Jc : { J : Subgroup p.fst.Y // J ≠ ⊤ ∧ J ⊔ K.Ksub = ⊤ }) : framedCountA ⟨p.fst.exactImageTarget ↑Jc ⋯, p.fst.exactImageFrame ↑Jc ⋯ p.snd⟩ = ↑(Nat.card (boundaryFramedSurj boundaryPackage_GammaA (p.fst.exactImageTarget ↑Jc ⋯) (p.fst.exactImageFrame ↑Jc ⋯ p.snd)))

Per-image count bridges.

theorem Q2Presentation.Induction.MStage.hcountQ_bridge {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Jc : { J : Subgroup p.fst.Y // J ≠ ⊤ ∧ J ⊔ K.Ksub = ⊤ }) : framedCountQ ⟨p.fst.exactImageTarget ↑Jc ⋯, p.fst.exactImageFrame ↑Jc ⋯ p.snd⟩ = ↑(Nat.card (boundaryFramedSurj boundaryPackage_GQ2 (p.fst.exactImageTarget ↑Jc ⋯) (p.fst.exactImageFrame ↑Jc ⋯ p.snd)))

theorem Q2Presentation.Induction.MStage.partitionPacket_proven {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (h : ¬ScalarTerminal p) (hR : Nat.card ↥(kernelFrattini K) = 1) : Nonempty ((child : Sec7FrattiniTrivialElementaryChildData p) ×' (src : Sec7FrattiniTrivialElementaryMStageSourceIndexData child (sec7MStageCanonicalMultiplicityData K child)) ×' Sec7FrattiniTrivialElementaryMStageCandidateExactImagePartitionCanonicalFinSigmaPartitionCardData child (sec7MStageCanonicalMultiplicityData K child) src ×' Sec7FrattiniTrivialElementaryMStageLocalExactImagePartitionCanonicalFinSigmaPartitionCardData child (sec7MStageCanonicalMultiplicityData K child) src)

The eq:Mstage partition packet, PROVEN.

theorem Q2Presentation.Induction.MStage.sec7_fourierBranch_of_frattiniTrivial_proven {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (h : ¬ScalarTerminal p) (hR : Nat.card ↥(kernelFrattini K) = 1) : Nonempty (FourierBranchData p)

The R = 1 branch over the PROVEN packet (clone chain).