Target framed marked-quotient proofs

This sidecar closes the routed centralCover_targetFramedMarkedQuotientData packet down to the strictly smaller manuscript packet centralCover_targetCanonicalFramedQuotientData.

The narrower packet already says that the quotient children realizing Y/R and Y/K carry the inherited marked kernels:

• L_B is the image of L_Y in Y/R;
• L_C is the image of L_Y in Y/K.

From those image equalities, the ambient quotient maps restrict surjectively to the marked kernels, and the middle ambient kernel is marked because it is K/R and K <= L_Y.

Marked restriction data from inherited marked quotient children

def Q2Presentation.Induction.targetTopMarkedRestrictionSurjData_of_framedQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (F : CentralCoverTargetCanonicalFramedQuotientData B D) : CentralCoverTargetTopMarkedRestrictionSurjData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D F)

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.targetMiddleMarkedRestrictionSurjData_of_framedQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (F : CentralCoverTargetCanonicalFramedQuotientData B D) : CentralCoverTargetMiddleMarkedRestrictionSurjData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D F)

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.targetMiddleAmbientKernelMarkedData_of_framedQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (F : CentralCoverTargetCanonicalFramedQuotientData B D) : CentralCoverTargetMiddleAmbientKernelMarkedData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D F)

Equations

• ⋯ = ⋯

Closure of the routed coherent packet to the smaller quotient packet

theorem Q2Presentation.Induction.centralCover_targetFramedMarkedQuotientData_proven {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetFramedMarkedQuotientData B D)

Route-ready reassembly through the refined packet

theorem Q2Presentation.Induction.centralCover_targetCanonicalQuotientTowerData_from_selfGroupTower_targetFramedMarkedQuotientProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) : Nonempty (CentralCoverTargetCanonicalQuotientTowerData (G.toMinimalBlock h Fdet A Rdet))

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerTargetFramedMarkedQuotientProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) : Nonempty (CoverRealization (G.toMinimalBlock h Fdet A Rdet))

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_targetFramedMarkedQuotientProofs (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_targetFramedMarkedQuotientProofs (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_targetFramedMarkedQuotientProofs (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_targetFramedMarkedQuotientProofs (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_targetFramedMarkedQuotientProofs (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))