Candidate exact-image Route67 closers

Route67 is candidate-side only. It gives the active integrated route a provider with the same public call shape as Route63,

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but it does not route through the two broad exact-image packet axioms currently visible in Route66:

• centralCover_candidateObstructionMapData;
• centralCover_candidateFrattiniExactImageCardinalityData.

Instead it reuses the existing Route39 manuscript-shaped exact-image split:

• one selected scalar-pushout family, additive in lambda : X_R, which builds the actual middle R-valued obstruction map (lem:obstructionseparation);
• the final Frattini/Fourier zero-locus count for that selected obstruction (prop:finalfourier), plus the theorem-level regular affine-fibre torsor count.

Thus the Route67 provider strictly lowers the two Route66 candidate atoms to the selected scalar-obstruction and selected Frattini/Fourier packets already present in the API. No theorem in this file calls the broad packet axioms.

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

Route67 selected middle R-obstruction map, assembled from the selected scalar-pushout family of Route39.

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

Route67 selected Frattini cardinality packet for a fixed middle obstruction.

This is not the over-general arbitrary-I, O packet. It is the cardinality shadow of the final Fourier zero-locus count for the selected middle obstruction and its canonical affine fibres.

theorem Q2Presentation.Induction.centralCover_candidateSelectedFrattiniAffineFiberPartition_from_route67 {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)

Route67 selected Frattini exact-image partition for a fixed middle obstruction.

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

Coherent Route67 direct exact-image residual: the selected middle obstruction and its matching Frattini partition.

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

Semantic central R-lift data from the Route67 exact-image split and the quotient-frame map supplied by the integrated route.

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

Drop-in candidate lift-partition provider for Route67.

This is the only theorem the integrated route needs at the candidate call site. Its expected candidate-side axiom frontier is

• centralCover_candidateRoute39ScalarPushoutSelectedFamilyData;
• centralCover_candidateRoute39FrattiniFourierZeroLocusData;

and not the two broad Route66 packet axioms.