Candidate Route145 closers

Route144 currently obtains candidate Section 8 lift-partition data from CandidateRoute130Closers, whose axiom closure still contains the two semantic exact-image leaves

• centralCover_candidateMiddleExactImageObstructionEvaluationData_residual;
• centralCover_candidateTopExactImageAffineFiberEquivData_residual.

This sidecar leaves Route144 untouched and exposes a same-shape replacement provider for a future Route145 call site:

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

The implementation routes through the Route106 coordinate lowering. Its remaining candidate assumptions are the smaller manuscript-shaped scalar and Frattini coordinate packets: nonzero scalar values, nonzero-distinct scalar additivity, Frattini base/fibre coordinates, curried realization, and the two inverse laws.

Coherent lowering of the two Route144 candidate leaves

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

Route145 coherent final exact-image residual data.

This replaces the two Route144 semantic leaves as a paired object: the selected middle obstruction and the top affine-fibre equivalence are both assembled from the same Route106 scalar/Frattini coordinate packet.

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

Route145 selected middle obstruction evaluation, projected from the coherent Route106 lowering.

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

Route145 selected middle/top pair.

The top affine-fibre equivalence is exposed for the same middle evaluation chosen by the lower scalar/Frattini packet, avoiding the older arbitrary-tower semantic residual pair.

Route145 drop-in provider

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

Drop-in Route145 candidate lift-partition provider.

The argument shape matches the Route144 candidate call site, replacing centralCover_candidateLiftPartitionData_from_candidateRoute130Closers B T Q.

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

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

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

Audit surface exposing the selected lower Route106 packet together with the route-ready lift partition it determines.