Candidate scalar/Frattini route44 proofs

Route44 is a candidate Section 8 cleanup sidecar. It keeps the Route43 drop-in provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but avoids the seven Route43 candidate leaves in the route-ready proof path.

Scalar side:

• scalar-pushout values are not taken as independent pointwise data;
• they are obtained by evaluating the selected R-valued obstruction map against lambda : X_R;
• additivity is theorem-level from the linear-map structure of the obstruction value.

Frattini side:

• the arbitrary base/fibre coordinate leaves are not used;
• coordinates, realization, and the two inverse laws are the two directions of the exact affine-fibre partition.

The remaining candidate residuals are the lower exact-image packets already isolated in CandidateExactImagePacketClosers:

• centralCover_candidateObstructionMapData;
• centralCover_candidateFrattiniExactImageCardinalityData.

These are concrete Section 8 residuals: the obstruction map on the canonical middle exact-image index, and the finite Frattini exact-image cardinality statement that recovers the partition.

Scalar pushouts from the selected R-obstruction map

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.route44ScalarPushoutValueAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (lam : ↥B.XR) : CentralCoverCandidateMiddleScalarPushoutValueAtData B T lam

The scalar-pushout value at lambda, obtained by evaluating the selected R-valued middle obstruction map.

Equations

• D.route44ScalarPushoutValueAtData lam = { valueAt := fun (x : Q2Presentation.Induction.centralCoverCandidateMiddleSource T) => (D.obstruction x) lam }

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

The selected scalar-pushout family induced by the middle obstruction map.

Equations

• D.route44ScalarPushoutFamilyData = { valueAt := fun (lam : ↥B.XR) => D.route44ScalarPushoutValueAtData lam }

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.route44ScalarPushoutAdditivityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : CentralCoverCandidateMiddleScalarPushoutAdditivityData D.route44ScalarPushoutFamilyData

Additivity in lambda follows from linearity of the obstruction value in B.obstructionSpace.

Equations

• D.route44ScalarPushoutAdditivityData = { map_add := ⋯ }

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

Route44 closes the pointwise scalar-pushout value leaf by evaluating the selected middle R-obstruction map.

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

Route44 supplies additivity for the selected scalar-pushout family induced by the middle R-obstruction map. This is the route-needed replacement for the Route43 arbitrary-family additivity leaf.

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

Route44 scalar-obstruction evaluator. Homogeneity over ZMod 2 remains theorem-level from additivity.

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

Route44 middle R-lift obstruction map, exposed directly from the lower exact-image obstruction-map packet.

Frattini coordinates from the exact affine-fibre partition

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

Route44 exact affine-fibre partition, recovered from the lower Frattini cardinality packet for the selected middle obstruction map.

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

Route44 base coordinate induced by the exact affine-fibre partition.

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

Route44 selected base/fibre coordinate pair induced by the exact affine-fibre partition. This replaces the Route43 arbitrary-base fibre coordinate leaf in the route-ready path.

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

Route44 curried realization induced by the inverse exact affine-fibre partition.

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

Route44 selected Frattini coordinate system and both inverse laws, all induced by one exact affine-fibre partition.

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

Route44 affine-fibre coordinate data induced by the selected partition coordinate system.

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

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

Route-ready reassembly

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

Route44 direct exact-image residual data from the exact-image obstruction map and matching Frattini partition.

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

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

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

Drop-in Route44 candidate lift-partition provider.

The closure of this theorem no longer contains the seven Route43 candidate scalar/Frattini leaves.