Elementary-stage residuals for Section 8

This sidecar refines the two elementary-stage residuals in CentralCoverFineResiduals.lean.

The manuscript source is Section 8, especially eq:Mstage, eq:Mdescent, and lem:strictdecrease. The existing MinimalBlock p abstraction contains the module-level block data R, M, C, but it does not contain the realized normal subgroups R <= K <= Y, the quotient targets B = Y/R, C = Y/K, or the proper exact-image subgroups J < B. Consequently the old residuals

• centralCover_elementaryLowerTarget;
• centralCover_elementaryProperImageChildrenData;

cannot be manuscript-faithfully proved from the current fields alone. The packets below isolate exactly that missing finite group data, then reassemble the existing coarse elementary-stage interfaces from it.

Lower quotient C = Y/K

theorem Q2Presentation.Induction.framedMeasure_pos (p : FramedPair) : 0 < framedMeasure p

Every framed target has nonzero marked-kernel measure.

theorem Q2Presentation.Induction.minimalBlock_M_card_gt_one {p : FramedPair} (B : MinimalBlock p) : 1 < Nat.card B.M

The elementary layer M = K/R in a MinimalBlock is nontrivial.

This is not extra target-side data: it follows from the existing simple-head field Nontrivial (M/T).

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

A realized elementary quotient tower for eq:targettower.

This is the missing target-side finite group datum behind the lower term in eq:Mstage: the middle quotient B = Y/R, the lower quotient C = Y/K, and the map B -> C. The cardinal equations record the two quotient steps in a form that proves strict decrease.

The current MinimalBlock supplies the abstract modules, but not this realized quotient tower.

• 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

  The subgroup R is normal in Y, so Y/R is the middle quotient.

• Ksub_normal : self.Ksub.Normal

  The subgroup K is normal in Y, so Y/K is the lower quotient.

• Rsub_le_Ksub : self.Rsub ≤ self.Ksub

  The manuscript tower has R <= K <= Y.

• middleChild : FramedPair

  The quotient target B = Y/R on which the elementary M-stage is evaluated.

• 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 quotient map Y -> B is onto.

• topToMiddle_ker : self.topToMiddle.ker = self.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 quotient map Y -> C is onto.

• topToLower_ker : self.topToLower.ker = self.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: Y -> B -> C is the quotient Y -> C.

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

  The kernel of B -> C has the cardinality of the elementary layer M = K/R.

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

  The realized R is nontrivial, so the middle quotient is strictly lower.

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

  Manuscript |L_B| |R| = |L_Y| for the middle quotient.

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

  Manuscript |L_B| = |M| |L_C| for the elementary quotient B -> C.

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

A manuscript-realized version of the quotient tower.

The older CentralCoverElementaryQuotientTowerData is the exact interface needed by the recursion, but the paper constructs it from actual subgroups R = Phi(K) <= K <= L_Y and the quotient maps Y -> B = Y/R -> C = Y/K in eq:targettower. This packet records the extra semantic data that is needed before the quotient-tower theorem can be proved from finite group theory rather than assumed as a black box.

• tower : CentralCoverElementaryQuotientTowerData B
• Ksub_le_LY : self.tower.Ksub ≤ p.fst.LY

  The subgroup K lives inside the marked 2-kernel.

• middleKernelEquivM : ↥self.tower.middleToLower.ker ≃* Multiplicative B.M

  The kernel of B -> C is the realized elementary layer M = K/R.

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

The manuscript target tower R = Phi(K) <= K <= Y, before attaching the kernel equivalence ker(B -> C) ≃ M.

This is the smaller quotient-side packet needed by eq:Mstage: all quotient targets, quotient maps, commutativity, and cardinal identities are present in tower; the extra field records that K is inside the marked kernel. The remaining Frattini-surjectivity input is isolated on the candidate exact-image side, where it is actually consumed.

• tower : CentralCoverElementaryQuotientTowerData B
• Ksub_le_LY : self.tower.Ksub ≤ p.fst.LY

  The subgroup K lives inside the marked 2-kernel.

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

The separate identification of the elementary kernel with the abstract module M = K/R. This is not needed for the lower-target strict decrease, but it is the semantic bridge used by the manuscript proof of exact-image subtraction.

• middleKernelEquivM : ↥T.middleToLower.ker ≃* Multiplicative B.M

