Actual target marked-quotient closers

This sidecar keeps the §8 target quotient route tied to the manuscript tower

Y -> B = Y/R -> C = Y/K.

The older split packets in TargetMarkedQuotientClosers separated map existence, kernel identification, and quotient-map agreement. Here the marked restriction residuals are replaced by actual provenance packets: the selected marked maps are required to be the restrictions of the already constructed ambient quotient maps Q.topToMiddle and Q.middleToLower.

The quotient-child split packets are theorem-level projections of the existing canonical quotient data. The middle-kernel image packet is constructed from the quotient-map tower itself.

Canonical quotient children

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

The middle quotient target Y/R follows by projecting the existing canonical quotient packet.

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

The lower quotient target Y/K follows by projecting the existing canonical quotient packet.

theorem Q2Presentation.Induction.centralCover_targetQuotientChildConcreteData_from_actualClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetQuotientChildConcreteData B (targetSubgroupTowerData_of_concrete B D))

Concrete quotient-child data assembled through the canonical quotient packet, without the split middle/lower quotient axioms.

Actual marked restrictions

structure Q2Presentation.Induction.CentralCoverTargetActualTopMarkedRestrictionData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Type

Actual top marked restriction of Y -> B = Y/R.

This is the narrow provenance packet replacing the old pair centralCover_targetTopMarkedRestrictionData and centralCover_targetTopMarkedKernelOfRestrictionData: the marked map is not arbitrary, but agrees with the ambient quotient map Q.topToMiddle.

• topMarkedMap : ↥p.fst.LY →* ↥Q.middleChild.fst.LY
• topMarkedMap_surj : Function.Surjective ⇑self.topMarkedMap
• topMarkedMap_agrees (x : ↥p.fst.LY) : ↑(self.topMarkedMap x) = Q.topToMiddle ↑x
• topMarkedKernelEquivR : ↥self.topMarkedMap.ker ≃* ↥S.Rsub

structure Q2Presentation.Induction.CentralCoverTargetActualMiddleMarkedRestrictionData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Type

Actual middle marked restriction of B = Y/R -> C = Y/K.

This is the narrow provenance packet replacing the old pair centralCover_targetMiddleMarkedRestrictionData and centralCover_targetMiddleMarkedKernelOfRestrictionData.

• middleMarkedMap : ↥Q.middleChild.fst.LY →* ↥Q.lowerChild.fst.LY
• middleMarkedMap_surj : Function.Surjective ⇑self.middleMarkedMap
• middleMarkedMap_agrees (x : ↥Q.middleChild.fst.LY) : ↑(self.middleMarkedMap x) = Q.middleToLower ↑x
• middleMarkedKernelEquiv : ↥self.middleMarkedMap.ker ≃* ↥Q.middleToLower.ker

axiom Q2Presentation.Induction.centralCover_targetActualTopMarkedRestrictionData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetActualTopMarkedRestrictionData B S Q)

Actual residual: construct the marked restriction of Y -> Y/R.

axiom Q2Presentation.Induction.centralCover_targetActualMiddleMarkedRestrictionData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetActualMiddleMarkedRestrictionData B S Q)

Actual residual: construct the marked restriction of Y/R -> Y/K.

def Q2Presentation.Induction.targetTopMarkedRestrictionData_of_actual {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetActualTopMarkedRestrictionData B S Q) : CentralCoverTargetTopMarkedRestrictionData B S Q

Equations

• Q2Presentation.Induction.targetTopMarkedRestrictionData_of_actual B S Q D = { topMarkedMap := D.topMarkedMap, topMarkedMap_surj := ⋯, topMarkedMap_agrees := ⋯ }

def Q2Presentation.Induction.targetTopMarkedKernelOfRestrictionData_of_actual {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetActualTopMarkedRestrictionData B S Q) : CentralCoverTargetTopMarkedKernelOfRestrictionData B S Q (targetTopMarkedRestrictionData_of_actual B S Q D)

Equations

• Q2Presentation.Induction.targetTopMarkedKernelOfRestrictionData_of_actual B S Q D = { topMarkedKernelEquivR := D.topMarkedKernelEquivR }

def Q2Presentation.Induction.targetMiddleMarkedRestrictionData_of_actual {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetActualMiddleMarkedRestrictionData B S Q) : CentralCoverTargetMiddleMarkedRestrictionData B S Q

Equations

• Q2Presentation.Induction.targetMiddleMarkedRestrictionData_of_actual B S Q D = { middleMarkedMap := D.middleMarkedMap, middleMarkedMap_surj := ⋯, middleMarkedMap_agrees := ⋯ }

