Actual candidate obstruction closers

This sidecar attacks the three semantic candidate residuals currently isolated in CandidateObstructionSemanticClosers.lean.

The file does not edit the routed integration files. It proves the current semantic residual conclusions from narrower manuscript-facing packets already present in the sidecar stack:

• actual quotient postcomposition is obtained from the quotient-frame commuting square for the concrete map T.topToMiddle : Y -> Y/R;
• the middle exact-image obstruction evaluation is obtained from the actual R-lift obstruction map on the canonical X_Gamma(B) index;
• the top affine-fibre/Frattini equivalence is obtained from the Frattini-cover exact-image equivalence for the canonical affine fibres.

Thus the theorem closures below avoid the three axioms named in CandidateObstructionSemanticClosers.lean; the remaining axioms are the smaller packets that still encode the manuscript's central-cover/lift-torsor semantics.

Actual top-to-middle postcomposition

def Q2Presentation.Induction.CentralCoverCandidateActualTopToMiddlePostcompData.ofQuotientFrameMap {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateQuotientFrameMapData B T) : CentralCoverCandidateActualTopToMiddlePostcompData B T

Build the actual postcomposition packet from the concrete quotient-frame commuting square. The map is still exactly T.topToMiddle; the extra datum is only that the boundary codomain square commutes with q_Y and beta.

Equations

• Q2Presentation.Induction.CentralCoverCandidateActualTopToMiddlePostcompData.ofQuotientFrameMap D = { boundary_compat := ⋯ }

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

The current actual postcomposition residual follows from the narrower quotient-frame commuting-square packet.

Actual R-lift obstruction on the middle exact-image index

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

Reinterpret the actual middle R-lift obstruction map as the evaluation packet used by the newer semantic residual.

Equations

• Q2Presentation.Induction.CentralCoverCandidateMiddleExactImageObstructionEvaluationData.ofMiddleRLiftObstructionMapData D = { obstruction := D.obstruction }

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

The current middle exact-image obstruction residual follows from the narrower R-lift obstruction map on the canonical middle exact-image index.

Actual affine-fibre/Frattini exact-image equivalence

def Q2Presentation.Induction.CentralCoverCandidateTopExactImageAffineFiberEquivData.ofFrattiniCoverData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T) (F : CentralCoverCandidateFrattiniCoverData B T D.obstructionEvaluationData) : CentralCoverCandidateTopExactImageAffineFiberEquivData B T D

Build the top affine-fibre equivalence from the Frattini-cover exact-image equivalence attached to the same canonical middle obstruction evaluation.

Equations

• Q2Presentation.Induction.CentralCoverCandidateTopExactImageAffineFiberEquivData.ofFrattiniCoverData D F = { frattiniEquiv := id F.equiv }

theorem Q2Presentation.Induction.centralCover_candidateTopExactImageAffineFiberEquivData_from_frattiniCover {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T) : Nonempty (CentralCoverCandidateTopExactImageAffineFiberEquivData B T D)

The current top exact-image affine-fibre residual follows from the narrower Frattini-cover exact-image equivalence for the canonical affine fibres.

Reassembly using only the narrower packets above

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

Candidate semantic R-lift data assembled without invoking the three semantic residual axioms from CandidateObstructionSemanticClosers.lean.

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

Coherent candidate lift-partition data routed through the actual-closer theorems in this sidecar.