Target-tower residual split for Section 8

This sidecar refines the two remaining target-side elementary-stage packets in ElementaryStageResiduals.lean.

Manuscript anchors:

• eq:targettower: R = Phi(K) <= K <= L_Y, with quotient maps Y -> B = Y/R -> C = Y/K;
• eq:Mstage / eq:Mdescent: proper exact-image subgroups J < B mapping onto C, with |J ∩ L_B| = |J ∩ M| |L_C| and 2 |J ∩ M| <= |M|.

The current MinimalBlock API is module-level: it supplies R, M, T, the simple head, and obstruction-space data, but it still does not construct the realized normal subgroups and quotient maps inside an arbitrary finite target. Accordingly this file does not claim a full de-axiomatization. It strictly refines the two live target residuals into concrete finite group packets and proves the exact reassembly theorems needed by the existing elementary-stage interfaces.

Target tower R <= K <= L_Y

structure Q2Presentation.Induction.CentralCoverTargetSubgroupTowerData {p : FramedPair} (B : MinimalBlock p) : Type

The subgroup part of the manuscript target tower.

This is the concrete finite-group content before quotient targets are attached: R = Phi(K), R <= K <= L_Y, both normal in Y, and R nontrivial so that the middle quotient is strictly smaller.

• Rsub : Subgroup p.fst.Y

  The realized subgroup R = Phi(K) of the original finite target Y.

• Ksub : Subgroup p.fst.Y

  The realized subgroup K of the original finite target Y.

• Rsub_normal : self.Rsub.Normal

  R is normal in Y.

• Ksub_normal : self.Ksub.Normal

  K is normal in Y.

• Rsub_le_Ksub : self.Rsub ≤ self.Ksub

  Manuscript tower condition R <= K.

• Ksub_le_LY : self.Ksub ≤ p.fst.LY

  Manuscript tower condition K <= L_Y.

• Rsub_card_gt_one : 1 < Nat.card ↥self.Rsub

  The realized R is nontrivial.

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

Quotient targets and maps for the manuscript tower Y -> B -> C.

This packet contains the boundary-framed quotient targets and quotient maps, but not the cardinal equalities.

• middleChild : FramedPair

  The quotient target B = Y/R.

• lowerChild : FramedPair

  The lower quotient target C = Y/K.

• topToMiddle : p.fst.Y →* self.middleChild.fst.Y

  The quotient map Y -> B = Y/R.

• topToMiddle_surj : Function.Surjective ⇑self.topToMiddle

  The map Y -> B is onto.

• topToMiddle_ker : self.topToMiddle.ker = S.Rsub

  The map Y -> B has kernel R.

• topToLower : p.fst.Y →* self.lowerChild.fst.Y

  The quotient map Y -> C = Y/K.

• topToLower_surj : Function.Surjective ⇑self.topToLower

  The map Y -> C is onto.

• topToLower_ker : self.topToLower.ker = S.Ksub

  The map Y -> C has kernel K.

• middleToLower : self.middleChild.fst.Y →* self.lowerChild.fst.Y

  The quotient map B -> C.

• middleToLower_surj : Function.Surjective ⇑self.middleToLower

  The map B -> C is onto.

• quotient_commutes : self.middleToLower.comp self.topToMiddle = self.topToLower

  The quotient maps commute.

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

Cardinal equalities for the quotient tower.

These are the finite cardinal statements used by lem:strictdecrease and eq:Mdescent: the kernel of B -> C has the size of the elementary layer, and the marked-kernel measures factor as in the manuscript.

• middle_kernel_card : Nat.card ↥Q.middleToLower.ker = Nat.card B.M

  |ker(B -> C)| = |M|.

• middle_measure_mul_Rcard : framedMeasure Q.middleChild * Nat.card ↥S.Rsub = framedMeasure p

  Manuscript |L_B| |R| = |L_Y|.

• middle_measure_eq : framedMeasure Q.middleChild = Nat.card B.M * framedMeasure Q.lowerChild

  Manuscript |L_B| = |M| |L_C|.

