Candidate scalar/Frattini route40 proofs

Route40 keeps the Route39 drop-in provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but does not use either Route39 candidate residual axiom.

• Scalar side: the Route39 selected scalar-pushout family is reassembled from the existing scalar-pushout value packet and its linearity in lambda : B.XR. This is the manuscript lem:obstructionseparation scalar-pushout evaluator in Section 8.
• Frattini side: the final Fourier zero-locus count is recovered from the explicit affine-fibre exact-image partition supplied by coordinate, realization, and inverse-law packets. This is the partition underlying prop:finalfourier in Section 8, before taking its cardinality shadow.

No new axiom is introduced in this file. The exported provider is a strict Route40 lowering of the Route39 candidate frontier: its axiom closure should name the smaller scalar/Frattini semantic packets, not centralCover_candidateRoute39ScalarPushoutSelectedFamilyData or centralCover_candidateRoute39FrattiniFourierZeroLocusData.

Route40 scalar packet: selected family from scalar values and linearity

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

Route40 recovers the Route39 selected scalar-pushout family from the scalar-pushout value packet plus linearity in the invariant scalar parameter.

Manuscript anchor: Section 8, lem:obstructionseparation, where scalar pushouts separate the complete R-valued obstruction.

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

Route40 scalar-obstruction evaluator.

The selected Route40 value family carries additivity; homogeneity over ZMod 2 is the theorem-level Route36 consequence of additivity.

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

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

Route40 Frattini packet: exact affine-fibre partition before cardinality

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

Route40 Frattini exact-image cardinality from the explicit affine-fibre partition.

This is the cardinal shadow of the coordinate/realization equivalence, not the Route39 Fourier zero-locus axiom.

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

Route40 recovers the Route39 Fourier zero-locus packet from the explicit affine-fibre partition plus the theorem-level regular torsor count.

Manuscript anchor: Section 8, prop:finalfourier, where unobstructed final R-lifts form regular affine fibres of cardinality z_R.

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

Route38's Frattini transform shape, recovered through the Route40 explicit partition rather than through the Route39 Fourier zero-locus axiom.

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

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

This is deliberately the stronger structural packet, so the Route40 provider does not need to call the Route39 Fourier zero-locus residual.

Route-ready reassembly

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

Route40 direct exact-image residual data from the lowered scalar evaluator and the explicit Frattini affine-fibre partition.

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

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

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

Drop-in Route40 candidate lift-partition provider.

The theorem has the same B T Q target shape as Route39, but its axiom closure uses the smaller scalar value/linearity and Frattini coordinate/realization semantic packets instead of either Route39 candidate residual axiom.