Final candidate exact-image closers

This sidecar targets the two broad candidate Section 8 packet axioms still visible in the current final closure:

• centralCover_candidateObstructionMapData;
• centralCover_candidateFrattiniExactImageCardinalityData.

The obstruction-map packet is harmless once the actual middle exact-image obstruction evaluation is available: any supplied finite obstruction index maps to the middle exact-image source, so the obstruction is pulled back along that map.

The Frattini cardinality packet is too strong for an arbitrary index. The manuscript statement is canonical: it uses the middle exact-image index X_Gamma(C) and the affine fibres attached to that same obstruction. We therefore close the canonical instance from the exact-image affine-fibre equivalence and route the candidate lift-partition theorem through that canonical instance.

Coherent final residual

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

Coherent final candidate exact-image data for a fixed elementary quotient tower.

The obstruction evaluation and the Frattini affine-fibre equivalence are chosen together, so the equivalence is attached to the same obstruction used in the canonical affine fibres.

• middleEvaluation : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T
• frattiniEquiv : CentralCoverCandidateTopExactImageAffineFiberEquivData B T self.middleEvaluation

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

The middle R-lift obstruction map selected by the residual.

Equations

• D.middleRLiftObstructionMapData = D.middleEvaluation.middleRLiftObstructionMapData

def Q2Presentation.Induction.CentralCoverCandidateExactImageFinalResidualData.obstructionMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateExactImageFinalResidualData B T) (I : CentralCoverCandidateObstructionIndexBaseData B T) : CentralCoverCandidateObstructionMapData B T I

Pull the actual middle obstruction evaluation back along an arbitrary finite obstruction index. This closes the broad obstruction-map packet without inventing a source-independent dummy obstruction.

Equations

• D.obstructionMapData I = { obstruction := fun (x : I.X) => D.middleEvaluation.obstruction (I.indexToBase x) }

def Q2Presentation.Induction.CentralCoverCandidateExactImageFinalResidualData.canonicalFrattiniCardinalityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateExactImageFinalResidualData B T) : CentralCoverCandidateFrattiniExactImageCardinalityData B T D.middleRLiftObstructionMapData.obstructionIndexToBaseMapData.O D.middleRLiftObstructionMapData.affineFiberTorsorData.Z D.middleRLiftObstructionMapData.affineFiberTorsorData.F

The canonical Frattini cardinality packet carried by the affine-fibre equivalence.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.CentralCoverCandidateExactImageFinalResidualData.canonicalFrattiniExactImage {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateExactImageFinalResidualData B T) : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.middleRLiftObstructionMapData.obstructionIndexToBaseMapData.O D.middleRLiftObstructionMapData.affineFiberTorsorData.Z D.middleRLiftObstructionMapData.affineFiberTorsorData.F

The canonical Frattini exact-image partition carried by the affine-fibre equivalence.

Equations

• D.canonicalFrattiniExactImage = D.frattiniEquiv.frattiniExactImage

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

Reassemble semantic R-lift data from the final residual and a supplied exact-image base quotient.

Equations

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

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

Reassemble candidate lift-partition data from the final residual and a supplied quotient-frame map.

Equations

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

Closers for the two broad packets

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

The final residual follows from the existing semantic Section 8 packets.

theorem Q2Presentation.Induction.centralCover_candidateObstructionMapData_from_finalClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (I : CentralCoverCandidateObstructionIndexBaseData B T) : Nonempty (CentralCoverCandidateObstructionMapData B T I)

The broad obstruction-map packet is derivable by pulling back the actual middle exact-image obstruction evaluation along the supplied index-to-base map.

theorem Q2Presentation.Induction.centralCover_candidateCanonicalFrattiniExactImageCardinalityData_from_finalClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : ∃ (O : CentralCoverCandidateMiddleRLiftObstructionMapData B T), CentralCoverCandidateFrattiniExactImageCardinalityData B T O.obstructionIndexToBaseMapData.O O.affineFiberTorsorData.Z O.affineFiberTorsorData.F

Canonical instance of the Frattini cardinality packet, closed from the actual top exact-image affine-fibre equivalence.

This is the manuscript-shaped instance used by the final route. The arbitrary I, O form of centralCover_candidateFrattiniExactImageCardinalityData is stronger than the available Section 8 semantics and is intentionally not reproved here.

Route-ready reassembly

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

Candidate semantic R-lift data routed through the final closers, avoiding the two broad packet axioms targeted by this sidecar.

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

Candidate lift-partition data routed through the final closers and a supplied quotient-frame map. This matches the candidate-side call shape in the current integrated route.