Candidate scalar/Frattini route19 proofs

Route19 is the exact-image obstruction/cardinality sidecar for the two broad packets left visible after Route18:

• centralCover_candidateObstructionMapData;
• centralCover_candidateFrattiniExactImageCardinalityData.

The obstruction-map packet is theorem-level in the supported broad form: an actual middle exact-image obstruction evaluation can be pulled back along any finite index-to-base map.

The Frattini cardinality packet is not available in its over-general I, O-arbitrary form. The manuscript-shaped statement is canonical: choose the middle exact-image index, the corresponding R-valued obstruction, and the matching affine-fibre equivalence. Route19 exposes that canonical cardinality and routes the supervisor-facing B T Q lift-partition provider through the same coherent residual.

Route19 exact-image obstruction/cardinality packets

theorem Q2Presentation.Induction.centralCover_candidateObstructionMapData_from_scalarFrattiniRoute19 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (I : CentralCoverCandidateObstructionIndexBaseData B T) : Nonempty (CentralCoverCandidateObstructionMapData B T I)

Route19 closes the broad obstruction-map packet by pulling the actual middle exact-image obstruction evaluation back along the supplied finite index-to-base map.

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

Route19's coherent final exact-image residual.

This is the manuscript-shaped pair: the middle exact-image obstruction evaluation and the matching top exact-image affine-fibre equivalence.

theorem Q2Presentation.Induction.centralCover_candidateCanonicalFrattiniExactImageCardinalityData_from_scalarFrattiniRoute19 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : ∃ (O : CentralCoverCandidateMiddleRLiftObstructionMapData B T), CentralCoverCandidateFrattiniExactImageCardinalityData B T O.obstructionIndexToBaseMapData.O O.affineFiberTorsorData.Z O.affineFiberTorsorData.F

Route19 canonical Frattini cardinality packet.

This is the supported Section 8 cardinality statement: there exists the canonical middle R-lift obstruction map whose affine fibres carry the Frattini exact-image cardinality. This deliberately does not assert the stronger arbitrary-I, O cardinality axiom.

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

Route19 canonical Frattini partition packet, keeping the selected obstruction map and exact-image partition together.

Route-ready reassembly

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

Route19 direct exact-image residual data assembled from the coherent final exact-image residual, without using the broad Frattini cardinality axiom.

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

Middle R-lift obstruction map selected by Route19's coherent exact-image residual.

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

Semantic central R-lift data from Route19 and a supplied quotient-frame map.

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

Route19 candidate lift-partition provider in the same supervisor-facing shape as Route18.

The quotient-frame argument is still supplied by the integrated route; Route19 only replaces the exact-image obstruction/cardinality side by the coherent canonical Section 8 residual.