Candidate scalar/Frattini route31 proofs

Route31 keeps the route30 integration-facing provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but does not route through the route29/route30 candidate residual names:

• centralCover_candidateRoute29CanonicalScalarPushoutValueData;
• centralCover_candidateRoute29FrattiniFourierCountData;
• centralCover_candidateRoute30CanonicalScalarPushoutAdditivityData.

Instead, it uses the coherent current packets from CandidateScalarFrattiniCurrentProofs.lean: one chosen scalar-pushout evaluator with its linearity, and one chosen Frattini coordinate/realization equivalence. This is the route-ready theorem shape a coordinator can swap into an integrated route without editing the current route32 file.

Route31 coherent candidate wrappers

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

Route31 scalar-obstruction evaluator, routed through one coherent chosen scalar-pushout evaluator rather than the route29 value packet plus the route30 arbitrary-value additivity packet.

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

Route31 middle R-lift obstruction map through coherent scalar-pushout data.

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

Route31 Frattini exact-image partition through one coherent coordinate / realization equivalence, avoiding the route29 Fourier-count packet in this provider.

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

Route31 coherent direct exact-image residual data.

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

Route31 candidate lift-partition provider in the same B T Q shape as the route30 provider, with no dependency on the three route29/route30 candidate residual names.