Candidate Route127 closers

Route127 publicly exposes the two Route42 candidate Section 8 packets:

• centralCover_candidateRoute42ScalarPushoutSelectedFamilyData;
• centralCover_candidateRoute42FrattiniCoordinateSystemData.

This sidecar proves replacements for both packet types from the lower exact-image obstruction and Frattini partition APIs already isolated by the Route44 path. The drop-in provider at the bottom has the same downstream shape as centralCover_candidateLiftPartitionData_from_scalarFrattiniRoute42:

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

It does not call either public Route42 residual axiom.

Route42 packet replacements

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

Route127 closes the Route42 selected scalar-pushout family packet from the selected R-valued middle obstruction map.

The scalar family is evaluation of the selected obstruction map against lambda : B.XR; additivity is inherited from linearity of the obstruction value in the obstruction space.

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

Route127 closes the Route42 coherent Frattini coordinate-system packet from the selected exact affine-fibre partition.

The base/fibre coordinates, curried realization, and both inverse laws are the two directions of the same partition equivalence.

Reassembly without the public Route42 axioms

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

Route42 scalar-obstruction evaluator through the Route127 scalar closer.

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

Middle R-lift obstruction map through the Route127 scalar closer.

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

Current Frattini affine-fibre coordinate data through the Route127 Frattini coordinate-system closer.

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

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

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

Route127 direct exact-image residual data assembled without either public Route42 candidate residual axiom.

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

Drop-in Route127 candidate lift-partition provider.

This has the same downstream call shape as centralCover_candidateLiftPartitionData_from_scalarFrattiniRoute42, but its candidate closure is the lower exact-image obstruction/Frattini-cardinality route rather than the two Route42 public packet axioms.