Candidate Route169 closers

Route168's candidate insertion point consumes centralCover_candidateLiftPartitionData_from_candidateRoute167Closers, whose axiom closure is the seven Route146 pointwise scalar/Frattini atoms.

This sidecar keeps the same route-ready B T Q provider shape, but routes the candidate source side through the two actual middle/Frattini inputs isolated in CandidateMiddleFrattiniActualProofs:

• centralCover_candidateActualMiddleRLiftObstructionMapData;
• centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

Thus the Route169 provider removes all seven current Route168 candidate pointwise atoms from its own closure.

Route169 actual split

theorem Q2Presentation.Induction.centralCover_candidateRoute169ActualMiddleFrattiniSplitData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((O : CentralCoverCandidateMiddleRLiftObstructionMapData B T) × CentralCoverCandidateFrattiniExactImageEquivData B T O.obstructionIndexToBaseMapData.O O.affineFiberTorsorData.Z O.affineFiberTorsorData.F)

Route169 selected actual middle obstruction and matching Frattini exact-image equivalence.

The Frattini equivalence is dependent on the selected obstruction map, matching the affine-fibre organization in manuscript Section 8.

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

Coherent Route169 middle/Frattini source packet assembled from the actual split inputs, without calling the older coherent residual packet and without calling the Route146 pointwise atoms.

Drop-in provider

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

Drop-in Route169 candidate lift-partition provider.

This has the same B T Q call shape as centralCover_candidateLiftPartitionData_from_candidateRoute167Closers, but its closure is lowered from the seven Route168 pointwise atoms to the two actual middle/Frattini inputs above.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateRoute169Closers_canonical {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Canonical-tower spelling for integration routes that keep the canonical quotient tower in scope.

theorem Q2Presentation.Induction.centralCover_candidateRoute169LiftPartitionReplay {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty ((_ : CentralCoverCandidateMiddleFrattiniResidualProofData B T) × CentralCoverCandidateLiftPartitionData B)

Audit replay exposing the selected Route169 packet together with the route-ready lift partition it determines.