Candidate scalar/Frattini route46 proofs

Route46 is a drop-in candidate Section 8 provider with the same public call shape as Route45:

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

Route45's provider closure has two independent coherent leaves:

• centralCover_candidateMiddleScalarPushoutCoherentData;
• centralCover_candidateFrattiniCoordinateCoherentData.

Route46 keeps the same manuscript-facing scalar/Frattini content, but ties the two pieces together in one dependent packet: the Frattini coordinate equivalence is required for the exact middle R-obstruction map induced by the chosen scalar-pushout evaluator. This removes the two Route45 leaf names from the drop-in provider closure without falling back to the older broad exact-image obstruction/cardinality packets.

Route46 coherent dependent candidate packet

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

Route46 scalar/Frattini coherent data.

The scalar packet chooses the Section 8 scalar-pushout evaluator. The Frattini packet is dependent on the middle R-obstruction map assembled from exactly that evaluator, so the coordinate/realization equivalence is matched to the selected obstruction map used by the route.

• scalarData : CentralCoverCandidateMiddleScalarPushoutCoherentData B T
• frattiniData : CentralCoverCandidateFrattiniCoordinateCoherentData B T { obstruction := self.scalarData.evaluatorData.obstructionEvaluator }

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

The selected middle R-obstruction map induced by the chosen scalar pushout evaluator.

Equations

• D.middleObstructionMapData = { obstruction := D.scalarData.evaluatorData.obstructionEvaluator }

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute46CoherentData.frattiniCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateScalarFrattiniRoute46CoherentData B T) : CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D.middleObstructionMapData

The Frattini coordinate packet attached to the selected middle obstruction map.

Equations

• D.frattiniCoordinateData = id D.frattiniData.coordinateData

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute46CoherentData.frattiniPartition {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateScalarFrattiniRoute46CoherentData B T) : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.middleObstructionMapData.obstructionIndexToBaseMapData.O D.middleObstructionMapData.affineFiberTorsorData.Z D.middleObstructionMapData.affineFiberTorsorData.F

The matching Frattini exact-image partition for the selected middle obstruction map.

Equations

• D.frattiniPartition = { partition := { bij := D.frattiniCoordinateData.equiv } }

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

Route-ready direct exact-image residual data selected by the Route46 coherent dependent packet.

Equations

• D.directExactImageResidualData = { middleObstruction := D.middleObstructionMapData, frattiniPartition := D.frattiniPartition }

axiom Q2Presentation.Induction.centralCover_candidateScalarFrattiniRoute46CoherentData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateScalarFrattiniRoute46CoherentData B T)

Remaining Route46 candidate packet.

This is the single non-local candidate Section 8 leaf used by the Route46 provider. It is intentionally dependent: the Frattini coordinate equivalence is for the middle obstruction map assembled from the chosen scalar-pushout evaluator.

Route45-shape wrappers

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

Route46 middle R-lift obstruction map from the dependent coherent packet.

theorem Q2Presentation.Induction.centralCover_candidateRoute46SelectedFrattiniPartition {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)

Route46 selected Frattini affine-fibre partition, matched to the selected middle obstruction map from the same Route46 packet.

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

Route46 direct exact-image residual data from the single dependent coherent packet.

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

Route46 semantic central R-lift data from the direct exact-image split and the quotient-frame map supplied by the integrated route.

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

Drop-in Route46 candidate lift-partition provider.

This has the same target shape as centralCover_candidateLiftPartitionData_from_scalarFrattiniRoute45, while the provider closure uses the single dependent Route46 scalar/Frattini packet instead of the two Route45 coherent leaf names.