Candidate scalar/Frattini route43 proofs

Route43 keeps the Route42 drop-in provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but proves the two Route42 candidate packet shapes from the finer actual-closer obligations already present in the candidate Section 8 API.

Scalar side:

• Route42's selected scalar-pushout family is assembled from the pointwise scalar-pushout family and additivity packet of CandidateScalarFrattiniActualClosers.
• Homogeneity remains theorem-level over ZMod 2, via the Route36 additivity argument.

Frattini side:

• Route42's coherent coordinate-system packet is assembled from the lower base-coordinate, fibre-coordinate, curried realization, and two inverse-law actual-closer obligations.

No new axiom is introduced in this file. The exported Route43 provider has the same public target shape as Route42, but its axiom closure does not contain centralCover_candidateRoute42ScalarPushoutSelectedFamilyData or centralCover_candidateRoute42FrattiniCoordinateSystemData.

Route43 bridges to the Route42 packet shapes

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

Route43 closes the Route42 selected scalar-pushout family packet from the finer pointwise scalar-pushout values and additivity actual-closer packets.

Manuscript anchor: Section 8, lem:obstructionseparation: the complete R-obstruction is separated by invariant scalar pushouts, and the selected family is additive in lambda : X_R.

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

Route43 closes the Route42 coherent Frattini coordinate-system packet from the lower base/fibre coordinate, curried realization, and inverse-law actual-closer packets.

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

Route43 scalar route

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutValueAtData_from_scalarFrattiniRoute43 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (lam : ↥B.XR) : Nonempty (CentralCoverCandidateMiddleScalarPushoutValueAtData B T lam)

Route43 pointwise scalar-pushout values through the Route43 bridge.

theorem Q2Presentation.Induction.centralCover_candidateRoute43SelectedScalarPushoutAdditivityData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) × CentralCoverCandidateMiddleScalarPushoutAdditivityData V)

Route43 supplies additivity for the selected scalar-pushout family.

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

Route43 scalar-obstruction evaluator.

The only scalar residuals in the closure are the finer actual-closer pointwise value and additivity packets; homogeneity is theorem-level.

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

Route43 middle R-lift obstruction map from the refined scalar route.

Route43 Frattini route

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

Route43 base-coordinate shape through the coherent coordinate-system bridge.

theorem Q2Presentation.Induction.centralCover_candidateRoute43FrattiniBaseFiberCoordinateData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty ((C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) × CentralCoverCandidateFrattiniFiberCoordinateData C)

Route43 supplies the selected base/fibre Frattini coordinate pair.

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

Route43 curried fibre-realization shape through the coherent coordinate-system bridge.

theorem Q2Presentation.Induction.centralCover_candidateRoute43FrattiniCoordinateSystemSigma {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty ((C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) × (F : CentralCoverCandidateFrattiniFiberCoordinateData C) × (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) × CentralCoverCandidateFrattiniRealizeLiftCoordinateData C F R × CentralCoverCandidateFrattiniLiftCoordinateRealizeData C F R)

Route43 exposes the full selected Frattini coordinate system and both inverse laws.

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

Route43 Frattini affine-fibre coordinate data assembled from the refined coordinate-system bridge.

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

Route43 Frattini exact-image partition for the selected middle obstruction.

Route-ready reassembly

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

Route43 direct exact-image residual data from the refined scalar bridge and the refined coherent Frattini coordinate-system bridge.

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

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

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

Drop-in Route43 candidate lift-partition provider.

The theorem has the same B T Q target shape as Route42. Its candidate Section 8 closure is the finer actual-closer frontier rather than the two Route42 aggregate residual names.