Target-tower realization closers

This sidecar further refines the five concrete target-tower residuals from TargetTowerConcreteClosers.lean.

Manuscript anchors:

• Section 7, eq:targettower: choose R = Phi(K) <= K <= L_Y, with B = Y/R, C = Y/K, and M = K/R;
• Section 8, eq:Mstage/eq:Mdescent: the marked-kernel exact sequences L_Y -> L_B -> L_C and the identification of ker(B -> C) with M.

The current MinimalBlock interface is module-level. It does not, by itself, construct the realized subgroups, quotient framed targets, or marked-kernel restriction maps. Accordingly this file does not manufacture those objects. It splits the five concrete residuals into smaller semantic packets and proves the reassembly theorems whose closures no longer mention the five current concrete residual names.

Subgroup provenance split

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

Frattini provenance for a selected manuscript tower R <= K <= L_Y.

• Rsub_eq_frattini : S.Rsub = Subgroup.map S.Ksub.subtype (frattini ↥S.Ksub)

  Manuscript R = Phi(K), with R realized as a subgroup of Y.

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

Module provenance for the selected manuscript tower: K/R realizes M.

• KmodR_equivM : ↥(Subgroup.map (QuotientGroup.mk' S.Rsub) S.Ksub) ≃* Multiplicative B.M

  Manuscript K/R ~= M, represented as the image of K in Y/R.

def Q2Presentation.Induction.targetSubgroupConcreteData_of_realizationParts {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (F : CentralCoverTargetSubgroupFrattiniData B S) (M : CentralCoverTargetSubgroupKmodRData B S) : CentralCoverTargetSubgroupConcreteData B

Reassemble subgroup provenance from the tower core, Frattini identity, and K/R ~= M identification.

Equations

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

def Q2Presentation.Induction.targetSubgroupProvenanceData_of_realizationParts {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (F : CentralCoverTargetSubgroupFrattiniData B S) (M : CentralCoverTargetSubgroupKmodRData B S) : CentralCoverTargetSubgroupProvenanceData B S

Reassemble the subgroup-provenance packet attached to an already selected tower.

Equations

• Q2Presentation.Induction.targetSubgroupProvenanceData_of_realizationParts B S F M = { Rsub_eq_frattini := ⋯, KmodR_equivM := M.KmodR_equivM }

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

Smaller residual: prove R = Phi(K) for a selected target tower.

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

Smaller residual: identify the selected quotient K/R with the abstract elementary module M.

theorem Q2Presentation.Induction.centralCover_targetSubgroupConcreteData_from_realizationClosers {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverTargetSubgroupConcreteData B)

Replacement for centralCover_targetSubgroupConcreteData, assembled from strictly smaller packets.

theorem Q2Presentation.Induction.centralCover_targetSubgroupProvenanceData_from_realizationClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) : Nonempty (CentralCoverTargetSubgroupProvenanceData B S)

Provenance for a fixed tower, assembled from the two smaller provenance packets.

Canonical quotient children from subgroup concrete data

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

Canonical quotient targets attached to concrete subgroup data.

This is the owned-file stand-in for the quotient-target constructor suggested by the Pro consult. The current global BoundaryFramedTarget API has no quotient constructor, and quotienting the decoration requires explicit factorization data, so the canonical quotient targets remain data here. Unlike CentralCoverTargetQuotientChildConcreteData, this packet does not duplicate the Frattini or K/R ~= M provenance: it only supplies the framed quotient targets equivalent to Y/R and Y/K.

• middleChild : FramedPair

  The framed middle target canonically equivalent to Y/R.

• lowerChild : FramedPair

  The framed lower target canonically equivalent to Y/K.

• middleEquiv : p.fst.Y ⧸ D.Rsub ≃* self.middleChild.fst.Y

  The middle target realizes the quotient group Y/R.

• lowerEquiv : p.fst.Y ⧸ D.Ksub ≃* self.lowerChild.fst.Y

  The lower target realizes the quotient group Y/K.

def Q2Presentation.Induction.targetQuotientChildConcreteData_of_canonicalQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetCanonicalQuotientData B D) : CentralCoverTargetQuotientChildConcreteData B (targetSubgroupTowerData_of_concrete B D)

Reassemble the existing concrete quotient-child packet from canonical quotient target data and concrete subgroup provenance.

Equations

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

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

Smaller residual: construct the canonical framed quotient targets Y/R and Y/K from concrete subgroup data.

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

Replacement for centralCover_targetQuotientChildConcreteData, downstream of concrete subgroup data and a canonical quotient-target packet.

Quotient children with separated provenance

def Q2Presentation.Induction.targetQuotientChildConcreteData_of_provenanceEquivs {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (P : CentralCoverTargetSubgroupProvenanceData B S) (D : CentralCoverTargetQuotientChildEquivData B S) : CentralCoverTargetQuotientChildConcreteData B S

Reassemble concrete quotient-child data from separate subgroup provenance and quotient-child equivalences.

Equations

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

theorem Q2Presentation.Induction.centralCover_targetQuotientChildConcreteData_from_realizationClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) : Nonempty (CentralCoverTargetQuotientChildConcreteData B S)

Replacement for centralCover_targetQuotientChildConcreteData, assembled from separated subgroup provenance and quotient equivalences.

Top marked-kernel exact sequence split

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

The map L_Y -> L_B and its surjectivity.

• topMarkedMap : ↥p.fst.LY →* ↥Q.middleChild.fst.LY
• topMarkedMap_surj : Function.Surjective ⇑self.topMarkedMap

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

The kernel of a selected top marked map is R.

• topMarkedKernelEquivR : ↥D.topMarkedMap.ker ≃* ↥S.Rsub

def Q2Presentation.Induction.targetTopMarkedExactData_of_mapKernel {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetTopMarkedMapData B S Q) (K : CentralCoverTargetTopMarkedKernelData B S Q D) : CentralCoverTargetTopMarkedExactData B S Q

Reassemble top marked exactness from map-surjectivity and kernel packets.

Equations

• Q2Presentation.Induction.targetTopMarkedExactData_of_mapKernel B S Q D K = { topMarkedMap := D.topMarkedMap, topMarkedMap_surj := ⋯, topMarkedKernelEquivR := K.topMarkedKernelEquivR }

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

Smaller residual: construct the top marked-kernel map and prove it is onto.

axiom Q2Presentation.Induction.centralCover_targetTopMarkedKernelData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetTopMarkedMapData B S Q) : Nonempty (CentralCoverTargetTopMarkedKernelData B S Q D)

Smaller residual: identify the kernel of the selected top marked map with R.

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

Replacement for centralCover_targetTopMarkedExactData, assembled from smaller map and kernel packets.

theorem Q2Presentation.Induction.centralCover_targetTopMarkedExactData_from_subgroupConcrete {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetQuotientMapsData B (targetSubgroupTowerData_of_concrete B D)) : Nonempty (CentralCoverTargetTopMarkedExactData B (targetSubgroupTowerData_of_concrete B D) Q)

Top marked exactness, explicitly downstream of concrete subgroup data. With a genuine quotient-target constructor this is the restriction L_Y -> L_B = L_Y/R; here the remaining map/kernel content is kept in the smaller marked-map packets above.

Middle marked-kernel exact sequence split

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

The map L_B -> L_C and its surjectivity.

• middleMarkedMap : ↥Q.middleChild.fst.LY →* ↥Q.lowerChild.fst.LY
• middleMarkedMap_surj : Function.Surjective ⇑self.middleMarkedMap

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

The kernel of a selected middle marked map is ker(B -> C).

• middleMarkedKernelEquiv : ↥D.middleMarkedMap.ker ≃* ↥Q.middleToLower.ker

def Q2Presentation.Induction.targetMiddleMarkedExactData_of_mapKernel {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleMarkedMapData B S Q) (K : CentralCoverTargetMiddleMarkedKernelData B S Q D) : CentralCoverTargetMiddleMarkedExactData B S Q

Reassemble middle marked exactness from map-surjectivity and kernel packets.

Equations

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

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

Smaller residual: construct the middle marked-kernel map and prove it is onto.

axiom Q2Presentation.Induction.centralCover_targetMiddleMarkedKernelData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleMarkedMapData B S Q) : Nonempty (CentralCoverTargetMiddleMarkedKernelData B S Q D)

