Candidate obstruction semantic closers

This sidecar narrows the current Section 8 candidate residuals to the actual semantic objects used by the final route:

• quotient-frame data is the real postcomposition by the tower map T.topToMiddle : Y -> B = Y/R; the only residual field is boundary preservation for that postcomposition;
• the R-lift obstruction is an evaluation on the canonical middle exact-image source X_Gamma(B) from def:Xgamma;
• the Frattini packet is an explicit top exact-image equivalence for the canonical affine fibres, not merely an anonymous partition datum.

No theorem below calls the older residuals centralCover_candidateQuotientFrameMapData_residual, centralCover_candidateMiddleRLiftObstructionMapData_residual, or centralCover_candidateFrattiniAffineFiberPartition_residual.

Actual top-to-middle postcomposition

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

Boundary preservation for the actual quotient postcomposition T.topToMiddle : Y -> B = Y/R.

The profinite morphism and its surjectivity are already theorem-level from CentralCoverElementaryQuotientTowerData; the residual content is only that a top boundary-framed candidate map remains boundary-framed after postcomposition to the middle target.

• boundary_compat (f : centralCoverCandidateSource) (γ : ↑GammaA.toProfinite.toTop) : T.middleChild.fst.qYMap (T.topToMiddle ((ProfiniteGrp.Hom.hom (↑f).hom) γ)) = (ProfiniteGrp.Hom.hom T.middleChild.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) γ)

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

Reassemble the postcomposition packet with the actual finite quotient map stored in the elementary tower.

Equations

• D.boundaryPostcompData = { topToMiddleHom := Q2Presentation.Induction.centralCover_candidateFiniteQuotientPostcompHom B T, topToMiddle_surj := ⋯, topToMiddle_agrees := ⋯, boundary_compat := ⋯ }

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

The exact-image base quotient induced by actual top-to-middle postcomposition.

Equations

• D.exactImageBaseQuotient = D.boundaryPostcompData.exactImageBaseQuotient

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

Semantic replacement residual for centralCover_candidateQuotientFrameMapData_residual.

The quotient map is no longer residual data: it is the actual T.topToMiddle. Only boundary-frame preservation for that map remains.

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

Exact-image base quotient from actual top-to-middle postcomposition.

Obstruction on the canonical middle exact-image index

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

The actual candidate R-lift obstruction evaluation on the canonical middle exact-image source.

• obstruction : centralCoverCandidateMiddleSource T → B.obstructionSpace

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

Repackage as the existing middle obstruction-map structure.

Equations

• D.middleRLiftObstructionMapData = { obstruction := D.obstruction }

def Q2Presentation.Induction.CentralCoverCandidateMiddleExactImageObstructionEvaluationData.obstructionEvaluationData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T) : CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)

Repackage as an explicit obstruction evaluation over the concrete middle exact-image index.

Equations

• D.obstructionEvaluationData = { obstruction := D.obstruction }

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

Semantic replacement residual for centralCover_candidateMiddleRLiftObstructionMapData_residual.

The index is fixed to the actual middle exact-image source; this residual is only the obstruction evaluation on that index.

Top exact-image affine-fibre equivalence

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

Explicit Frattini exact-image equivalence for the canonical affine fibres attached to a middle exact-image obstruction evaluation.

• frattiniEquiv : CentralCoverCandidateFrattiniExactImageEquivData B T D.middleRLiftObstructionMapData.obstructionIndexToBaseMapData.O D.middleRLiftObstructionMapData.affineFiberTorsorData.Z D.middleRLiftObstructionMapData.affineFiberTorsorData.F

def Q2Presentation.Induction.CentralCoverCandidateTopExactImageAffineFiberEquivData.frattiniExactImage {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T} (E : CentralCoverCandidateTopExactImageAffineFiberEquivData B T D) : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.middleRLiftObstructionMapData.obstructionIndexToBaseMapData.O D.middleRLiftObstructionMapData.affineFiberTorsorData.Z D.middleRLiftObstructionMapData.affineFiberTorsorData.F

The existing Frattini surjectivity/partition packet obtained from the explicit top exact-image equivalence.

Equations

• E.frattiniExactImage = E.frattiniEquiv.frattiniExactImage

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

Semantic replacement residual for centralCover_candidateFrattiniAffineFiberPartition_residual.

For the chosen middle obstruction evaluation, this supplies an actual equivalence between top candidate exact-image maps and the dependent sum of unobstructed canonical affine fibres.

Reassembly for the final route

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

Candidate semantic R-lift data assembled from the three semantic packets above.

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

Coherent candidate lift-partition data routed through the semantic packets.