Candidate scalar/Frattini route15 proofs

This sidecar gives a route14-shaped candidate lift-partition provider without using the eight pointwise scalar/Frattini packet axioms exposed by route14:

• centralCover_candidateMiddleScalarPushoutValueAtData;
• centralCover_candidateMiddleScalarPushoutAdditivityData;
• centralCover_candidateMiddleScalarPushoutHomogeneityData;
• centralCover_candidateFrattiniBaseCoordinateData;
• centralCover_candidateFrattiniFiberCoordinateData;
• centralCover_candidateFrattiniFiberRealizationData;
• centralCover_candidateFrattiniRealizeLiftCoordinateData;
• centralCover_candidateFrattiniLiftCoordinateRealizeData.

The available API still does not construct the scalar evaluator or Frattini coordinate maps from first principles. The theorem below therefore routes through the two smaller current semantic inputs:

• centralCover_candidateMiddleScalarObstructionEvaluatorData;
• centralCover_candidateFrattiniAffineFiberCoordinateData.

No routed file is edited here.

Route15 middle obstruction and Frattini partition

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

Route15 middle R-lift obstruction map.

The obstruction is assembled from scalar-pushout evaluations linear in lambda : B.XR, via centralCover_candidateMiddleRLiftObstructionEvaluator.

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

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

theorem Q2Presentation.Induction.centralCover_candidateDirectExactImageResidualData_from_scalarFrattiniRoute15 {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 route15 candidate direct exact-image data.

This is the manuscript-shaped pair actually needed downstream: one middle obstruction map and the matching Frattini partition for its affine fibres.

Route14-shaped provider

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

Candidate lift-partition provider in the shape consumed by route14.

The quotient-frame argument is retained so this theorem can replace centralCover_candidateLiftPartitionData_from_route12SemanticProofs at the route14 call site. The final lift-partition structure itself stores the obstruction data, affine fibres, and partition; the quotient-frame map is used upstream to justify the exact-image base quotient but is not a field of CentralCoverCandidateLiftPartitionData.