theorem Q2Presentation.Induction.middle_small_of_elementaryQuotientTower {p : FramedPair} {B : MinimalBlock p} (T : CentralCoverElementaryQuotientTowerData B) : framedMeasure T.middleChild < framedMeasure p

The middle quotient target from a realized elementary tower is strictly smaller.

theorem Q2Presentation.Induction.lower_small_of_elementaryQuotientTower {p : FramedPair} {B : MinimalBlock p} (T : CentralCoverElementaryQuotientTowerData B) : framedMeasure T.lowerChild < framedMeasure p

The lower quotient target from a realized elementary tower is strictly smaller.

def Q2Presentation.Induction.elementaryLowerTarget_of_quotientTower {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : CentralCoverElementaryLowerTarget B

Reassemble the existing lower-target interface from the realized quotient tower.

Equations

• Q2Presentation.Induction.elementaryLowerTarget_of_quotientTower B T = { lowerChild := T.lowerChild, lower_small := ⋯ }

axiom Q2Presentation.Induction.centralCover_targetTowerRealizationData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverTargetTowerRealizationData B)

Refined residual: construction of the manuscript-realized quotient tower R = Phi(K) <= K <= Y together with Y -> B = Y/R -> C = Y/K.

This is the exact target-side group-theory datum missing from the current MinimalBlock abstraction. It is smaller than the older realized-tower packet: the kernel equivalence ker(B -> C) ≃ M is isolated separately below.

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

Refined residual: identify the kernel of B -> C with the elementary module layer M = K/R.

theorem Q2Presentation.Induction.centralCover_realizedTowerData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverRealizedTowerData B)

The older realized-tower packet is reassembled from the quotient tower and the separate kernel equivalence.

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

The quotient-tower interface used by the recursion, projected from the manuscript-realized tower packet.

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

The old lower-target residual follows from the refined quotient-tower datum.

Proper exact-image children in eq:Mstage

def Q2Presentation.Induction.elementaryExactImageChild (middle : FramedPair) (J : Subgroup middle.fst.Y) (hJ : Function.Surjective ⇑(middle.fst.piY.comp J.subtype)) : FramedPair

The boundary-framed child induced by an exact-image subgroup of a framed target.

Equations

• Q2Presentation.Induction.elementaryExactImageChild middle J hJ = ⟨middle.fst.exactImageTarget J hJ, middle.fst.exactImageFrame J hJ middle.snd⟩

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

A finite family of proper exact-image subgroups J < B mapping onto C.

This is the proper-image subtraction family in eq:Mstage. Each child is constructed using the existing exact-image inheritance API from Boundary/FramedTarget.lean; the final cardinal fields record the exact-sequence calculation behind the manuscript estimate eq:Mdescent.

• properImages : Type
• finProperImages : Fintype self.properImages
• subgroup : self.properImages → Subgroup T.middleChild.fst.Y
• subgroup_surj (i : self.properImages) : Function.Surjective ⇑(T.middleChild.fst.piY.comp (self.subgroup i).subtype)

  Each proper image still projects onto the fixed tame quotient of the middle target.

• proper_subgroup (i : self.properImages) : self.subgroup i < ⊤

  Manuscript condition J < B.

• maps_onto_lower (i : self.properImages) : Function.Surjective ⇑(T.middleToLower.comp (self.subgroup i).subtype)

  Manuscript condition J -> C is onto.

• kernelPartCard : self.properImages → ℕ

  The cardinal |J ∩ M| in the exact sequence 1 -> J ∩ M -> J ∩ L_B -> L_C -> 1.

• kernelPart_bound (i : self.properImages) : 2 * self.kernelPartCard i ≤ Nat.card B.M

  Properness in the elementary abelian layer gives |J ∩ M| <= |M| / 2, recorded without division.

• child_measure_eq (i : self.properImages) : framedMeasure (elementaryExactImageChild T.middleChild (self.subgroup i) ⋯) = self.kernelPartCard i * framedMeasure T.lowerChild

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

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

The semantic proper-image family used in manuscript eq:Mdescent.