def Q2Presentation.Induction.targetMiddleMarkedKernelOfRestrictionData_of_actual {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetActualMiddleMarkedRestrictionData B S Q) : CentralCoverTargetMiddleMarkedKernelOfRestrictionData B S Q (targetMiddleMarkedRestrictionData_of_actual B S Q D)

Equations

• Q2Presentation.Induction.targetMiddleMarkedKernelOfRestrictionData_of_actual B S Q D = { middleMarkedKernelEquiv := D.middleMarkedKernelEquiv }

theorem Q2Presentation.Induction.centralCover_targetTopMarkedRestrictionData_from_actualClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetTopMarkedRestrictionData B S Q)

Top marked restriction theorem-level from the actual provenance packet.

theorem Q2Presentation.Induction.centralCover_targetTopMarkedExactData_from_actualClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetTopMarkedExactData B S Q)

Top marked exactness assembled through the actual restriction packet.

theorem Q2Presentation.Induction.centralCover_targetMiddleMarkedRestrictionData_from_actualClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetMiddleMarkedRestrictionData B S Q)

Middle marked restriction theorem-level from the actual provenance packet.

theorem Q2Presentation.Induction.centralCover_targetMiddleMarkedExactData_from_actualClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetMiddleMarkedExactData B S Q)

Middle marked exactness assembled through the actual restriction packet.

Middle kernel image

def Q2Presentation.Induction.targetMiddleKernelImageData_of_childEquivs {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (D : CentralCoverTargetQuotientChildEquivData B S) : CentralCoverTargetMiddleKernelImageData B S (targetQuotientMapsData_of_childEquivs B S D)

For the actual quotient-map packet built from quotient equivalences, the middle kernel is the canonical image of K in Y/R.

This is the manuscript identity ker(B -> C) = K/R, proved here from the quotient-map constructor and TargetTowerClosers.quotientMapOfLEHom_ker.

Equations

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

theorem Q2Presentation.Induction.centralCover_targetMiddleKernelImageData_from_childEquivs_actualClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (D : CentralCoverTargetQuotientChildEquivData B S) : Nonempty (CentralCoverTargetMiddleKernelImageData B S (targetQuotientMapsData_of_childEquivs B S D))

Middle-kernel image data from the actual quotient child equivalences.

theorem Q2Presentation.Induction.centralCover_targetMiddleKernelImageHomData_from_childEquivs_actualClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (D : CentralCoverTargetQuotientChildEquivData B S) : Nonempty (CentralCoverTargetMiddleKernelImageHomData B S (targetQuotientMapsData_of_childEquivs B S D))

Split comparison hom for the actual quotient-map packet built from child equivalences.

theorem Q2Presentation.Induction.centralCover_targetMiddleKernelImageBijectiveData_from_childEquivs_actualClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (D : CentralCoverTargetQuotientChildEquivData B S) : Nonempty (CentralCoverTargetMiddleKernelImageBijectiveData B S (targetQuotientMapsData_of_childEquivs B S D) (targetMiddleKernelImageHomData_of_imageData B S (targetQuotientMapsData_of_childEquivs B S D) (targetMiddleKernelImageData_of_childEquivs B S D)))

Bijectivity of the split comparison hom for the actual quotient-map packet built from child equivalences.

theorem Q2Presentation.Induction.centralCover_targetMiddleKernelIdentificationData_from_childEquivs_actualClosers {p : FramedPair} (B : MinimalBlock p) (Dsub : CentralCoverTargetSubgroupConcreteData B) (D : CentralCoverTargetQuotientChildEquivData B (targetSubgroupTowerData_of_concrete B Dsub)) : Nonempty (CentralCoverTargetMiddleKernelIdentificationData B (targetSubgroupTowerData_of_concrete B Dsub) (targetQuotientMapsData_of_childEquivs B (targetSubgroupTowerData_of_concrete B Dsub) D))

Middle-kernel identification for the actual quotient-map packet built from canonical child equivalences, using the concrete K/R ~= M bridge.

Final route

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

Canonical target quotient data for a block built from a Section 7 group tower, routed through actual marked restrictions.

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

Cover realization through actual target marked-quotient closers.

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

Nonterminal Fourier branch through actual target marked-quotient closers.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_actualClosers (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)

Recursive branch through actual target marked-quotient closers.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_actualClosers (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)

Recursion step through actual target marked-quotient closers.

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

Boundary-framed counts equal through actual target marked-quotient closers.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_targetMarkedQuotientActualClosers (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)))

Equal finite surjection counts through actual target marked-quotient closers.