Documentation

Q2Presentation.Induction.CandidateAffineLiftComponentProofs

Candidate affine-lift component proofs #

This sidecar gives the final Section 8 candidate route a narrower input than the three arbitrary elementary-tower component residuals used by CandidateAffineLiftActualProofs.lean.

The packet consumed here is the canonical candidate concrete packet attached to a supplied canonical target quotient tower D : CentralCoverTargetCanonicalQuotientTowerData B. Thus the quotient-frame map, middle R-lift obstruction, and Frattini affine-fibre equivalence all belong to the same manuscript tower Y -> Y/R -> Y/K; there is no arbitrary bare T detached from the actual block.

Canonical component projections #

source
theorem Q2Presentation.Induction.centralCover_candidateQuotientFrameMapData_from_candidateAffineLiftComponentProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) :
Nonempty (CentralCoverCandidateQuotientFrameMapData B D.tower)

Canonical quotient-frame component for the supplied quotient tower.

source
theorem Q2Presentation.Induction.centralCover_candidateMiddleRLiftObstructionMapData_from_candidateAffineLiftComponentProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) :
Nonempty (CentralCoverCandidateMiddleRLiftObstructionMapData B D.tower)

Canonical middle R-lift obstruction component for the supplied quotient tower.

source
theorem Q2Presentation.Induction.centralCover_candidateFrattiniCoverData_from_candidateAffineLiftComponentProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) :
Nonempty ((E : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B D.tower) × CentralCoverCandidateFrattiniCoverData B D.tower E.obstructionEvaluationData)

Canonical Frattini-cover component, only for the middle obstruction chosen by the same canonical candidate packet.

Route-ready coherent candidate affine lift data #

source
theorem Q2Presentation.Induction.centralCover_candidateChosenAffineLiftActualData_from_candidateAffineLiftComponentProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) :
Nonempty (CentralCoverCandidateChosenAffineLiftActualData B D.tower)

Coherent chosen affine-lift data from the canonical component packet.

This has the same shape as centralCover_candidateChosenAffineLiftActualData, but its closure is the canonical quotient-tower packet rather than the three arbitrary-tower residuals.

source
theorem Q2Presentation.Induction.centralCover_candidateRLiftSemanticData_from_candidateAffineLiftComponentProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) :
Nonempty (CentralCoverCandidateRLiftSemanticData B D.tower)

Candidate semantic R-lift data for the canonical quotient tower.

source
theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateAffineLiftComponentProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) :
Nonempty (CentralCoverCandidateLiftPartitionData B)

Route-ready replacement for centralCover_candidateLiftPartitionData_from_candidateAffineLiftActualProofs when the final proof already has the canonical quotient tower Dcan.