Candidate Route157 closers

Route156 still exposes the coherent candidate Section 8 packet centralCover_candidateMiddleFrattiniResidualProofData. The existing sidecar CandidateMiddleFrattiniActualProofs already splits that packet into the two lower manuscript-shaped inputs:

• centralCover_candidateActualMiddleRLiftObstructionMapData;
• centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

This file is a thin route wrapper. It does not call the old broad Route152 leaves centralCover_candidateObstructionMapData or centralCover_candidateFrattiniExactImageCardinalityData.

Explicit bridge from lower Route157 data

theorem Q2Presentation.Induction.centralCover_candidateMiddleFrattiniResidualProofData_of_route157LowerData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (O : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (F : CentralCoverCandidateFrattiniExactImageEquivData B T O.obstructionIndexToBaseMapData.O O.affineFiberTorsorData.Z O.affineFiberTorsorData.F) : Nonempty (CentralCoverCandidateMiddleFrattiniResidualProofData B T)

Assemble the current coherent middle/Frattini residual from the two lower Route157 Section 8 inputs.

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

Route157 bridge from the two lower actual Section 8 inputs to the Route156 candidate middle/Frattini packet.

Route-ready replacement providers

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

Drop-in Route157 candidate lift-partition provider.

This has the same B T Q call shape as centralCover_candidateLiftPartitionData_from_candidateRoute152Closers, but its axiom closure is the two lower Route157 actual inputs rather than the coherent Route156 packet.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateRoute157Closers_canonical {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Canonical-tower spelling for routes that keep the canonical quotient tower in scope.