Candidate scalar/Frattini route20 proofs

Route20 keeps the supervisor-facing hook shape from Route19,

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B),

but does not route through the two arbitrary final exact-image residual axioms used by Route19:

• centralCover_candidateMiddleExactImageObstructionEvaluationData_residual;
• centralCover_candidateTopExactImageAffineFiberEquivData_residual.

Instead it exposes the manuscript-shaped packets actually needed by the lift partition:

• the middle R-lift obstruction map on the canonical middle exact-image index;
• the Frattini exact-image partition of the canonical affine fibres for that selected obstruction map.

The second packet is weaker than the Route19 top affine-fibre equivalence residual: it supplies the partition consumed by CentralCoverCandidateLiftPartitionData, without asserting a separately quantified top equivalence for an arbitrary middle evaluation.

Route20 manuscript-shaped packets

structure Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute20MiddleData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Type

Route20 middle packet: the actual R-valued obstruction map on the canonical middle exact-image source.

• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T

structure Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute20TopPartitionData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (M : CentralCoverCandidateScalarFrattiniRoute20MiddleData B T) : Type

Route20 top packet: the exact-image partition of top candidate maps by the unobstructed canonical affine R-lift fibres attached to the selected middle obstruction map.

• frattiniPartition : CentralCoverCandidateFrattiniExactImageSurjectivityData B T M.middleObstruction.obstructionIndexToBaseMapData.O M.middleObstruction.affineFiberTorsorData.Z M.middleObstruction.affineFiberTorsorData.F

axiom Q2Presentation.Induction.centralCover_candidateScalarFrattiniRoute20MiddleData_residual {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateScalarFrattiniRoute20MiddleData B T)

Route20 residual for the middle R-lift obstruction map.

axiom Q2Presentation.Induction.centralCover_candidateScalarFrattiniRoute20TopPartitionData_residual {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (M : CentralCoverCandidateScalarFrattiniRoute20MiddleData B T) : Nonempty (CentralCoverCandidateScalarFrattiniRoute20TopPartitionData B T M)

Route20 residual for the Frattini exact-image partition attached to the selected middle obstruction map.

Reassembly

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

Route20 direct exact-image residual data assembled from the smaller manuscript-shaped packets.

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

Route20 coherent final exact-image residual for the selected middle obstruction and its matching top Frattini partition.

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

Route20 middle exact-image obstruction evaluation for the selected middle obstruction map.

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

Route20's dependent top affine-fibre packet.

This deliberately exposes the manuscript-supported Sigma shape rather than the stronger Route19 statement for every arbitrary supplied middle evaluation.

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

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

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

Route20 candidate lift-partition provider in the same B T Q shape as the current integrated route.