Canonical candidate obstruction decompositions

This sidecar works only over a supplied canonical target quotient tower D : CentralCoverTargetCanonicalQuotientTowerData B.

The current routed file CandidateObstructionConcreteProofs.lean packages the candidate side of manuscript Section 8 into one canonical residual, centralCover_candidateCanonicalConcreteProofData. The theorems below avoid that aggregate axiom in two ways:

• centralCover_candidateCanonicalConcreteProofData_from_componentPackets reassembles the exact canonical concrete structure from its three concrete component packets: quotient-frame map, middle R-lift obstruction, and Frattini exact-image equivalence.
• centralCover_candidateLiftPartitionData_from_canonicalSemanticClosers gives the route-ready candidate lift-partition packet directly from the manuscript-shaped semantic packets: actual top-to-middle postcomposition, middle exact-image obstruction evaluation, and top exact-image affine-fibre equivalence.

No theorem in this file calls centralCover_candidateCanonicalConcreteProofData.

Exact canonical aggregate from component packets

theorem Q2Presentation.Induction.centralCover_candidateCanonicalConcreteProofData_from_componentPackets {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverCandidateCanonicalConcreteProofData B D)

Reassemble the current canonical concrete packet from its three concrete Section 8 component packets.

This is an exact theorem-level replacement for the aggregate residual centralCover_candidateCanonicalConcreteProofData. Its axiom closure should name the three component residuals, not the aggregate residual.

Route-ready canonical semantic split

theorem Q2Presentation.Induction.centralCover_candidateRLiftSemanticData_from_canonicalSemanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverCandidateRLiftSemanticData B D.tower)

Candidate semantic R-lift data for a supplied canonical quotient tower, routed through the semantic Section 8 packets rather than through the aggregate canonical concrete residual.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_canonicalSemanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Coherent candidate lift-partition data for a supplied canonical quotient tower, assembled without the aggregate canonical concrete residual.

theorem Q2Presentation.Induction.centralCover_liftTorsorData_fine_from_canonicalSemanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverLiftTorsorData B)

Lift-torsor data for a supplied canonical quotient tower, with the candidate source routed through the semantic split above.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_canonicalSemanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CoverRealization B)

Cover realization from a supplied canonical quotient tower, where only the candidate side is changed: it uses the semantic candidate split rather than the canonical concrete aggregate residual.

Integrated route shape with the semantic candidate split

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCanonicalSemanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (R : MinimalBlockPreheadExtraspecialRadicalData F) : Nonempty (CoverRealization (G.toMinimalBlock h F A R))

The current integrated cover-realization route, but with the candidate side rerouted through centralCover_candidateLiftPartitionData_from_canonicalSemanticClosers instead of centralCover_candidateLiftPartitionData_from_canonicalConcreteProofs.

This keeps the existing target/proper-image actual route intact, so its axiom closure should not contain either the aggregate candidate residual centralCover_candidateCanonicalConcreteProofData or the old proper-image trio.