Candidate exact-image packet closers

This sidecar splits the live candidate exact-image aggregate packet from CandidateExactImageResiduals.lean into the smaller manuscript-facing pieces:

• boundary-compatible postcomposition (lem:covertransform);
• a finite obstruction index and base map (def:Xgamma);
• the R-valued obstruction map (lem:obstructionseparation);
• the Frattini exact-image cardinality statement (prop:finalfourier).

The affine fibre torsor remains theorem-level through centralCover_candidateCanonicalAffineFiberTorsorData.

Strictly smaller candidate exact-image packets

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

Candidate boundary-compatible postcomposition packet.

This is the concrete lem:covertransform datum sending a top candidate boundary-framed exact-image map through the quotient Y -> B = Y/R, with the boundary-frame compatibility needed to land in the middle exact-image source.

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

Candidate finite obstruction index/base-map packet.

This isolates the finite exact-image index and its forgetful map to the middle candidate exact-image source before the R-valued obstruction map is chosen.

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

Candidate R-valued obstruction-map packet.

For a fixed finite obstruction index, this supplies only the obstruction map into B.obstructionSpace.

axiom Q2Presentation.Induction.centralCover_candidateFrattiniExactImageCardinalityData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (I : CentralCoverCandidateObstructionIndexBaseData B T) (O : CentralCoverCandidateObstructionMapData B T I) : let Odata := I.sourceObstructionData O; let A := centralCover_candidateCanonicalAffineFiberTorsorData B Odata; Nonempty (CentralCoverCandidateFrattiniExactImageCardinalityData B T Odata A.Z A.F)

Candidate Frattini exact-image cardinality packet.

For the obstruction datum assembled from a fixed index/base map and obstruction map, this is the finite cardinal statement whose choice-free content recovers the Frattini exact-image partition by liftPartition_of_cardinality.

Reassembly theorems

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

Reassemble the aggregate candidate exact-image residual from the strictly smaller concrete packets in this sidecar.

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

Short alias for the split-packet reassembly theorem.

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

Candidate semantic R-lift data routed through the split packet closers.

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

Coherent candidate lift-partition data routed through the split packet closers.