Candidate scalar/Frattini route42 proofs

Route42 keeps the Route41 drop-in provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but narrows the candidate Section 8 residuals used by the provider.

Scalar side:

• Route41 used pointwise scalar-pushout values, additivity, and homogeneity.
• Route42 asks only for the selected scalar-pushout family used by the middle R-obstruction, together with additivity for that same family.
• Homogeneity over ZMod 2 is recovered theorem-level from the Route36 additivity argument.

Frattini side:

• Route41 exposed base coordinate, fibre coordinate, fibre realization, and two inverse-law leaves as independent arbitrary packets.
• Route42 asks for one coherent coordinate system: the selected base/fibre coordinates, selected curried realization, and the two inverse laws tying exactly those maps together.

The residual axioms in this file are still semantic inputs from manuscript Section 8 (lem:obstructionseparation, lem:affinelifting, and prop:finalfourier), but they are the route-needed coherent data rather than the stronger arbitrary-family/arbitrary-coordinate Route41 packets.

Route42 scalar packet: selected additive scalar-pushout family

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

Route42 selected scalar-pushout family.

Manuscript meaning: for the fixed elementary quotient tower, this is the family of scalar obstruction tests lambda_* o_R : X_Gamma(B) -> F_2 from lem:obstructionseparation, together with additivity in the invariant scalar pushout character lambda : X_R. It is intentionally the selected family used to assemble the R-valued obstruction, not an arbitrary externally supplied family and not a separate homogeneity axiom.

• scalarFamily : CentralCoverCandidateMiddleScalarPushoutFamilyData B T
• additivity : CentralCoverCandidateMiddleScalarPushoutAdditivityData self.scalarFamily

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

Route42 scalar residual: the selected additive scalar-pushout family from Section 8, lem:obstructionseparation.

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutValueAtData_from_scalarFrattiniRoute42 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (lam : ↥B.XR) : Nonempty (CentralCoverCandidateMiddleScalarPushoutValueAtData B T lam)

Route41 pointwise scalar-pushout values recovered from the selected Route42 family.

theorem Q2Presentation.Induction.centralCover_candidateRoute42SelectedScalarPushoutAdditivityData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) × CentralCoverCandidateMiddleScalarPushoutAdditivityData V)

Route42 supplies additivity for its selected scalar-pushout family.

This is the route-needed replacement for Route41's arbitrary-family additivity packet.

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

Route42 scalar-obstruction evaluator.

The only scalar residual used here is the selected additive scalar family; homogeneity is derived theorem-level over ZMod 2.

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

Route42 middle R-lift obstruction map from the selected scalar route.

Route42 Frattini packet: one coherent coordinate system

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

Route42 Frattini coordinate system.

Manuscript meaning: for the selected middle R-obstruction, this is the actual affine-fibre identification from lem:affinelifting and prop:finalfourier: a top exact-image candidate map is sent to its unobstructed middle base point and affine R-lift coordinate, and the curried Frattini realization map is inverse to those coordinates. The inverse laws are part of the same coherent packet, so the route no longer assumes them for arbitrary unrelated coordinate and realization choices.

• baseCoordinate : CentralCoverCandidateFrattiniBaseCoordinateData B T D
• fiberCoordinate : CentralCoverCandidateFrattiniFiberCoordinateData self.baseCoordinate
• fiberRealization : CentralCoverCandidateFrattiniFiberRealizationData B T D
• realizeLift : CentralCoverCandidateFrattiniRealizeLiftCoordinateData self.baseCoordinate self.fiberCoordinate self.fiberRealization
• liftRealize : CentralCoverCandidateFrattiniLiftCoordinateRealizeData self.baseCoordinate self.fiberCoordinate self.fiberRealization

def Q2Presentation.Induction.CentralCoverCandidateRoute42FrattiniCoordinateSystemData.liftCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (S : CentralCoverCandidateRoute42FrattiniCoordinateSystemData B T D) : CentralCoverCandidateFrattiniLiftCoordinateData B T D

The uncurried lift-coordinate map determined by the Route42 coherent coordinate system.

Equations

• S.liftCoordinateData = S.baseCoordinate.liftCoordinateData S.fiberCoordinate

def Q2Presentation.Induction.CentralCoverCandidateRoute42FrattiniCoordinateSystemData.realizationData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (S : CentralCoverCandidateRoute42FrattiniCoordinateSystemData B T D) : CentralCoverCandidateFrattiniRealizationData B T D

The uncurried realization map determined by the Route42 coherent coordinate system.

Equations

• S.realizationData = S.fiberRealization.realizationData

def Q2Presentation.Induction.CentralCoverCandidateRoute42FrattiniCoordinateSystemData.inverseData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (S : CentralCoverCandidateRoute42FrattiniCoordinateSystemData B T D) : CentralCoverCandidateFrattiniCoordinateInverseData S.liftCoordinateData S.realizationData

The inverse-law packet for the uncurried maps determined by the Route42 coherent coordinate system.

Equations

• S.inverseData = { realize_liftCoordinate := ⋯, liftCoordinate_realize := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateRoute42FrattiniCoordinateSystemData.affineFiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (S : CentralCoverCandidateRoute42FrattiniCoordinateSystemData B T D) : CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D

The current Frattini affine-fibre coordinate packet induced by the Route42 coherent coordinate system.

Equations

• S.affineFiberCoordinateData = S.liftCoordinateData.coordinateData S.realizationData S.inverseData

axiom Q2Presentation.Induction.centralCover_candidateRoute42FrattiniCoordinateSystemData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty (CentralCoverCandidateRoute42FrattiniCoordinateSystemData B T D)

Route42 Frattini residual: the coherent coordinate/realization system from Section 8, lem:affinelifting and prop:finalfourier.

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

Route41 base-coordinate shape recovered from the coherent Route42 Frattini system.

theorem Q2Presentation.Induction.centralCover_candidateRoute42FrattiniBaseFiberCoordinateData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty ((C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) × CentralCoverCandidateFrattiniFiberCoordinateData C)

Route42 supplies the fibre coordinate for the same selected base coordinate. This replaces Route41's arbitrary-base fibre-coordinate packet.

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

Route41 fibre-realization shape recovered from the coherent Route42 Frattini system.

theorem Q2Presentation.Induction.centralCover_candidateRoute42FrattiniCoordinateSystemSigma {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty ((C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) × (F : CentralCoverCandidateFrattiniFiberCoordinateData C) × (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) × CentralCoverCandidateFrattiniRealizeLiftCoordinateData C F R × CentralCoverCandidateFrattiniLiftCoordinateRealizeData C F R)

The full selected Frattini coordinate system and both inverse laws.

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

Current Frattini affine-fibre coordinate data assembled from Route42's coherent coordinate system.

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

Route42 Frattini exact-image partition for the selected middle obstruction.

Route-ready reassembly

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

Route42 direct exact-image residual data from the selected additive scalar family and coherent Frattini coordinate system.

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

Route42 semantic central R-lift data from the direct exact-image split and a route-supplied quotient-frame map.

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

Drop-in Route42 candidate lift-partition provider.

Compared with Route41, the public provider no longer depends on the three Route41 scalar leaves or the five independent Route41 Frattini leaves. Its non-local candidate frontier is the two coherent Route42 packets:

• centralCover_candidateRoute42ScalarPushoutSelectedFamilyData;
• centralCover_candidateRoute42FrattiniCoordinateSystemData.