Candidate Route161 closers

Route160's candidate side currently exposes two actual Section 8 leaves:

• centralCover_candidateActualMiddleRLiftObstructionMapData;
• centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

This sidecar lowers both to the scalar/Frattini semantic packets matching lem:obstructionseparation and prop:finalfourier in the manuscript:

• scalar pushout values for the middle R-obstruction;
• linearity of those values in lambda : X_R;
• Frattini lift coordinates;
• Frattini realizations;
• inverse laws for the coordinate/realization pair.

It does not call the old broad packets centralCover_candidateMiddleFrattiniResidualProofData, centralCover_candidateObstructionMapData, or centralCover_candidateFrattiniExactImageCardinalityData.

Route161 replacements for the two Route160 actual leaves

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

Route161 replacement for centralCover_candidateActualMiddleRLiftObstructionMapData.

The target type is unchanged, but the proof routes through the lower scalar pushout value and linearity packets.

theorem Q2Presentation.Induction.centralCover_candidateActualFrattiniAffineFiberExactImageEquivData_from_candidateRoute161Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (O : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty (CentralCoverCandidateFrattiniExactImageEquivData B T O.obstructionIndexToBaseMapData.O O.affineFiberTorsorData.Z O.affineFiberTorsorData.F)

Route161 replacement for centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

The selected middle obstruction is kept fixed; the equivalence is recovered from the lower Frattini affine-fibre partition supplied by the coordinate, realization, and inverse-law packets.

Coherent Route161 exact-image packet

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

Coherent Route161 candidate actual exact-image data.

This packages the selected middle obstruction and the matching Frattini exact-image equivalence while keeping the two Route160 actual axiom names out of the proof closure.

• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T
• frattiniEquiv : CentralCoverCandidateFrattiniExactImageEquivData B T self.middleObstruction.obstructionIndexToBaseMapData.O self.middleObstruction.affineFiberTorsorData.Z self.middleObstruction.affineFiberTorsorData.F

def Q2Presentation.Induction.CentralCoverCandidateRoute161ActualExactImageData.middleFrattiniResidualProofData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute161ActualExactImageData B T) : CentralCoverCandidateMiddleFrattiniResidualProofData B T

Route161 data repackaged in the current coherent middle/Frattini residual type.

Equations

• D.middleFrattiniResidualProofData = { middleObstruction := D.middleObstruction, frattiniEquiv := D.frattiniEquiv }

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

Candidate lift-partition data recovered from Route161 exact-image data and the route-supplied quotient-frame map.

Equations

• D.liftPartitionData Q = D.middleFrattiniResidualProofData.liftPartitionData Q

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

Route161 coherent actual exact-image provider from the two lowered same-target replacements above.

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

Coherent middle/Frattini residual data through the Route161 exact-image packet.

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

Drop-in Route161 candidate lift-partition provider.

This has the same B T Q call shape as the current Route157 provider used by Route160, but its axiom frontier is the five scalar/Frattini semantic packets rather than the two Route160 actual Section 8 leaves.

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

Canonical-tower spelling for routes that keep the canonical quotient tower in scope.