Candidate middle/Frattini actual proof split

This sidecar targets the current final-closure candidate Section 8 packet centralCover_candidateMiddleFrattiniResidualProofData.

The current packet is already coherent: it chooses the middle R-lift obstruction map and the matching Frattini affine-fibre exact-image equivalence together. The split below exposes the two manuscript-shaped facts separately:

• the actual R-valued obstruction on the middle exact-image source (lem:obstructionseparation, lem:affinelifting);
• the actual Frattini affine-fibre exact-image equivalence for the selected obstruction (prop:finalfourier, using R = Phi(K)).

No theorem below calls centralCover_candidateMiddleFrattiniResidualProofData, and no routed file is edited here.

Split actual candidate-source inputs

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

Actual middle R-lift obstruction input.

This is the candidate-source obstruction evaluation on the canonical middle exact-image source for the realized elementary tower. It is one field of the previous coherent packet, exposed as its own residual.

axiom Q2Presentation.Induction.centralCover_candidateActualFrattiniAffineFiberExactImageEquivData {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)

Actual Frattini affine-fibre exact-image input.

For the selected middle obstruction map, this supplies the exact-image equivalence between top candidate maps and unobstructed canonical affine R-lift fibres. This is the Frattini half of the previous coherent packet, but it is dependent on the chosen obstruction rather than independently quantified over an arbitrary obstruction evaluation.

The fused coherent middle/Frattini residual (checkpoint-F5)

The two split axioms above are kept for the legacy audit surface, but the split was UNSOUND as a pair of residuals: the Frattini half is property-form over an arbitrary opaque obstruction packet O, hence falsifiable at junk O (e.g. an obstruction map with empty unobstructed fibre set while top candidate maps exist) — the same over-strong shape as the corrected §7 kernel findings in PROGRESS.md. The live route below therefore consumes ONE existence-form coherent residual: the manuscript chooses the obstruction map and proves the affine-fibre exact-image equivalence FOR THAT choice in one construction (lem:obstructionseparation + lem:affinelifting + prop:finalfourier).

axiom Q2Presentation.Induction.centralCover_candidateActualMiddleFrattiniCoherentData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((O : CentralCoverCandidateMiddleRLiftObstructionMapData B T) ×' CentralCoverCandidateFrattiniExactImageEquivData B T O.obstructionIndexToBaseMapData.O O.affineFiberTorsorData.Z O.affineFiberTorsorData.F)

Fused actual middle/Frattini residual (existence-form). The candidate R-lift obstruction packet together with the Frattini affine-fibre exact-image equivalence for that same packet, as one same-construction datum.

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

Reassemble the current middle/Frattini packet from the fused coherent residual (checkpoint-F5; formerly from the two split axioms above, which are no longer consumed by the live route).

theorem Q2Presentation.Induction.centralCover_candidateCanonicalConcreteProofData_from_middleFrattiniActualProofs {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 split actual middle/Frattini inputs.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_middleFrattiniActualProofs {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 split actual middle/Frattini inputs.

Route-ready hook for the current final nonterminal branch

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_middleFrattiniActualProofs_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, but with the candidate source side routed through the two split actual middle/Frattini inputs rather than through centralCover_candidateMiddleFrattiniResidualProofData.

To route this sidecar, import it where the current final route is assembled and replace the call to centralCover_candidateLiftPartitionData_from_componentResidualProofs_selfGroupTower by this theorem.