Proper-image canonical restriction closers

This sidecar closes one more Section 8 proper-image residual in the final route without editing the target-tower sidecars.

Manuscript anchors:

• eq:targettower: the realized tower supplies B = Y/R, C = Y/K, and ker(B -> C) ~= K/R = M;
• eq:Mstage / eq:Mdescent: proper-image subtraction uses the same B -> C map, then restricts it to J ∩ L_B -> L_C.

TargetTowerRealizationClosers already constructs the elementary quotient tower through a packet that contains ker(B -> C) ~= M. The previous proper-image route rebuilt cardinality data from an arbitrary tower and had to call the residual axiom centralCover_middleKernelEquivData for that tower. Here we keep the quotient tower paired with the kernel equivalence produced by the target-tower construction, so the integrated route no longer needs that residual name. The remaining restriction content is still the explicit canonical restriction packet from ProperImageExactClosers.

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

A quotient tower together with the manuscript identification ker(B -> C) ~= M for that same tower.

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

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

Convert the target marked-kernel identification packet into the older middle-kernel equivalence packet for the assembled elementary quotient tower.

Equations

• Q2Presentation.Induction.middleKernelEquivData_of_targetKernelIdentification B S Q C K = { middleKernelEquivM := id K.middleKernelEquivM }

theorem Q2Presentation.Induction.centralCover_elementaryQuotientTowerMiddleKernelData_from_realizationClosers {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryQuotientTowerMiddleKernelData B)

Target-tower realization with the ker(B -> C) ~= M witness retained.

This follows the existing construction in centralCover_elementaryQuotientTowerData_from_realizationClosers, but keeps the middle-kernel equivalence instead of projecting it away.

theorem Q2Presentation.Induction.centralCover_elementaryProperImageCardinalityData_from_middleKernelAndRestriction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverElementaryQuotientTowerMiddleKernelData B) : Nonempty (CentralCoverElementaryProperImageCardinalityData B D.tower)

Proper-image cardinality data for a tower whose middle-kernel equivalence has been carried along from the target-tower construction.

The only remaining residual in this theorem is the semantic statement that the actual map B -> C canonically restricts to J ∩ L_B -> L_C.

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

Elementary-stage children routed through the target-tower construction that already supplies ker(B -> C) ~= M.

Compared with centralCover_elementaryStageChildren_from_integratedRealizationClosers before this sidecar is wired in, this route eliminates the residual centralCover_middleKernelEquivData from the final closure.