Documentation

Q2Presentation.Induction.CandidateRoute124ExactImageClosers

Candidate Route124 exact-image closers #

This sidecar is a Route124-named wrapper around the already verified current semantic exact-image split from CandidateRoute113ExactImageClosers.

The current public candidate branch calls centralCover_candidateLiftPartitionData_from_exactImageFinalClosers, whose closure still contains the two exact-image residual atoms

The theorems below keep the same downstream consumer shape but route the candidate packet through the smaller current semantic packets exposed by CandidateCurrentPacketSplitClosers:

No theorem below calls either exact-image residual axiom directly, and no local/CFT axiom is touched.

Route124 wrappers for the current semantic exact-image split #

source
@[reducible, inline]
abbrev Q2Presentation.Induction.CentralCoverCandidateRoute124ExactImageData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) :
Type

Route124 candidate exact-image data, using the same coherent direct packet as the Route113 current semantic split.

Equations
Instances For
    source
    theorem Q2Presentation.Induction.centralCover_candidateDirectExactImageResidualData_from_route124ExactImageClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) :
    Nonempty (CentralCoverCandidateDirectExactImageResidualData B T)

    Coherent direct exact-image residual data from the smaller current semantic split: middle scalar obstruction evaluator plus Frattini affine-fibre coordinate packet.

    source
    theorem Q2Presentation.Induction.centralCover_candidateRoute124ExactImageData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) :
    Nonempty (CentralCoverCandidateRoute124ExactImageData B T)

    Route124 exact-image packet from the smaller current semantic split.

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

    Route124 dependent residual-pair replacement.

    This proves the pair shape needed to replace the two current exact-image residual axioms, but its closure is the smaller current semantic pair.

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

    Route124 replacement for centralCover_candidateMiddleExactImageObstructionEvaluationData_residual.

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

    Route124 replacement for centralCover_candidateTopExactImageAffineFiberEquivData_residual.

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

    Final exact-image residual data for Route124, assembled from the smaller current semantic split.

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

    Route-ready semantic R-lift data for the Route124 candidate branch.

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

    Drop-in Route124 candidate provider.

    This has the same canonical consumer shape as centralCover_candidateLiftPartitionData_from_exactImageFinalClosers, but its candidate closure avoids the two exact-image residual axioms and is instead the two current semantic packets.

    source
    theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_route124ExactImageAudit {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) :
    Nonempty ((_ : CentralCoverCandidateMiddleScalarObstructionEvaluatorData B D.tower) × (O : CentralCoverCandidateMiddleRLiftObstructionMapData B D.tower) × CentralCoverCandidateFrattiniAffineFiberCoordinateData B D.tower O × CentralCoverCandidateLiftPartitionData B)

    Audit surface exposing the lower candidate packets used by the Route124 provider.