Candidate Route114 semantic closers

This sidecar targets the two candidate Section 8 leaves exposed by Route114:

• centralCover_candidateMiddleScalarObstructionEvaluatorData;
• centralCover_candidateFrattiniAffineFiberCoordinateData.

There is no proof of these facts from already-closed Lean data in the current API. The useful lowering is to the coherent constructor shapes isolated in CandidateScalarFrattiniCurrentProofs:

• one selected scalar-pushout evaluator, with linearity for that same choice;
• one selected Frattini coordinate/realization tuple, with inverse laws for that same pair and the selected middle obstruction.

The route-ready provider below has the same call shape as the Route114 candidate provider, but its axiom closure contains those coherent constructor packets instead of the two Route114 semantic leaves.

Direct replacements for the two Route114 semantic leaves

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

Route114 middle scalar-obstruction evaluator, lowered to one coherent selected scalar-pushout evaluator.

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

Route114 Frattini affine-fibre coordinate data, lowered to one coherent selected coordinate/realization equivalence for the supplied obstruction.

Route-ready candidate provider

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

Middle R-lift obstruction map from the Route114 semantic lowering.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberPartition_from_route114SemanticClosers {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 from the Route114 semantic lowering.

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

Coherent direct exact-image residual data from the Route114 semantic lowering.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_route114SemanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Drop-in Route114 candidate provider with the candidate closure lowered to the coherent semantic constructors from CandidateScalarFrattiniCurrentProofs.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_route114SemanticAudit {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) : Nonempty ((_ : CentralCoverCandidateMiddleScalarPushoutCoherentData B D.tower) × (O : CentralCoverCandidateMiddleRLiftObstructionMapData B D.tower) × CentralCoverCandidateFrattiniCoordinateCoherentData B D.tower O × CentralCoverCandidateLiftPartitionData B)

Audit surface exposing the exact lower constructors used by the route-ready provider.