Candidate scalar/Frattini route16 proofs

Route16 attacks the two route15 candidate residuals:

• centralCover_candidateMiddleScalarObstructionEvaluatorData;
• centralCover_candidateFrattiniAffineFiberCoordinateData.

The exact route15 target shapes are exported below under route16 names, but their proofs route through the smaller manuscript-shaped packets from CandidateScalarFrattiniSemanticClosers:

• scalar pushout values and linearity in lambda : B.XR;
• Frattini coordinate, realization, and inverse-law data.

The route-ready theorem at the bottom has the same target shape as centralCover_candidateLiftPartitionData_from_scalarFrattiniRoute15.

Exact route15 target replacements

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

Route16 scalar obstruction evaluator, proved without the broad route15 scalar-obstruction evaluator axiom.

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

Route16 Frattini affine-fibre coordinate data, proved without the broad route15 Frattini affine-fibre coordinate axiom.

Route15-shaped middle obstruction and Frattini partition

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

Route16 middle R-lift obstruction map assembled from the route16 scalar obstruction evaluator.

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

Route16 Frattini exact-image partition for the affine fibres attached to the selected middle obstruction map.

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

Coherent route16 candidate direct exact-image data.

This keeps the route15 sigma shape: one selected middle obstruction map paired with the matching Frattini partition for its affine fibres.

Route-ready replacement

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

Route16 candidate lift-partition provider in the same target shape as centralCover_candidateLiftPartitionData_from_scalarFrattiniRoute15.

The quotient-frame argument is retained for drop-in route compatibility.