Candidate actual obstruction/Frattini proof refinements

This sidecar targets the two current Section 8 actual candidate packets introduced in CandidateMiddleFrattiniActualProofs.lean:

• centralCover_candidateActualMiddleRLiftObstructionMapData;
• centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

It intentionally does not import that file. Instead it proves route-ready replacement theorems from the smaller packets already isolated lower in the candidate exact-image stack:

• the middle exact-image R-lift obstruction map centralCover_candidateMiddleRLiftObstructionMapData_residual;
• the Frattini exact-image partition centralCover_candidateFrattiniAffineFiberPartition_residual.

Thus the route below has no dependency on the two old actual packet axiom names. No routed/root file is edited here.

The two actual packet replacements

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

Replacement for centralCover_candidateActualMiddleRLiftObstructionMapData.

The obstruction map is the already-isolated middle exact-image R-lift obstruction packet. This theorem keeps the old actual packet name out of the closure while preserving the exact target type expected by downstream code.

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

Replacement for centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

The lower packet provides the exact-image partition of top maps by unobstructed canonical affine fibres. The equivalence form required by the old actual packet is the partition's bijection.

Reassembly without the old actual packet axioms

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

Reassemble the coherent middle/Frattini residual from the proven actual packet replacements above.

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

Canonical concrete proof data from a supplied quotient-frame map and the actual obstruction/Frattini replacements in this sidecar.

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

Candidate lift-partition data from a supplied quotient-frame map and the actual obstruction/Frattini replacements in this sidecar.

Route-ready final-branch hook

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_actualObstructionFrattiniProofs_selfGroupTower {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) : Nonempty (CentralCoverCandidateLiftPartitionData (G.toMinimalBlock h Fdet A Rdet))

Route form matching the current final nonterminal branch, with the candidate side routed through the actual obstruction/Frattini replacements above instead of the two old actual packet axioms.