Lower target marked-quotient proof packets

This sidecar is not imported by the routed theorem. It targets the six current Section 8 target-side residuals in TargetMarkedQuotientClosers.lean:

• centralCover_targetCanonicalMiddleQuotientData
• centralCover_targetCanonicalLowerQuotientData
• centralCover_targetTopMarkedRestrictionData
• centralCover_targetTopMarkedKernelOfRestrictionData
• centralCover_targetMiddleMarkedRestrictionData
• centralCover_targetMiddleMarkedKernelOfRestrictionData

Manuscript anchors:

• Section 7, eq:targettower: Y -> B = Y/R -> C = Y/K with R <= K <= L_Y;
• Section 8, eq:Mstage/eq:Mdescent: the marked-kernel restrictions L_Y -> L_B -> L_C.

The existing framed-target API does not yet construct quotient framed targets from a normal subgroup killed by the decoration. The lower packets below are therefore exactly the missing construction facts: the quotient children are framed quotient targets, and the ambient quotient maps restrict to the marked kernels. Once those are supplied, the top kernel is theorem-level from ker(Y -> B) = R, and the middle kernel is theorem-level from the single fact that ker(B -> C) lies in the middle marked kernel.

Framed quotient-target construction packets

structure Q2Presentation.Induction.CentralCoverTargetCanonicalFramedQuotientData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type 1

Framed quotient targets for the manuscript quotients Y/R and Y/K.

The final two fields record the genuinely framed part of the construction: the marked kernels of the quotient targets are the images of the original marked kernel under the quotient maps.

• middleChild : FramedPair
• lowerChild : FramedPair
• middleEquiv : p.fst.Y ⧸ D.Rsub ≃* self.middleChild.fst.Y
• lowerEquiv : p.fst.Y ⧸ D.Ksub ≃* self.lowerChild.fst.Y
• middleMarkedImage_eq : Subgroup.map self.middleEquiv.toMonoidHom (Subgroup.map (QuotientGroup.mk' D.Rsub) p.fst.LY) = self.middleChild.fst.LY
• lowerMarkedImage_eq : Subgroup.map self.lowerEquiv.toMonoidHom (Subgroup.map (QuotientGroup.mk' D.Ksub) p.fst.LY) = self.lowerChild.fst.LY

axiom Q2Presentation.Induction.centralCover_targetCanonicalFramedQuotientData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

Lower construction packet: build the framed quotient targets Y/R and Y/K, including their inherited marked kernels.

def Q2Presentation.Induction.targetCanonicalMiddleQuotientData_of_framedQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetCanonicalFramedQuotientData B D) : CentralCoverTargetCanonicalMiddleQuotientData B D

Equations

• Q2Presentation.Induction.targetCanonicalMiddleQuotientData_of_framedQuotient B D Q = { middleChild := Q.middleChild, middleEquiv := Q.middleEquiv }

def Q2Presentation.Induction.targetCanonicalLowerQuotientData_of_framedQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetCanonicalFramedQuotientData B D) : CentralCoverTargetCanonicalLowerQuotientData B D

Equations

• Q2Presentation.Induction.targetCanonicalLowerQuotientData_of_framedQuotient B D Q = { lowerChild := Q.lowerChild, lowerEquiv := Q.lowerEquiv }

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

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

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

Broad canonical quotient data reassembled from the framed quotient construction packet.

Ambient quotient maps restricted to marked kernels

def Q2Presentation.Induction.targetTopMarkedMapOfAmbient {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (hmarked : ∀ (x : ↥p.fst.LY), Q.topToMiddle ↑x ∈ Q.middleChild.fst.LY) : ↥p.fst.LY →* ↥Q.middleChild.fst.LY

Equations

• Q2Presentation.Induction.targetTopMarkedMapOfAmbient B S Q hmarked = { toFun := fun (x : ↥p.fst.LY) => ⟨Q.topToMiddle ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

def Q2Presentation.Induction.targetMiddleMarkedMapOfAmbient {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (hmarked : ∀ (x : ↥Q.middleChild.fst.LY), Q.middleToLower ↑x ∈ Q.lowerChild.fst.LY) : ↥Q.middleChild.fst.LY →* ↥Q.lowerChild.fst.LY

Equations

• Q2Presentation.Induction.targetMiddleMarkedMapOfAmbient B S Q hmarked = { toFun := fun (x : ↥Q.middleChild.fst.LY) => ⟨Q.middleToLower ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

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

Lower construction packet: the ambient quotient map Y -> B maps L_Y onto L_B.

• topToMiddle_maps_marked (x : ↥p.fst.LY) : Q.topToMiddle ↑x ∈ Q.middleChild.fst.LY
• topToMiddle_marked_surj : Function.Surjective ⇑(targetTopMarkedMapOfAmbient B S Q ⋯)

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

Lower construction packet: the ambient quotient map B -> C maps L_B onto L_C.

• middleToLower_maps_marked (x : ↥Q.middleChild.fst.LY) : Q.middleToLower ↑x ∈ Q.lowerChild.fst.LY
• middleToLower_marked_surj : Function.Surjective ⇑(targetMiddleMarkedMapOfAmbient B S Q ⋯)

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

Lower construction packet: every ambient middle-kernel element is marked. Together with agreement of the restricted map, this identifies the kernel of L_B -> L_C with the ambient kernel of B -> C.

• middleKernel_le_marked : Q.middleToLower.ker ≤ Q.middleChild.fst.LY

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

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

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

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

Equations

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

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

Equations

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

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

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

Kernel identifications from ambient quotient-map facts

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

Equations

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

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

def Q2Presentation.Induction.targetMiddleMarkedKernelOfRestrictionData_of_ambientKernelMarked {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleMarkedRestrictionData B S Q) (H : CentralCoverTargetMiddleAmbientKernelMarkedData B S Q) : CentralCoverTargetMiddleMarkedKernelOfRestrictionData B S Q D

Equations

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

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

Route-ready reassembly without the six split residual names

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

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

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

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

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

theorem Q2Presentation.Induction.centralCover_targetCanonicalQuotientTowerData_from_selfGroupTower_lowerProofs {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))

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerLowerProofs {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))

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

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_lowerProofs (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_lowerProofs (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_lowerProofs (p : FramedPair) : framedCountA p = framedCountQ p

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