Candidate Route113 exact-image closers

This sidecar targets the two candidate exact-image residuals visible in IntegratedCurrentRouteProofs113:

• centralCover_candidateMiddleExactImageObstructionEvaluationData_residual;
• centralCover_candidateTopExactImageAffineFiberEquivData_residual.

The older Route112 attack sidecar routes these residuals through the Route106 scalar/Frattini coordinate packet, whose audit frontier is the seven coordinate leaves from the scalar-pushout and Frattini-coordinate split. The present sidecar is stricter: it routes the same exact-image pair through the current semantic split in CandidateCurrentPacketSplitClosers.

Thus the candidate closure is lowered to the two manuscript-shaped current Section 8 packets:

• centralCover_candidateMiddleScalarObstructionEvaluatorData;
• centralCover_candidateFrattiniAffineFiberCoordinateData.

No theorem below calls the two Route113 residual axioms, and no theorem touches any local/CFT axiom.

Route113 candidate exact-image packet

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

Route113 candidate exact-image data, lowered to the current semantic split.

It packages the selected middle R-lift obstruction on the canonical middle exact-image source together with the matching Frattini exact-image partition for its affine fibres.

• direct : CentralCoverCandidateDirectExactImageResidualData B T

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

The middle exact-image obstruction-evaluation packet selected by the Route113 current semantic data.

Equations

• D.middleEvaluation = D.direct.middleEvaluation

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

The top affine-fibre equivalence attached to the same selected middle obstruction evaluation.

Equations

• D.topAffineFiberEquiv = D.direct.topAffineFiberEquiv

def Q2Presentation.Induction.CentralCoverCandidateRoute113ExactImageData.residualPair {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute113ExactImageData B T) : (E : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T) × CentralCoverCandidateTopExactImageAffineFiberEquivData B T E

The dependent residual-pair shape used to audit replacement of the two current exact-image residual axioms.

Equations

• D.residualPair = ⟨D.middleEvaluation, D.topAffineFiberEquiv⟩

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

Final residual data induced by the current semantic split.

Equations

• D.finalResidualData = D.direct.finalResidualData

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

Semantic R-lift data for a supplied quotient-frame map.

Equations

• D.rLiftSemanticData Q = D.direct.rLiftSemanticData Q

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

Candidate lift-partition data for a supplied quotient-frame map.

Equations

• D.liftPartitionData Q = D.direct.liftPartitionData Q

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

Coherent direct exact-image residual data from the current semantic split.

This theorem is the key improvement over the Route112 exact-image attack: the closure goes directly through CandidateCurrentPacketSplitClosers, rather than through the seven Route106 scalar/Frattini coordinate leaves.

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

Route113 exact-image packet from the current semantic split.

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

Route113 dependent residual-pair replacement.

This proves the current pair target from the lower current semantic split and avoids both exact-image residual axioms exposed by Route113.

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

Current middle exact-image residual shape, proved from the current semantic split instead of from centralCover_candidateMiddleExactImageObstructionEvaluationData_residual.

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

Current top exact-image affine-fibre residual shape, proved from the current semantic split instead of from centralCover_candidateTopExactImageAffineFiberEquivData_residual.

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

Final exact-image residual data from the Route113 current semantic split.

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

Route-ready semantic R-lift data for the canonical Route113 tower.

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

Drop-in Route113 candidate provider.

This has the same canonical consumer shape as centralCover_candidateLiftPartitionData_from_exactImageFinalClosers, but its candidate closure is the current semantic two-packet frontier, not the two broad Route113 residuals and not the seven Route106 coordinate leaves.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_route113ExactImageAudit {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 current semantic objects used by the route-ready lift-partition provider.

The theorem statement deliberately exposes the scalar obstruction evaluator and a Frattini affine-fibre coordinate packet; the selected middle obstruction map is assembled theorem-level from the scalar evaluator.