Candidate scalar/Frattini route17 proofs

Route17 is a candidate-side sidecar for the route16 call site. Route16 exposed five scalar/Frattini leaves from CandidateScalarFrattiniSemanticClosers:

• centralCover_candidateMiddleScalarPushoutValueData;
• centralCover_candidateMiddleScalarPushoutLinearityData;
• centralCover_candidateFrattiniLiftCoordinateData;
• centralCover_candidateFrattiniRealizationData;
• centralCover_candidateFrattiniCoordinateInverseData.

The arbitrary linearity and arbitrary inverse-law packet shapes are stronger than the route needs: the manuscript construction supplies one coherent scalar obstruction evaluator and one matching Frattini affine-fibre equivalence. The route-ready theorem below therefore factors through the direct exact-image split from CandidateExactImageDirectResidualProofs, whose residuals are the middle R-lift obstruction map and the matching Frattini partition for its canonical affine fibres.

This file does not edit routed integration files. A supervisor can replace the route16 call

centralCover_candidateLiftPartitionData_from_scalarFrattiniRoute16 B T Qframe

by

centralCover_candidateLiftPartitionData_from_scalarFrattiniRoute17 B T Qframe

to remove the five route16 candidate scalar/Frattini names from the integrated candidate-side closure.

Diagnostic bridges for the old route16 packet names

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

Route17 proves the old scalar-pushout value packet from the finer pointwise scalar-pushout family. Its closure does not name centralCover_candidateMiddleScalarPushoutValueData.

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutChosenLinearityData_from_scalarFrattiniRoute17 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) × CentralCoverCandidateMiddleScalarPushoutLinearityData V.valueData)

Route17's scalar linearity replacement: one chosen scalar-pushout family with linearity for that same family.

This is the manuscript-shaped datum needed to assemble the scalar obstruction evaluator. It intentionally does not assert the stronger route16 residual centralCover_candidateMiddleScalarPushoutLinearityData D for an arbitrary externally supplied value packet D.

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

Route17 scalar obstruction evaluator assembled from the chosen pointwise scalar-pushout family and its additivity/homogeneity laws.

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

Route17 proves the old Frattini lift-coordinate packet from the finer base/fibre coordinate packets. Its closure does not name centralCover_candidateFrattiniLiftCoordinateData.

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

Route17 proves the old Frattini realization packet from the finer curried base/fibre realization packet. Its closure does not name centralCover_candidateFrattiniRealizationData.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniChosenCoordinateInverseData_from_scalarFrattiniRoute17 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty ((C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) × (F : CentralCoverCandidateFrattiniFiberCoordinateData C) × (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) × CentralCoverCandidateFrattiniCoordinateInverseData (C.liftCoordinateData F) R.realizationData)

Route17's Frattini inverse-law replacement: one chosen base coordinate, fibre coordinate, and realization map with inverse laws for that same pair.

This is the coherent datum needed to assemble the affine-fibre coordinate equivalence. It intentionally does not assert inverse laws for arbitrary externally supplied coordinate and realization maps.

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

Route17 affine-fibre coordinate packet assembled from the finer coherent base/fibre coordinate and realization data.

Route-ready direct exact-image replacement

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

Direct exact-image residual data for Route17.

The residuals are the strictly narrower manuscript-shaped pair:

• the middle R-lift obstruction map on the canonical middle exact-image source;
• the matching Frattini exact-image partition of top candidate maps by unobstructed affine R-lift fibres.

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

Middle R-lift obstruction map used by the Route17 direct residual.

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

Frattini affine-fibre partition used by the Route17 direct residual.

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

Route17 candidate lift-partition provider in the same supervisor-facing shape as Route16.

The quotient-frame argument is consumed by the direct exact-image residual reassembly, matching the route16 call site while avoiding the five route16 candidate scalar/Frattini residual names.