Smaller residual: identify the kernel of the selected middle marked map with ker(B -> C).

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

Replacement for centralCover_targetMiddleMarkedExactData, assembled from smaller map and kernel packets.

theorem Q2Presentation.Induction.centralCover_targetMiddleMarkedExactData_from_subgroupConcrete {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetQuotientMapsData B (targetSubgroupTowerData_of_concrete B D)) : Nonempty (CentralCoverTargetMiddleMarkedExactData B (targetSubgroupTowerData_of_concrete B D) Q)

Middle marked exactness, explicitly downstream of concrete subgroup data. With canonical quotient targets this is the restriction L_B -> L_C; the map and kernel exactness remain the smaller marked-map packets.

Middle kernel identification split

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

Identify ker(B -> C) with the quotient image of K inside Y/R.

• middleKernelImageEquiv : ↥Q.middleToLower.ker ≃* ↥(Subgroup.map (QuotientGroup.mk' S.Rsub) S.Ksub)

def Q2Presentation.Induction.targetMiddleKernelIdentificationData_of_imageKmodR {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleKernelImageData B S Q) (M : CentralCoverTargetSubgroupKmodRData B S) : CentralCoverTargetMiddleKernelIdentificationData B S Q

Reassemble ker(B -> C) ~= M from the quotient-image identification and the separate K/R ~= M provenance.

Equations

• Q2Presentation.Induction.targetMiddleKernelIdentificationData_of_imageKmodR B S Q D M = { middleKernelEquivM := D.middleKernelImageEquiv.trans M.KmodR_equivM }

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

Smaller residual: identify the middle map kernel with the quotient image of K in Y/R.

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

Replacement for centralCover_targetMiddleKernelIdentificationData, assembled from the quotient-image packet and the K/R ~= M packet.

def Q2Presentation.Induction.targetMiddleKernelIdentificationData_of_subgroupConcreteImage {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetQuotientMapsData B (targetSubgroupTowerData_of_concrete B D)) (I : CentralCoverTargetMiddleKernelImageData B (targetSubgroupTowerData_of_concrete B D) Q) : CentralCoverTargetMiddleKernelIdentificationData B (targetSubgroupTowerData_of_concrete B D) Q

Reassemble ker(B -> C) ~= M from concrete subgroup data. The only remaining quotient-map fact is the smaller image-kernel packet ker(B -> C) ~= K/R; the final K/R ~= M equivalence is already part of CentralCoverTargetSubgroupConcreteData.

Equations

• Q2Presentation.Induction.targetMiddleKernelIdentificationData_of_subgroupConcreteImage B D Q I = { middleKernelEquivM := I.middleKernelImageEquiv.trans D.KmodR_equivM }

theorem Q2Presentation.Induction.centralCover_targetMiddleKernelIdentificationData_from_subgroupConcrete {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetQuotientMapsData B (targetSubgroupTowerData_of_concrete B D)) : Nonempty (CentralCoverTargetMiddleKernelIdentificationData B (targetSubgroupTowerData_of_concrete B D) Q)

Middle-kernel identification, explicitly downstream of concrete subgroup data and the quotient-image kernel packet.

Reassembly of the target tower without the five concrete residual names

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

Marked exactness reassembled without using the three current concrete marked-exactness residual names.

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

Quotient-tower data reassembled without using any of the five current concrete residual names from TargetTowerConcreteClosers.lean.

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

Elementary-stage children reassembled with the new target-tower closers and the existing proper-image concrete packets.

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

Central-cover child data reassembled with the new target-tower closers.

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

Partial recipe assembled with the new target-tower closers.

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

Cover realization assembled with the new target-tower closers.