Candidate Route98 coordinate closers

This sidecar is candidate Section 8 only. It does not edit any integrated route file.

Route98 currently consumes

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

through centralCover_candidateLiftPartitionData_from_route94. The candidate closure of that provider still exposes the two current Section 8 packets:

• centralCover_candidateMiddleScalarObstructionEvaluatorData;
• centralCover_candidateFrattiniAffineFiberCoordinateData.

This file lowers those packets to the coherent route-needed data isolated in CandidateScalarFrattiniCurrentProofs: one selected scalar-pushout evaluator with linearity for that same choice, and one selected Frattini coordinate/realization/inverse tuple attached to the induced middle obstruction.

Route98 selected scalar/Frattini coordinate datum

def Q2Presentation.Induction.CentralCoverCandidateMiddleScalarPushoutCoherentData.middleRLiftObstructionMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateMiddleScalarPushoutCoherentData B T) : CentralCoverCandidateMiddleRLiftObstructionMapData B T

The middle R-lift obstruction map induced by a coherent selected scalar-pushout evaluator.

Equations

• S.middleRLiftObstructionMapData = { obstruction := S.evaluatorData.obstructionEvaluator }

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

Route98 selected coordinate datum.

This is the coherent candidate-side Section 8 datum needed at the route call site: the selected scalar-pushout evaluator determines the middle R-valued obstruction, and the Frattini coordinates are attached to that same obstruction.

• scalar : CentralCoverCandidateMiddleScalarPushoutCoherentData B T
• frattini : CentralCoverCandidateFrattiniCoordinateCoherentData B T self.scalar.middleRLiftObstructionMapData

def Q2Presentation.Induction.CentralCoverCandidateRoute98CoordinateData.middleScalarObstructionEvaluatorData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute98CoordinateData B T) : CentralCoverCandidateMiddleScalarObstructionEvaluatorData B T

Scalar-obstruction evaluator projected from the selected Route98 data.

Equations

• D.middleScalarObstructionEvaluatorData = D.scalar.evaluatorData

def Q2Presentation.Induction.CentralCoverCandidateRoute98CoordinateData.middleRLiftObstructionMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute98CoordinateData B T) : CentralCoverCandidateMiddleRLiftObstructionMapData B T

Middle R-lift obstruction map projected from the selected Route98 data.

Equations

• D.middleRLiftObstructionMapData = D.scalar.middleRLiftObstructionMapData

def Q2Presentation.Induction.CentralCoverCandidateRoute98CoordinateData.frattiniAffineFiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute98CoordinateData B T) : CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D.middleRLiftObstructionMapData

Frattini affine-fibre coordinate packet projected from the selected Route98 data.

Equations

• D.frattiniAffineFiberCoordinateData = D.frattini.coordinateData

def Q2Presentation.Induction.CentralCoverCandidateRoute98CoordinateData.frattiniExactImage {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute98CoordinateData B T) : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.middleRLiftObstructionMapData.obstructionIndexToBaseMapData.O D.middleRLiftObstructionMapData.affineFiberTorsorData.Z D.middleRLiftObstructionMapData.affineFiberTorsorData.F

Frattini exact-image partition carried by the selected coordinate packet.

Equations

• D.frattiniExactImage = { partition := { bij := D.frattiniAffineFiberCoordinateData.equiv } }

def Q2Presentation.Induction.CentralCoverCandidateRoute98CoordinateData.directExactImageResidualData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute98CoordinateData B T) : CentralCoverCandidateDirectExactImageResidualData B T

Coherent direct exact-image residual data recovered from Route98 selected coordinate data.

Equations

• D.directExactImageResidualData = { middleObstruction := D.middleRLiftObstructionMapData, frattiniPartition := D.frattiniExactImage }

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

Reassemble the candidate lift partition from Route98 selected coordinate data and the route-supplied quotient-frame map.

Equations

• D.liftPartitionData Q = D.directExactImageResidualData.liftPartitionData Q

Route98 public projections

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

Coherent Route98 coordinate packet from the current smaller scalar and Frattini residuals.

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

Route98 scalar-obstruction evaluator, lowered to the coherent selected scalar-pushout packet.

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

Route98 middle R-lift obstruction map, lowered to the coherent selected scalar-pushout packet.

theorem Q2Presentation.Induction.centralCover_candidateSelectedFrattiniAffineFiberCoordinateData_from_route98 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) × CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D)

Selected Route98 Frattini coordinate packet, attached to the middle obstruction selected by the Route98 scalar data.

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

Route98 Frattini coordinate packet for a supplied middle obstruction, lowered to the coherent Frattini coordinate residual.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberPartition_from_route98 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) × CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F)

Frattini exact-image partition recovered from the selected Route98 coordinate packet.

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

Coherent direct exact-image residual data through the Route98 selected coordinate packet.

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

Route98 drop-in candidate lift-partition provider.

This has the same public call shape as centralCover_candidateLiftPartitionData_from_route94, but its candidate closure lowers the two current Route98 packet names to:

• centralCover_candidateMiddleScalarPushoutCoherentData;
• centralCover_candidateFrattiniCoordinateCoherentData.