The list-based recursion only needs CentralCoverElementaryProperImageFamilyData, but the proof in the paper first identifies the kernel of B -> C with the elementary layer M and then enumerates proper exact-image subgroups J < B mapping onto C. This packet keeps that kernel identification attached to the family. The recursion below now uses the canonical exact-image subgroup index directly; this older packet remains as a semantic reassembly theorem.

• middleKernelEquivM : ↥T.middleToLower.ker ≃* Multiplicative B.M

  The exact sequence kernel ker(B -> C), realized as the module M.

• family : CentralCoverElementaryProperImageFamilyData B T

@[reducible, inline]

abbrev Q2Presentation.Induction.CentralCoverElementaryProperExactImageSubgroups {p : FramedPair} {B : MinimalBlock p} (T : CentralCoverElementaryQuotientTowerData B) : Type

The canonical finite index of proper exact-image subgroups in eq:Mstage.

An element is an actual subgroup J of the middle target B = Y/R, together with the manuscript conditions used in the elementary subtraction term: J < B, J inherits the fixed boundary frame, and J -> C is onto.

Equations

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

instance Q2Presentation.Induction.instFintypeCentralCoverElementaryProperExactImageSubgroups {p : FramedPair} {B : MinimalBlock p} (T : CentralCoverElementaryQuotientTowerData B) : Fintype (CentralCoverElementaryProperExactImageSubgroups T)

Equations

• Q2Presentation.Induction.instFintypeCentralCoverElementaryProperExactImageSubgroups T = id inferInstance

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

The remaining eq:Mdescent cardinal data on the canonical exact-image subgroup index.

The index set itself is now theorem-level finite data. This residual only records the exact-sequence cardinal calculation |J ∩ L_B| = |J ∩ M| |L_C| and the proper-subspace bound 2 |J ∩ M| <= |M|.

• kernelPartCard : CentralCoverElementaryProperExactImageSubgroups T → ℕ
• kernelPart_bound (i : CentralCoverElementaryProperExactImageSubgroups T) : 2 * self.kernelPartCard i ≤ Nat.card B.M
• child_measure_eq (i : CentralCoverElementaryProperExactImageSubgroups T) : framedMeasure (elementaryExactImageChild T.middleChild ↑i ⋯) = self.kernelPartCard i * framedMeasure T.lowerChild

def Q2Presentation.Induction.elementaryProperImageFamilyData_of_cardinality {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverElementaryProperImageCardinalityData B T) : CentralCoverElementaryProperImageFamilyData B T

Convert the canonical exact-image index plus eq:Mdescent cardinal data into the family interface used by the recursion.

Equations

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

theorem Q2Presentation.Induction.elementaryProperImageChild_small_of_family {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (F : CentralCoverElementaryProperImageFamilyData B T) (i : F.properImages) : framedMeasure (elementaryExactImageChild T.middleChild (F.subgroup i) ⋯) < framedMeasure p

Manuscript eq:Mdescent, proved from the finite exact-sequence cardinal data.

def Q2Presentation.Induction.elementaryProperImageChildrenData_of_family {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (F : CentralCoverElementaryProperImageFamilyData B T) : CentralCoverElementaryProperImageChildrenData B

Convert a finite exact-image family into the older list-based interface.

Equations

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

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

Refined residual: the exact-sequence cardinal calculation for the canonical finite exact-image subgroup family in eq:Mstage / eq:Mdescent.

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

The older semantic proper-image packet is reassembled from the kernel identification and the canonical exact-image cardinal data.

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

The proper-image family interface used by the recursion, built from the canonical finite exact-image subgroup index and the eq:Mdescent cardinal data.

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

The old proper-image residual follows from the refined exact-image family datum.

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

Elementary-stage children reassembled from the refined manuscript packets, without using the old elementary lower/proper-image axioms.

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

Elementary-stage child stratum reassembled from the refined quotient tower and finite exact-image family, avoiding the two old elementary residual axioms.

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

The full Section 8 child packet reassembled with the refined elementary-stage data. The scalar proper-image and phase-cover strata are the existing theorem-level empty packets; the elementary stratum uses the realized quotient tower and eq:Mdescent family above.

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

Partial recursion reassembled with refined elementary-stage children, so the closure names the quotient-tower and proper exact-image family packets rather than the old lower/proper-image residual axioms.

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

Same target statement as centralCover_realization_proven_fine, but with the elementary-stage final residuals replaced by the refined finite group packets in this file.