Candidate scalar/Frattini route18 proofs

Route18 is the direct exact-image sidecar for the two candidate Route17 leaves:

• centralCover_candidateMiddleRLiftObstructionMapData_residual;
• centralCover_candidateFrattiniAffineFiberPartition_residual.

The sidecar keeps Route17's supervisor-facing provider shape B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B), but routes the two leaves through the narrower manuscript-shaped exact-image packets already isolated in CandidateExactImagePacketClosers:

• the R-valued obstruction map on the canonical middle exact-image index;
• the Frattini exact-image cardinality/partition packet attached to that same obstruction datum.

Route18 replacements for the two Route17 leaves

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

Route18 replacement for the middle R-lift obstruction-map residual.

The closure should name the smaller centralCover_candidateObstructionMapData packet, not the Route17 residual centralCover_candidateMiddleRLiftObstructionMapData_residual.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberPartition_from_scalarFrattiniRoute18 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty (CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F)

Route18 replacement for the Frattini affine-fibre partition residual.

The closure should name the smaller centralCover_candidateFrattiniExactImageCardinalityData packet, not the Route17 residual centralCover_candidateFrattiniAffineFiberPartition_residual.

Direct exact-image reassembly

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

Coherent direct exact-image data assembled from the two Route18 replacements.

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

Final exact-image residual data assembled through Route18's direct replacement pair.

theorem Q2Presentation.Induction.centralCover_candidateRLiftSemanticData_from_scalarFrattiniRoute18 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty (CentralCoverCandidateRLiftSemanticData B T)

Semantic central R-lift data from Route18 and a supplied quotient-frame map.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_scalarFrattiniRoute18 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Route18 candidate lift-partition provider in the same supervisor-facing shape as Route17.

The quotient-frame argument is still supplied by the integrated route; Route18 only replaces the two direct exact-image residual leaves below it.