Candidate scalar and Frattini actual proof route

This sidecar retires the eight lower packets introduced in CandidateScalarFrattiniActualClosers.lean from the route-level theorem shape, without importing that file.

The old split asks for scalar-pushout additivity and homogeneity for an arbitrary family V. The manuscript route only supplies those laws for the chosen scalar obstruction evaluator. Rather than manufacture unrelated maps, we route through the coherent semantic packets already isolated in CandidateScalarFrattiniSemanticClosers.lean:

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

These are the remaining finer semantic assumptions exposed by this file.

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

Middle R-lift obstruction data through the coherent scalar-pushout value/linearity packets, not through the old pointwise arbitrary-family packets.

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

Frattini exact-image partition through the coherent coordinate, realization, and inverse-law packets.

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

Coherent direct exact-image residual data through the honest scalar/Frattini semantic packets.

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

Route-level replacement for centralCover_candidateLiftPartitionData_from_scalarFrattiniActualClosers.

The target shape is the same as the old actual-closer theorem, but the axiom closure names only the coherent scalar/Frattini semantic packets listed in this module docstring, not the eight retired actual-closer packet names.