Candidate Route130 closers

Route130 currently exposes the two broad candidate exact-image packets

• centralCover_candidateObstructionMapData;
• centralCover_candidateFrattiniExactImageCardinalityData.

This sidecar attacks those leaves without promoting any integrated route.

The obstruction-map packet is derivable in its broad form: pull the actual middle exact-image obstruction evaluation back along the supplied finite index-to-base map.

The Frattini cardinality packet is not manuscript-shaped in its fully broad form, because it quantifies over arbitrary I and O. The Section 8 statement is the canonical instance attached to the selected middle obstruction and its canonical affine fibres. The drop-in provider below routes through that coherent final residual and has the same downstream shape as centralCover_candidateLiftPartitionData_from_candidateRoute127Closers:

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

Broad obstruction packet and canonical Frattini replacement

theorem Q2Presentation.Induction.centralCover_candidateObstructionMapData_from_candidateRoute130Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (I : CentralCoverCandidateObstructionIndexBaseData B T) : Nonempty (CentralCoverCandidateObstructionMapData B T I)

Route130 closes the broad obstruction-map packet from the existing semantic exact-image API.

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

Route130's coherent final exact-image residual.

This packages the selected middle obstruction evaluation together with the matching top exact-image affine-fibre equivalence.

theorem Q2Presentation.Induction.centralCover_candidateCanonicalFrattiniExactImageCardinalityData_from_candidateRoute130Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : ∃ (O : CentralCoverCandidateMiddleRLiftObstructionMapData B T), CentralCoverCandidateFrattiniExactImageCardinalityData B T O.obstructionIndexToBaseMapData.O O.affineFiberTorsorData.Z O.affineFiberTorsorData.F

Route130 canonical Frattini cardinality replacement.

This is the manuscript-shaped cardinality statement for the selected middle obstruction and its canonical affine fibres. It intentionally does not assert the stronger arbitrary-I, O cardinality packet.

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

Route130 canonical Frattini partition replacement, keeping the selected obstruction map and exact-image partition together.

Drop-in Route130 provider

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

Route130 direct exact-image residual data from the coherent final exact-image residual.

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

Route130 middle R-lift obstruction map selected by the coherent final exact-image residual.

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

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

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

Drop-in Route130 candidate lift-partition provider.

This has exactly the same downstream call shape as centralCover_candidateLiftPartitionData_from_candidateRoute127Closers, but the candidate closure avoids the two broad Route130 packet axioms.