Integrated central-cover refinements

This file wires together the two Section 8 sidecars:

• CandidateExactImagePacketClosers.lean, which splits the concrete candidate exact-image packet into boundary-postcomposition, obstruction-index/base, obstruction-map, and Frattini-cardinality packets;
• ElementaryTowerResiduals.lean, which splits the elementary target/proper image residuals into concrete subgroup, quotient-map, cardinality, and exact-sequence packets.

The target theorem has the same shape as centralCover_realization_proven_fine, but its axiom closure names the refined manuscript packets instead of the older coarse residuals.

theorem Q2Presentation.Induction.centralCover_liftTorsorData_fine_integrated {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverLiftTorsorData B)

Central-cover lift-torsor data with the candidate source routed through the concrete candidate exact-image packet.

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

Elementary-stage children routed through the target-tower realization sidecar and the proper-image exactness sidecar.

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

Central-cover child data routed through the target-tower realization and proper-image exactness sidecars.

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

Central-cover partial recipe with elementary children routed through the quotient-tower/proper-image-family packets.

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

Full central-cover realization using both refined sidecars.