Candidate scalar/Frattini route36 proofs

Route36 keeps the route35 provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but lowers the five route35 candidate residuals.

On the scalar side, the coherent scalar evaluator is assembled from pointwise scalar-pushout values and additivity in lambda; homogeneity over ZMod 2 is proved theorem-level. On the Frattini side, the coordinate/realization equivalence is assembled from the lower base coordinate, fibre coordinate, curried realization, and the two inverse-law leaves.

Scalar pushout values plus additivity only

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutHomogeneityData_from_route36Additivity {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) (A : CentralCoverCandidateMiddleScalarPushoutAdditivityData V) : Nonempty (CentralCoverCandidateMiddleScalarPushoutHomogeneityData V)

Additivity of scalar-pushout values over ZMod 2 implies homogeneity.

This removes the actual-closer homogeneity residual for the selected route36 pointwise scalar-pushout family.

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

Route36 scalar evaluator from pointwise scalar-pushout values and additivity only.

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

Route36 middle R-lift obstruction map from the lowered scalar route.

Frattini coordinates from lower base/fibre leaves

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

Route36 Frattini affine-fibre coordinate data from lower base/fibre coordinate, curried realization, and inverse-law leaves.

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

Route36 Frattini exact-image partition from the lowered coordinate route.

Route-ready reassembly

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

Route36 direct exact-image residual data from the lowered scalar and Frattini leaves.

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

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

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

Route36 candidate lift-partition provider in the same B T Q shape as route35, with the route35 five residuals replaced by lower scalar and Frattini leaves.