Candidate Route194 actual-to-current-semantic lowering

Route192's candidate insertion point reaches the two actual Section 8 candidate leaves

• centralCover_candidateActualMiddleRLiftObstructionMapData;
• centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

This sidecar keeps the exact Route192 downstream B T Q call shape, but routes through CandidateRoute172Closers. Thus the candidate side is lowered from the two actual leaves to the current scalar-obstruction evaluator and Frattini affine-fibre coordinate packets:

• centralCover_candidateMiddleScalarObstructionEvaluatorData;
• centralCover_candidateFrattiniAffineFiberCoordinateData.

No target, kernel, pushout, local/CFT, or terminal data is introduced here.

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

Route194 selected lower middle/Frattini split.

This has the same dependent shape as Route192's selected actual split, but it is proved through Route172's current semantic packets rather than through centralCover_candidateActualMiddleRLiftObstructionMapData and centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

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

Route194 coherent middle/Frattini packet with the actual Route192 leaves removed from the closure.

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

Drop-in Route194 candidate lift-partition provider.

This is the only theorem the integrated route needs. Its input/output surface matches Route192's provider exactly, while its axiom closure is the Route172 current semantic candidate closure.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateRoute194ActualLowerClosers_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 in scope.

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

Audit replay exposing the lowered selected packet and the route-ready lift partition it determines.