Candidate Route201 pointwise-to-actual closer for Route200

Route200 exposes the seven Route146 pointwise candidate scalar/Frattini atoms:

• centralCover_candidateFrattiniBaseCoordinateAtData;
• centralCover_candidateFrattiniFiberCoordinateAtData;
• centralCover_candidateFrattiniFiberRealizationAtData;
• centralCover_candidateFrattiniLiftCoordinateRealizeAtData;
• centralCover_candidateFrattiniRealizeLiftCoordinateAtData;
• centralCover_candidateMiddleScalarPushoutNonzeroDistinctAdditivityAtData;
• centralCover_candidateMiddleScalarPushoutNonzeroValueAtPointData.

This sidecar gives a Route200-shaped candidate provider which bypasses those pointwise atoms and routes through the actual Section 8 middle/Frattini split already isolated by CandidateRoute192PointwiseActualClosers:

• centralCover_candidateActualMiddleRLiftObstructionMapData;
• centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

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

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

Route201 selected actual middle/Frattini split.

This is a stable Route201 audit-facing spelling of the Route192 split, included so Route200 candidate lowerings can be audited independently of older integrated routes.

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

Route201 coherent middle/Frattini packet.

The closure of this theorem should contain the two actual Section 8 candidate inputs, not the seven Route146 pointwise atoms.

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

Drop-in Route201 candidate lift-partition provider.

The call shape matches centralCover_candidateLiftPartitionData_from_candidateRoute197PointwiseCurrentLowerClosers, which Route200 currently uses, but the candidate closure is lowered from the seven pointwise atoms to the two actual Section 8 middle/Frattini inputs.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateRoute201ActualPointwiseClosers_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_candidateRoute201ActualPointwiseAudit {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty ((_ : (O : CentralCoverCandidateMiddleRLiftObstructionMapData B T) × CentralCoverCandidateFrattiniExactImageEquivData B T O.obstructionIndexToBaseMapData.O O.affineFiberTorsorData.Z O.affineFiberTorsorData.F) × (_ : CentralCoverCandidateMiddleFrattiniResidualProofData B T) × CentralCoverCandidateLiftPartitionData B)

Audit replay exposing the Route201 actual split and the route-ready lift partition it determines.