Candidate scalar/Frattini coherent proof providers

This sidecar proves theorem-level providers for the two coherent route10 candidate residuals introduced in CandidateScalarFrattiniCurrentProofs.lean.

The routed file is not edited here. The route-ready theorem at the bottom has the same target shape as centralCover_candidateLiftPartitionData_from_scalarFrattiniCurrentProofs, but its proof uses the providers in this file, so its axiom closure does not name the two route10 coherent residual axioms:

• centralCover_candidateMiddleScalarPushoutCoherentData;
• centralCover_candidateFrattiniCoordinateCoherentData.

Coherent scalar-pushout provider

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

The coherent scalar-pushout evaluator packet follows by choosing the current scalar-pushout value packet and its linearity packet for that same choice.

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

Current scalar-obstruction evaluator assembled through the theorem-level coherent scalar provider, not the route10 coherent scalar axiom.

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

Middle R-lift obstruction map assembled through the theorem-level scalar coherent provider.

Coherent Frattini-coordinate provider

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

The coherent Frattini coordinate packet follows by choosing the current lift-coordinate map, realization map, and inverse laws for that same pair.

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

Current Frattini affine-fibre coordinate data assembled through the theorem-level coherent Frattini provider, not the route10 coherent Frattini axiom.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberPartition_from_coherentProofs {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 assembled through the theorem-level coherent Frattini provider.

Route-ready replacement

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

Direct exact-image residual data from the theorem-level coherent scalar and Frattini providers in this file.

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

Route-ready candidate lift-partition provider with the same target shape as the route10 current provider, but without the two route10 coherent residual axioms in its closure.