Candidate scalar/Frattini semantic route12 proofs

This sidecar refines the five route12 candidate scalar/Frattini semantic residuals without editing routed files:

• centralCover_candidateMiddleScalarPushoutValueData;
• centralCover_candidateMiddleScalarPushoutLinearityData;
• centralCover_candidateFrattiniLiftCoordinateData;
• centralCover_candidateFrattiniRealizationData;
• centralCover_candidateFrattiniCoordinateInverseData.

The two arbitrary-family semantic packets are stronger than the manuscript route needs. The route only needs one coherent scalar-pushout family and one coherent Frattini coordinate/realization pair. We therefore route through the strictly finer pointwise scalar-pushout and base/fibre Frattini packets isolated in CandidateScalarFrattiniActualClosers.lean, then export the same lift-partition target shape consumed by the integrated route.

Refined leaves still visible in the exported theorem's axiom closure:

• scalar point values, additivity, and homogeneity: centralCover_candidateMiddleScalarPushoutValueAtData, centralCover_candidateMiddleScalarPushoutAdditivityData, centralCover_candidateMiddleScalarPushoutHomogeneityData;
• Frattini base/fibre coordinate, fibre realization, and the two inverse laws: centralCover_candidateFrattiniBaseCoordinateData, centralCover_candidateFrattiniFiberCoordinateData, centralCover_candidateFrattiniFiberRealizationData, centralCover_candidateFrattiniRealizeLiftCoordinateData, centralCover_candidateFrattiniLiftCoordinateRealizeData.

Scalar-pushout bridge

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

Route12 scalar value packet from the pointwise scalar-pushout family.

This proves the value half of the old semantic packet through finer residuals, so its axiom closure does not name centralCover_candidateMiddleScalarPushoutValueData.

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutChosenLinearityData_from_route12SemanticProofs {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) × CentralCoverCandidateMiddleScalarPushoutLinearityData V.valueData)

Chosen scalar family with linearity for that same family.

This is the manuscript-shaped replacement for the arbitrary semantic linearity residual. It avoids the over-strong target centralCover_candidateMiddleScalarPushoutLinearityData D for an unrelated chosen D, while providing exactly what the route needs to assemble the middle obstruction evaluator.

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

Route12 scalar-obstruction evaluator assembled from the chosen pointwise scalar family and its linearity.

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

Middle R-lift obstruction map through the route12 scalar bridge.

Frattini coordinate bridge

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

Route12 Frattini lift-coordinate packet from base and fibre coordinates.

Its axiom closure does not name centralCover_candidateFrattiniLiftCoordinateData.

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

Route12 Frattini realization packet from the curried fibre realization.

Its axiom closure does not name centralCover_candidateFrattiniRealizationData.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniChosenInverseData_from_route12SemanticProofs {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) × CentralCoverCandidateFrattiniCoordinateInverseData (C.liftCoordinateData F) R.realizationData)

Chosen Frattini coordinate/realization pair with inverse laws.

This is the manuscript-shaped replacement for the arbitrary semantic inverse residual. It supplies inverse laws for the maps assembled from the same base/fibre coordinate and realization data.

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

Current Frattini affine-fibre coordinate packet assembled through the route12 base/fibre coordinate bridge.

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

Frattini exact-image partition through the route12 coordinate bridge.

Route-ready replacement

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

Direct exact-image residual data with the five route12 semantic residual names removed from the closure.

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

Route-ready candidate lift-partition provider for route12.

This has the same target shape as centralCover_candidateLiftPartitionData_from_scalarFrattiniCoherentProofs, but its closure refines away the five route12 semantic residual names listed in the module docstring.