def Q2Presentation.Induction.elementaryQuotientTowerData_of_targetPackets {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (C : CentralCoverTargetTowerCardinalityData B S Q) : CentralCoverElementaryQuotientTowerData B

Reassemble the existing quotient-tower interface from the smaller target tower packets.

Equations

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

def Q2Presentation.Induction.targetTowerRealizationData_of_targetPackets {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (C : CentralCoverTargetTowerCardinalityData B S Q) : CentralCoverTargetTowerRealizationData B

Reassemble the exact target-tower realization packet from subgroup, quotient, and cardinality data.

Equations

• Q2Presentation.Induction.targetTowerRealizationData_of_targetPackets B S Q C = { tower := Q2Presentation.Induction.elementaryQuotientTowerData_of_targetPackets B S Q C, Ksub_le_LY := ⋯ }

axiom Q2Presentation.Induction.centralCover_targetSubgroupTowerData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverTargetSubgroupTowerData B)

Refined residual: construct the concrete subgroup tower R = Phi(K) <= K <= L_Y.

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

Refined residual: construct the quotient targets and quotient maps Y -> B = Y/R -> C = Y/K for a fixed subgroup tower.

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

Refined residual: prove the cardinal identities attached to a fixed quotient tower.

theorem Q2Presentation.Induction.centralCover_targetTowerRealizationData_from_packets {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverTargetTowerRealizationData B)

Exact replacement theorem for centralCover_targetTowerRealizationData, assembled from smaller packets.

theorem Q2Presentation.Induction.centralCover_elementaryQuotientTowerData_from_packets {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryQuotientTowerData B)

Quotient-tower replacement theorem assembled from the same smaller packets.

theorem Q2Presentation.Induction.centralCover_elementaryLowerTarget_from_packets {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryLowerTarget B)

Lower-target replacement theorem assembled from the refined target packets.

Proper exact-image cardinality data

structure Q2Presentation.Induction.CentralCoverElementaryProperImageKernelSubgroupData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Type

Concrete kernel-part subgroups for the proper exact-image terms in eq:Mdescent.

For each canonical proper exact-image subgroup J < B mapping onto C, this packet names the finite subgroup that represents J ∩ M inside ker(B -> C), and records the index-at-least-two bound on its cardinality.

• kernelPart : CentralCoverElementaryProperExactImageSubgroups T → Subgroup ↥T.middleToLower.ker

  The concrete subgroup corresponding to J ∩ M.

• kernelPart_bound (i : CentralCoverElementaryProperExactImageSubgroups T) : 2 * Nat.card ↥(self.kernelPart i) ≤ Nat.card B.M

  Properness of J gives 2 |J ∩ M| <= |M|.

structure Q2Presentation.Induction.CentralCoverElementaryProperImageExactSequenceData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) : Prop

Exact-sequence cardinality for the proper-image terms.

This is the concrete 1 -> J ∩ M -> J ∩ L_B -> L_C -> 1 calculation from eq:Mdescent, stated after the kernel-part subgroup has been chosen.

• child_measure_eq (i : CentralCoverElementaryProperExactImageSubgroups T) : framedMeasure (elementaryExactImageChild T.middleChild ↑i ⋯) = Nat.card ↥(K.kernelPart i) * framedMeasure T.lowerChild

  Manuscript |J ∩ L_B| = |J ∩ M| |L_C|.

def Q2Presentation.Induction.elementaryProperImageCardinalityData_of_kernelExact {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) (E : CentralCoverElementaryProperImageExactSequenceData B T K) : CentralCoverElementaryProperImageCardinalityData B T

Reassemble the existing cardinality packet from a concrete kernel-part choice and the exact-sequence cardinality statement.

Equations

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

axiom Q2Presentation.Induction.centralCover_elementaryProperImageKernelSubgroupData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageKernelSubgroupData B T)

Refined residual: choose the concrete kernel-part subgroups J ∩ M and prove the proper-subspace cardinal bound.

axiom Q2Presentation.Induction.centralCover_elementaryProperImageExactSequenceData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) : Nonempty (CentralCoverElementaryProperImageExactSequenceData B T K)

Refined residual: prove the exact-sequence cardinality calculation for a fixed kernel-part choice.

theorem Q2Presentation.Induction.centralCover_elementaryProperImageCardinalityData_from_packets {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageCardinalityData B T)

Exact replacement theorem for centralCover_elementaryProperImageCardinalityData, assembled from smaller proper-image packets.

theorem Q2Presentation.Induction.centralCover_elementaryProperImageFamilyData_from_packets {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageFamilyData B T)

Proper-image family replacement theorem assembled from the smaller packets.

Reassembly to the Section 8 child/realization interfaces

theorem Q2Presentation.Induction.centralCover_elementaryProperImageChildrenData_from_packets {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryProperImageChildrenData B)

Elementary proper-image child packet assembled from the refined target and proper-image packets.

theorem Q2Presentation.Induction.centralCover_elementaryStageChildren_from_towerPackets {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryStageChildren B)

Elementary-stage children assembled without using the two old target-side elementary residual axioms.

theorem Q2Presentation.Induction.centralCover_elementaryChildren_from_towerPackets {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverChildStratum B)

Elementary child stratum assembled from the refined target/proper-image packets.

theorem Q2Presentation.Induction.centralCover_childrenData_from_towerPackets {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverChildrenData B)

Full Section 8 children data assembled with the refined elementary target packets and the existing theorem-level empty scalar/phase strata.

theorem Q2Presentation.Induction.centralCover_partialRecipe_fine_from_towerPackets {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) : Nonempty (CentralCoverPartialRecipe B T)

Partial recipe reassembled with the refined target-tower/proper-image packets.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_towerPackets {p : FramedPair} (B : MinimalBlock p) : Nonempty (CoverRealization B)

Cover-realization replacement theorem whose target-side closure names the new target-tower/proper-image packets rather than the two old packets in ElementaryStageResiduals.lean.