Candidate component residual proofs

This sidecar strictly narrows the three current candidate Section 8 component residuals used by CandidateCanonicalConcreteProofs.lean.

The manuscript tower is the canonical exact-image tower

Y -> B = Y/R -> C = Y/K.

For the quotient-frame component, the canonical framed quotient construction already preserves the boundary codomain: the middle quotient has the same tame quotient H, the same decoration module E, and the same boundary frame beta. The quotient-frame map is therefore theorem-level for that explicit canonical construction.

For the source-side components, the middle R-obstruction and its Frattini exact-image affine-fibre equivalence are narrowed to one coherent packet. This avoids asking for a Frattini equivalence for an arbitrary independently chosen obstruction evaluation.

No routed file is edited here.

Closed quotient-frame map for the canonical framed quotient

def Q2Presentation.Induction.centralCover_candidateQuotientFrameMapData_of_decorationKernel {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationKernelData B D) (Card : CentralCoverTargetTowerCardinalityData B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D (TargetCanonicalFramedQuotientProofs.framedQuotientDataOfDecorationKernel B D H))) : CentralCoverCandidateQuotientFrameMapData B (elementaryQuotientTowerData_of_targetPackets B (targetSubgroupTowerData_of_concrete B D) (targetQuotientMapsData_of_framedQuotient B D (TargetCanonicalFramedQuotientProofs.framedQuotientDataOfDecorationKernel B D H)) Card)

The quotient-frame map is theorem-level for the explicit canonical framed quotient target constructed from the decoration-kernel packet.

The boundary codomain map is the identity because the canonical middle quotient target Y/R keeps the original H, E, and boundary frame.

Equations

• One or more equations did not get rendered due to their size.

Coherent middle-obstruction and Frattini source residual

structure Q2Presentation.Induction.CentralCoverCandidateMiddleFrattiniResidualProofData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Type

Coherent source-side component packet for the candidate final R-lift.

This is the narrowed replacement for the pair centralCover_candidateMiddleRLiftObstructionMapData_residual and centralCover_candidateFrattiniCoverData_residual: the Frattini equivalence is required only for the affine fibres attached to the selected middle obstruction map.

• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T
• frattiniEquiv : CentralCoverCandidateFrattiniExactImageEquivData B T self.middleObstruction.obstructionIndexToBaseMapData.O self.middleObstruction.affineFiberTorsorData.Z self.middleObstruction.affineFiberTorsorData.F

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

The remaining source-side candidate component residual, with the obstruction and matching Frattini exact-image equivalence chosen together.

def Q2Presentation.Induction.CentralCoverCandidateMiddleFrattiniResidualProofData.middleRLiftObstructionMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleFrattiniResidualProofData B T) : CentralCoverCandidateMiddleRLiftObstructionMapData B T

The coherent packet supplies the current middle obstruction map.

Equations

• D.middleRLiftObstructionMapData = D.middleObstruction

def Q2Presentation.Induction.CentralCoverCandidateMiddleFrattiniResidualProofData.frattiniCoverData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleFrattiniResidualProofData B T) : CentralCoverCandidateFrattiniCoverData B T (CentralCoverCandidateMiddleExactImageObstructionEvaluationData.ofMiddleRLiftObstructionMapData D.middleObstruction).obstructionEvaluationData

The coherent packet supplies the current Frattini cover data, but only for the selected obstruction evaluation.

Equations

• D.frattiniCoverData = { equiv := id D.frattiniEquiv }

def Q2Presentation.Induction.CentralCoverCandidateMiddleFrattiniResidualProofData.rLiftSemanticData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleFrattiniResidualProofData B T) (Q : CentralCoverCandidateQuotientFrameMapData B T) : CentralCoverCandidateRLiftSemanticData B T

Reassemble semantic R-lift data from the closed quotient-frame component and the coherent source-side residual.

Equations

• One or more equations did not get rendered due to their size.

def Q2Presentation.Induction.CentralCoverCandidateMiddleFrattiniResidualProofData.liftPartitionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleFrattiniResidualProofData B T) (Q : CentralCoverCandidateQuotientFrameMapData B T) : CentralCoverCandidateLiftPartitionData B

Reassemble lift-partition data from the closed quotient-frame component and the coherent source-side residual.

Equations

• One or more equations did not get rendered due to their size.

Route-ready reassembly from narrowed components

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

Canonical concrete proof data from the closed/narrowed component residuals.

The quotient-frame component is supplied explicitly; for the final route below it is supplied by centralCover_candidateQuotientFrameMapData_of_decorationKernel. The remaining axiom is the coherent middle-Frattini source packet.

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

Candidate lift-partition data from the closed/narrowed component residuals.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_componentResidualProofs_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 for the final nonterminal branch: for the block and canonical quotient tower built from the same Section 7 group tower, the quotient-frame component is closed and the candidate source side uses only the coherent middle-Frattini residual.