Candidate Route172 closers

Route169 replaced the seven Route168 candidate leaves by two actual middle/Frattini atoms:

• centralCover_candidateActualMiddleRLiftObstructionMapData;
• centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

This sidecar keeps the Route169 B T Q provider shape, but proves replacement facts from the current split semantic packets instead of calling those two actual atoms. The lowering follows manuscript Section 8: the middle obstruction is assembled from scalar pushout evaluations, and the Frattini exact-image equivalence is assembled from coordinate/realization maps for the canonical affine fibres.

Route172 replacements for the two Route169 actual atoms

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

Route172 replacement for centralCover_candidateActualMiddleRLiftObstructionMapData.

The closure is the current semantic middle-obstruction evaluator, not the Route169 actual atom.

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

Route172 replacement for centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

The current split sidecar provides the exact-image partition; this theorem keeps the same equivalence target expected by Route169 consumers.

Route169-shape reassembly without the Route169 actual atoms

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

Route172 selected middle obstruction and matching Frattini exact-image equivalence, with the same dependent shape as the Route169 split.

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

Coherent Route172 middle/Frattini source packet assembled without the two Route169 actual atoms and without the older coherent middle/Frattini axiom.

Drop-in provider

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

Drop-in Route172 candidate lift-partition provider.

This has the same B T Q call shape as centralCover_candidateLiftPartitionData_from_candidateRoute169Closers, but its closure is lowered to the current middle-obstruction evaluator and Frattini coordinate/realization packets.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateRoute172Closers_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_candidateRoute172LiftPartitionReplay {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty ((_ : CentralCoverCandidateMiddleFrattiniResidualProofData B T) × CentralCoverCandidateLiftPartitionData B)

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