Canonical target-quotient closers

This sidecar is intentionally not imported by the root module. It gives an alternate final-count route for the first current §8 priority: target/proper- image quotient bookkeeping.

Manuscript anchors:

• §7, eq:targettower: choose R = Phi(K) <= K <= L_Y, set B = Y/R, C = Y/K, and identify M = K/R;
• §8, eq:Mstage/eq:Mdescent: use the marked-kernel exact sequences for Y -> B -> C and the literal J ∩ M proper-image kernels.

The key point here is that the existing §7 group-tower packet already contains the realized subgroups R <= K, the Frattini identity, and the K/R ~= M bridge for the specific MinimalBlock built from that same packet. Therefore the target subgroup tower, Frattini, and K/R residual names are not needed in this route.

A canonical quotient tower with its middle-kernel equivalence

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

A quotient tower together with the semantic equivalence ker(B -> C) ~= M.

CentralCoverElementaryQuotientTowerData stores only the cardinality of the middle kernel. The proper-image exactness sidecar also needs the equivalence with M; carrying it here prevents the route from calling the separate centralCover_middleKernelEquivData residual.

• tower : CentralCoverElementaryQuotientTowerData B
• middleKernelEquivData : CentralCoverMiddleKernelEquivData B self.tower

def Q2Presentation.Induction.targetCanonicalQuotientTowerData_of_targetPackets {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (C : CentralCoverTargetTowerCardinalityData B S Q) (K : CentralCoverTargetMiddleKernelIdentificationData B S Q) : CentralCoverTargetCanonicalQuotientTowerData B

Build the canonical quotient-tower package from target packets, while retaining the already-proved middle-kernel identification.

Equations

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

Target subgroup data from the §7 group tower

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

The §7 group-tower packet supplies the concrete target subgroup provenance for the MinimalBlock constructed from that same packet.

theorem Q2Presentation.Induction.centralCover_targetCanonicalQuotientTowerData_from_selfGroupTower {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 the minimal block built from a §7 group-tower packet.

This route proves the subgroup tower, Frattini identity, and K/R ~= M bookkeeping from G; the remaining quotient-target and marked-map content is exactly the smaller target quotient/marked residual layer.

Reassembly from a supplied canonical quotient tower

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

Candidate lift-torsor data using a supplied quotient tower, so this theorem does not reconstruct the target tower internally.

theorem Q2Presentation.Induction.centralCover_elementaryStageChildren_from_canonicalQuotientTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverElementaryStageChildren B)

Elementary-stage children from a supplied canonical quotient tower and its middle-kernel equivalence.

theorem Q2Presentation.Induction.centralCover_childrenData_from_canonicalQuotientTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverChildrenData B)

Child data from a supplied canonical quotient tower.

theorem Q2Presentation.Induction.centralCover_partialRecipe_fine_from_canonicalQuotientTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (L : CentralCoverLiftTorsorData B) : Nonempty (CentralCoverPartialRecipe B L)

Partial recipe from a supplied canonical quotient tower.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_canonicalQuotientTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CoverRealization B)

Cover realization from a supplied canonical quotient tower.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerTargetClosers {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 for the specific block produced by a §7 group tower, using the canonical target quotient route above.

Alternate final-count route

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

Nonterminal branch routed through the §7 group tower without calling the target subgroup tower/Frattini/K/R residual names.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_targetQuotientCanonical (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 using the canonical target-quotient route.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_targetQuotientCanonical (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 using the canonical target-quotient nonterminal branch.

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

Boundary-framed counts equal through the canonical target-quotient route.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_targetQuotientCanonical (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 the canonical target-quotient route.