Candidate scalar/Frattini route41 proofs

Route41 keeps the Route40 drop-in provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but routes the candidate side through the finer actual-closer decomposition of the Section 8 scalar/Frattini packets. In particular, the exported provider does not use the five Route40 candidate residual axioms

• centralCover_candidateMiddleScalarPushoutValueData;
• centralCover_candidateMiddleScalarPushoutLinearityData;
• centralCover_candidateFrattiniLiftCoordinateData;
• centralCover_candidateFrattiniRealizationData;
• centralCover_candidateFrattiniCoordinateInverseData.

They are replaced by the pointwise scalar-pushout value/additivity/homogeneity packets and the base/fibre Frattini coordinate, realization, and inverse-law packets from CandidateScalarFrattiniActualClosers. These are the manuscript-shaped pieces of Section 8, pages 42--49: lem:obstructionseparation, lem:affinelifting, and prop:finalfourier.

No new axiom is introduced in this file.

Route41 scalar packet

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

Route41 middle R-lift obstruction map through the pointwise scalar-pushout actual closer packets.

Manuscript anchor: Section 8, pages 45--47, lem:obstructionseparation separates the R-valued obstruction by invariant scalar pushouts; the actual closer API records the value of each scalar test and its linearity in the invariant character.

Route41 Frattini packet

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

Route41 Frattini exact-image partition through the base/fibre coordinate actual closer packets.

Manuscript anchor: Section 8, pages 43--49, especially lem:affinelifting and prop:finalfourier: top exact-image maps are identified with unobstructed middle base points together with affine R-lift coordinates.

Route-ready reassembly

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

Route41 direct exact-image residual data from the finer scalar and Frattini actual closer packets.

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

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

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

Drop-in Route41 candidate lift-partition provider.

This has the same B T Q target shape as Route40, but its axiom closure is strictly finer on the candidate Section 8 frontier: it removes all five Route40 candidate scalar/Frattini residual names and exposes only the lower actual-closer packets.