Candidate scalar/Frattini route21 proofs

Route21 keeps the route20 supervisor-facing hook shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B),

but it no longer uses the two route20 wrapper residuals:

• centralCover_candidateScalarFrattiniRoute20MiddleData_residual;
• centralCover_candidateScalarFrattiniRoute20TopPartitionData_residual.

Instead it exposes the two manuscript-shaped pieces directly:

• the actual R-valued obstruction evaluation on the canonical middle exact-image index X_Gamma(C);
• an actual Frattini exact-image equivalence for the canonical affine fibres attached to that selected obstruction evaluation.

The second datum is stronger than the route20 partition field but narrower than the older arbitrary top-affine-fibre residual: it is only required for the chosen canonical middle obstruction.

Route21 manuscript-shaped packets

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

Route21 middle packet: an explicit obstruction evaluation on the canonical middle exact-image index.

• obstructionEvaluation : CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute21MiddleEvaluationData.middleRLiftObstructionMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateScalarFrattiniRoute21MiddleEvaluationData B T) : CentralCoverCandidateMiddleRLiftObstructionMapData B T

Repackage the explicit canonical-index evaluation as the route20 middle R-lift obstruction map.

Equations

• D.middleRLiftObstructionMapData = { obstruction := D.obstructionEvaluation.obstruction }

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute21MiddleEvaluationData.route20MiddleData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateScalarFrattiniRoute21MiddleEvaluationData B T) : CentralCoverCandidateScalarFrattiniRoute20MiddleData B T

The route20 middle wrapper induced by the route21 middle packet.

Equations

• D.route20MiddleData = { middleObstruction := D.middleRLiftObstructionMapData }

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

Route21 top packet: an actual exact-image equivalence for the canonical affine fibres attached to the selected route21 middle obstruction.

• frattiniEquiv : CentralCoverCandidateFrattiniExactImageEquivData B T M.middleRLiftObstructionMapData.obstructionIndexToBaseMapData.O M.middleRLiftObstructionMapData.affineFiberTorsorData.Z M.middleRLiftObstructionMapData.affineFiberTorsorData.F

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute21TopEquivData.route20TopPartitionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {M : CentralCoverCandidateScalarFrattiniRoute21MiddleEvaluationData B T} (D : CentralCoverCandidateScalarFrattiniRoute21TopEquivData B T M) : CentralCoverCandidateScalarFrattiniRoute20TopPartitionData B T M.route20MiddleData

The route20 top partition wrapper induced by the route21 exact-image equivalence.

Equations

• D.route20TopPartitionData = { frattiniPartition := D.frattiniEquiv.frattiniExactImage }

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

Route21 residual for the canonical middle exact-image obstruction evaluation.

axiom Q2Presentation.Induction.centralCover_candidateScalarFrattiniRoute21TopEquivData_residual {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (M : CentralCoverCandidateScalarFrattiniRoute21MiddleEvaluationData B T) : Nonempty (CentralCoverCandidateScalarFrattiniRoute21TopEquivData B T M)

Route21 residual for the Frattini exact-image equivalence attached to the selected route21 middle obstruction.

Route20 wrapper replacement theorems

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

Route20 middle wrapper obtained from the route21 canonical obstruction evaluation, without using the route20 middle residual.

theorem Q2Presentation.Induction.centralCover_candidateScalarFrattiniRoute20TopPartitionData_from_route21 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (M : CentralCoverCandidateScalarFrattiniRoute21MiddleEvaluationData B T) : Nonempty (CentralCoverCandidateScalarFrattiniRoute20TopPartitionData B T M.route20MiddleData)

Route20 top wrapper obtained from the route21 Frattini exact-image equivalence, without using the route20 top residual.

Route-ready reassembly

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

Route21 direct exact-image residual data assembled from the canonical obstruction evaluation and exact-image equivalence.

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

Route21 coherent final exact-image residual for the selected middle obstruction and matching Frattini exact-image equivalence.

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

Route21 middle exact-image obstruction evaluation for the selected canonical obstruction map.

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

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

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

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

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

Route21 candidate lift-partition provider in the same B T Q shape as the route20 candidate hook.