Coherent candidate affine-lift packet

This sidecar replaces the three current arbitrary-tower candidate Section 8 semantic residuals by one coherent chosen packet.

The important dependency is that the middle obstruction evaluation and the top affine-fibre equivalence are chosen together. This avoids proving a top affine-fibre equivalence for an arbitrary obstruction function, which is stronger than the manuscript's Section 8 construction.

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

Coherent candidate affine-lift data for one elementary quotient tower.

The packet keeps the quotient-frame map, the middle R-lift obstruction, and the top exact-image affine-fibre equivalence tied to the same obstruction map.

• quotientFrame : CentralCoverCandidateQuotientFrameMapData B T
• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T
• topAffineFiberEquiv : CentralCoverCandidateFrattiniExactImageEquivData B T self.middleObstruction.obstructionIndexToBaseMapData.O self.middleObstruction.affineFiberTorsorData.Z self.middleObstruction.affineFiberTorsorData.F

axiom Q2Presentation.Induction.centralCover_candidateChosenAffineLiftActualData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateChosenAffineLiftActualData B T)

Coherent candidate affine-lift input.

This is the strictly narrower replacement for the three independent current semantic residuals:

• centralCover_candidateActualTopToMiddlePostcompData_residual,
• centralCover_candidateMiddleExactImageObstructionEvaluationData_residual,
• centralCover_candidateTopExactImageAffineFiberEquivData_residual.

It records only the manuscript-shaped chosen obstruction and its matching affine-fibre equivalence.

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

The chosen middle obstruction as the current exact-image evaluation packet.

Equations

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

def Q2Presentation.Induction.CentralCoverCandidateChosenAffineLiftActualData.actualPostcomp {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateChosenAffineLiftActualData B T) : CentralCoverCandidateActualTopToMiddlePostcompData B T

The chosen quotient-frame map gives actual top-to-middle postcomposition.

Equations

• D.actualPostcomp = Q2Presentation.Induction.CentralCoverCandidateActualTopToMiddlePostcompData.ofQuotientFrameMap D.quotientFrame

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

The chosen top affine-fibre equivalence, repackaged in the current API.

Equations

• D.topExactImageAffineFiberEquiv = { frattiniEquiv := id D.topAffineFiberEquiv }

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

Reassemble the candidate semantic R-lift packet from the coherent data.

Equations

• One or more equations did not get rendered due to their size.

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

Reassemble the coherent candidate lift-partition packet.

Equations

• One or more equations did not get rendered due to their size.

Projections to the current API fields

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

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

theorem Q2Presentation.Induction.centralCover_candidateTopExactImageAffineFiberEquivData_from_chosenAffineLiftActual {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((E : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T) × CentralCoverCandidateTopExactImageAffineFiberEquivData B T E)

The top affine-fibre equivalence projected only for the chosen middle obstruction evaluation, not for an arbitrary obstruction function.

Route-ready reassembly

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

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