Candidate Route192 pointwise-to-actual closers

Route191's candidate side exposes the seven Route146 pointwise scalar/Frattini atoms. This candidate-only wrapper reuses the existing Route169 actual split as the Route192 insertion point: the pointwise atoms are replaced by the two actual Section 8 inputs for the selected middle R-obstruction and matching Frattini affine-fibre exact-image equivalence.

No target, kernel, or pushout data is introduced here.

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

Route192 selected actual middle/Frattini split.

This exposes the exact lower candidate surface used to replace the seven Route191 pointwise atoms.

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

Route192 coherent middle/Frattini packet without the Route146 pointwise atoms.

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

Drop-in Route192 candidate lift-partition provider.

The call shape matches the Route190 pointwise provider used by Route191, but the axiom closure uses the two actual middle/Frattini inputs instead of the seven pointwise atoms.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateRoute192PointwiseActualClosers_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.