Candidate scalar/Frattini route28 proofs

Route28 keeps the route27 downstream provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but replaces the eight route27 candidate scalar/Frattini residuals by two canonical exact-image packets fixed to the manuscript's Section 8 construction:

• the R-valued obstruction map on the canonical middle exact-image index X_Gamma(B);
• the Frattini exact-image cardinality statement for the same obstruction and the canonical regular affine R-lift fibres.

The route28 assumptions are narrower than the route27 coordinate packets: they are not quantified over arbitrary scalar-pushout families or arbitrary coordinate/realization systems. All adapters from these two packets to the route27-compatible lift-partition provider are theorem-level.

Route28 canonical exact-image packets

axiom Q2Presentation.Induction.centralCover_candidateRoute28CanonicalMiddleObstructionMapData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : let I := centralCover_candidateMiddleExactImageIndexBaseData B T; Nonempty (CentralCoverCandidateObstructionMapData B T I)

Route28 canonical middle obstruction-map packet.

Manuscript anchor: reference/q2_manuscript.tex, Section 8, pages 42--49: def:Xgamma (lines 3784--3789) defines the canonical exact-image source, and lem:obstructionseparation (lines 4207--4238) identifies scalar pushouts with the dual tests of the complete R-valued obstruction.

Unlike centralCover_candidateMiddleScalarPushoutValueAtData, centralCover_candidateMiddleScalarPushoutAdditivityData, and centralCover_candidateMiddleScalarPushoutHomogeneityData, this packet is already the assembled obstruction map on the canonical middle exact-image index.

axiom Q2Presentation.Induction.centralCover_candidateRoute28CanonicalFrattiniCardinalityData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : let I := centralCover_candidateMiddleExactImageIndexBaseData B T; let O := D.obstructionMapData; let Odata := I.sourceObstructionData O; let A := centralCover_candidateCanonicalAffineFiberTorsorData B Odata; Nonempty (CentralCoverCandidateFrattiniExactImageCardinalityData B T Odata A.Z A.F)

Route28 canonical Frattini cardinality packet.

Manuscript anchor: reference/q2_manuscript.tex, Section 8, pages 42--49: prop:finalfourier (lines 4240--4265) gives the Frattini Fourier inversion and the exact-image lift partition; the preceding affine-fibre construction is lem:affinelifting (lines 4033--4074).

For a selected route28 middle obstruction map, this asserts only the canonical finite cardinality statement for that same obstruction and the canonical regular affine fibres. It is narrower than the route27 base/fibre coordinate, realization, and inverse-law residuals.

Route28 adapters

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

Route28 middle R-lift obstruction map, fixed to the canonical middle exact-image index.

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

Route28 Frattini exact-image partition for the selected middle obstruction map.

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

Route28 coherent direct exact-image residual data assembled from the canonical middle obstruction and Frattini partition packets.

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

Route28 final exact-image residual for the selected middle obstruction and matching Frattini exact-image partition.

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

Route28 middle exact-image obstruction evaluation.

theorem Q2Presentation.Induction.centralCover_candidateTopExactImageAffineFiberEquivSigma_from_scalarFrattiniRoute28 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((E : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T) × CentralCoverCandidateTopExactImageAffineFiberEquivData B T E)

Route28 dependent top affine-fibre packet, retaining the selected middle obstruction evaluation.

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

Semantic central R-lift data from route28 and a supplied quotient-frame map.

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

Route28 candidate lift-partition provider in the same B T Q shape as the route27 provider, but with the eight route27 candidate scalar/Frattini packet axioms replaced by the two canonical exact-image route28 packets above.