Candidate scalar/Frattini route35 proofs

Route35 keeps the route34 provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but routes the candidate side below route34's two exact-image packet residuals:

• centralCover_candidateObstructionMapData;
• centralCover_candidateFrattiniExactImageCardinalityData.

Instead, it uses the lower scalar/Frattini semantic split:

• scalar-pushout values and linearity in lambda : X_R;
• Frattini lift-coordinate, realization, and inverse-law packets.

This is the manuscript-shaped split corresponding to scalar separation of the middle R-obstruction and the affine-fibre Frattini partition in Section 8.

Route35 wrappers around the lower scalar/Frattini semantic route

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

Route35 middle R-lift obstruction map.

Unlike route34, this does not call centralCover_candidateObstructionMapData; it is assembled from scalar pushout values plus linearity.

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

Route35 Frattini affine-fibre exact-image partition.

Unlike route34, this does not call centralCover_candidateFrattiniExactImageCardinalityData; it is assembled from the coordinate/realization equivalence data.

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

Route35 direct exact-image residual data from the lower semantic split.

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

Route35 semantic central R-lift data from the direct exact-image split and a route-supplied quotient-frame map.

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

Route35 candidate lift-partition provider in the same B T Q shape as route34, with both route34 candidate residual names replaced by the lower scalar/Frattini semantic packets.