Candidate R-lift/Frattini semantic residual proofs

This sidecar closes the two exact-image residual statements exposed in CandidateRLiftFrattiniClosers.lean from the smaller manuscript-shaped packets already isolated in CandidateExactImagePacketClosers.lean.

Manuscript anchors: Section 8, pages 42--49. The middle obstruction is the R-valued obstruction on the canonical exact-image source X_\Gamma(B) (def:Xgamma, lem:obstructionseparation), and the Frattini packet is the finite exact-image cardinality/partition statement used in prop:finalfourier.

Exact residual statements from smaller packets

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

The middle R-lift obstruction-map residual follows from the smaller obstruction-map packet applied to the theorem-level middle exact-image index.

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

The Frattini affine-fibre exact-image residual follows from the smaller Frattini cardinality packet for the selected middle obstruction map.

The proof keeps the obstruction map fixed: the finite index is the canonical middle exact-image source and the affine fibres are the canonical regular Z^1(R) fibres attached to that same obstruction datum.

Route-ready reassembly through the proven residuals

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

Candidate semantic R-lift data assembled from the quotient-frame closer and the two exact residual proofs in this sidecar.

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

Coherent candidate lift-partition data routed through the proven exact-image R-lift/Frattini residuals.