Current candidate Section 8 packet split closers

This sidecar keeps the current candidate route direction:

• it does not use the retired packets centralCover_candidateMiddleExactImageObstructionEvaluationData_residual or centralCover_candidateTopExactImageAffineFiberEquivData_residual;
• it does not fall back to the older broad packets centralCover_candidateObstructionMapData or centralCover_candidateFrattiniExactImageCardinalityData.

The two current residual packet shapes are split in CandidateCurrentSemanticClosers.lean to the smallest missing semantic data currently useful in the API:

• scalar-pushout evaluations, linear in lambda in X_R, which assemble the R-valued obstruction evaluator on the canonical middle exact-image source X_Gamma(B);
• exact-image Frattini/affine-fibre coordinate and realization maps for the canonical fibres attached to the selected obstruction map.

These are the manuscript-shaped inputs from def:Xgamma, lem:obstructionseparation, lem:affinelifting, and prop:finalfourier.

Theorem-level wrappers with the current packet target types

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

Direct theorem-level replacement for centralCover_candidateMiddleRLiftObstructionMapData_residual.

Its closure names only the primitive current obstruction evaluator, not the retired middle-obstruction-evaluation packet.

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

Direct theorem-level replacement for centralCover_candidateFrattiniAffineFiberPartition_residual.

Its closure names only the primitive current Frattini exact-image bijection, not the retired top affine-fibre residual or the older broad cardinality packet.

theorem Q2Presentation.Induction.centralCover_candidateDirectExactImageResidualData_from_currentSplitClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) × CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F)

Coherent current candidate pair assembled from the split semantic packets.

This is useful for local integration experiments: it packages the current middle obstruction map with the matching Frattini partition, without invoking either current residual axiom.