Direct candidate exact-image residual proofs

This sidecar targets the two candidate Section 8 residuals currently visible in the final route:

• centralCover_candidateMiddleExactImageObstructionEvaluationData_residual;
• centralCover_candidateTopExactImageAffineFiberEquivData_residual.

It does not route through the older broad packets centralCover_candidateObstructionMapData or centralCover_candidateFrattiniExactImageCardinalityData. Instead it uses the strictly finer manuscript-shaped packets already isolated below the current residuals:

• the middle R-lift obstruction map on the canonical middle exact-image source;
• the Frattini exact-image partition for the canonical affine fibres.

Coherent finer packet

structure Q2Presentation.Induction.CentralCoverCandidateDirectExactImageResidualData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Type

Coherent direct exact-image data for one elementary quotient tower.

This is smaller than the two current residuals as a route object: it records the actual middle R-obstruction map and the matching Frattini partition, not an arbitrary top affine-fibre equivalence detached from its chosen obstruction.

• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T
• frattiniPartition : CentralCoverCandidateFrattiniExactImageSurjectivityData B T self.middleObstruction.obstructionIndexToBaseMapData.O self.middleObstruction.affineFiberTorsorData.Z self.middleObstruction.affineFiberTorsorData.F

def Q2Presentation.Induction.CentralCoverCandidateDirectExactImageResidualData.middleEvaluation {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateDirectExactImageResidualData B T) : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T

Repackage the middle R-lift obstruction map as the current middle exact-image obstruction evaluation object.

Equations

• D.middleEvaluation = Q2Presentation.Induction.CentralCoverCandidateMiddleExactImageObstructionEvaluationData.ofMiddleRLiftObstructionMapData D.middleObstruction

def Q2Presentation.Induction.CentralCoverCandidateDirectExactImageResidualData.topAffineFiberEquiv {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateDirectExactImageResidualData B T) : CentralCoverCandidateTopExactImageAffineFiberEquivData B T D.middleEvaluation

Repackage the Frattini exact-image partition as the current top exact-image affine-fibre equivalence for the chosen middle obstruction evaluation.

Equations

• D.topAffineFiberEquiv = { frattiniEquiv := have E := { equiv := D.frattiniPartition.partition.bij }; id E }

def Q2Presentation.Induction.CentralCoverCandidateDirectExactImageResidualData.finalResidualData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateDirectExactImageResidualData B T) : CentralCoverCandidateExactImageFinalResidualData B T

Reassemble the final residual structure from the direct finer data.

Equations

• D.finalResidualData = { middleEvaluation := D.middleEvaluation, frattiniEquiv := D.topAffineFiberEquiv }

def Q2Presentation.Induction.CentralCoverCandidateDirectExactImageResidualData.rLiftSemanticData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateDirectExactImageResidualData B T) (Q : CentralCoverCandidateQuotientFrameMapData B T) : CentralCoverCandidateRLiftSemanticData B T

Reassemble semantic central R-lift data once the quotient-frame map has provided the top-to-middle exact-image base quotient.

Equations

• D.rLiftSemanticData Q = D.finalResidualData.rLiftSemanticData (Q2Presentation.Induction.CentralCoverCandidateActualTopToMiddlePostcompData.ofQuotientFrameMap Q).exactImageBaseQuotient

def Q2Presentation.Induction.CentralCoverCandidateDirectExactImageResidualData.liftPartitionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateDirectExactImageResidualData B T) (Q : CentralCoverCandidateQuotientFrameMapData B T) : CentralCoverCandidateLiftPartitionData B

Reassemble the candidate lift partition from the direct finer data and the route-supplied quotient-frame map.

Equations

• D.liftPartitionData Q = D.finalResidualData.liftPartitionData Q

Finer residuals imply the current residual shapes

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

Coherent direct exact-image residual data from the strictly finer packets: middle R-lift obstruction map plus matching Frattini exact-image partition.

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

Current middle exact-image residual, proved directly from the finer middle R-lift obstruction map packet.

theorem Q2Presentation.Induction.centralCover_candidateTopExactImageAffineFiberEquivData_from_directResidualProofs {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T) : Nonempty (CentralCoverCandidateTopExactImageAffineFiberEquivData B T D)

Current top exact-image affine-fibre residual, proved directly from the finer Frattini exact-image partition attached to the same middle obstruction evaluation.

Route-ready reassembly

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

Final candidate exact-image residual data from the direct finer split.

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

Semantic central R-lift data from the direct finer split and a route-supplied quotient-frame map.

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

Candidate lift-partition data from the direct finer split and a route-supplied quotient-frame map.