Candidate exact-image concrete data closers

This owned sidecar refines the aggregate residual centralCover_candidateConcreteExactImageData from CandidateExactImageConcreteClosers.lean.

The paper-side content is split along Section 8 and the Pro validation note:

• quotient-frame compatibility for postcomposition (lem:covertransform);
• semantic R-lift obstruction data on the exact-image middle index (def:Xgamma, lem:obstructionseparation);
• Frattini-cover exact-image data for the canonical affine fibres (prop:finalfourier).

No theorem below uses the aggregate axiom centralCover_candidateConcreteExactImageData.

Quotient-frame compatibility

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

Boundary-frame compatibility for the quotient map Y -> B = Y/R.

For an arbitrary bare T : CentralCoverElementaryQuotientTowerData B, the top and middle targets do not expose definitionally identical boundary codomains. This type-safe formulation records exactly what Section 8 needs: any top boundary equation is preserved after quotient postcomposition to the middle frame.

• postcompose_preserves_boundary {y : p.fst.Y} {b : ↑Boundary.toProfinite.toTop} : p.fst.qYMap y = (ProfiniteGrp.Hom.hom p.snd.beta) b → T.middleChild.fst.qYMap (T.topToMiddle y) = (ProfiniteGrp.Hom.hom T.middleChild.snd.beta) b

theorem Q2Presentation.Induction.centralCover_candidateBoundaryCompatibilityData_from_quotientFrame {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateQuotientFrameCompatibilityData B T) : CentralCoverCandidateBoundaryCompatibilityData B T

The quotient-frame packet implies the boundary-compatibility structure used by CandidateExactImageConcreteClosers.lean.

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

Residual quotient-frame compatibility for the candidate source.

Semantic R-lift obstruction data

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

Semantic R-lift obstruction data on the concrete middle exact-image index.

The current API has the finite exact-image index centralCover_candidateMiddleExactImageIndexBaseData; the missing paper content is the actual obstruction evaluation associated to the central R-cover.

• evaluation : CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)

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

Residual semantic R-lift obstruction data.

theorem Q2Presentation.Induction.centralCover_candidateObstructionEvaluationData_from_RLiftObstruction {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T))

The semantic R-lift obstruction packet supplies the concrete obstruction-evaluation packet.

Frattini-cover exact-image data

structure Q2Presentation.Induction.CentralCoverCandidateFrattiniCoverData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (E : CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)) : Type

Frattini-cover exact-image data for a fixed semantic obstruction evaluation.

This is the remaining R = Phi(K) content of prop:finalfourier: the canonical affine fibres are identified with the top exact-image candidate maps.

• equiv : CentralCoverCandidateFrattiniExactImageEquivData B T (centralCover_candidateMiddleObstructionData B T E) (centralCover_candidateMiddleAffineFiberTorsorData B T E).Z (centralCover_candidateMiddleAffineFiberTorsorData B T E).F

axiom Q2Presentation.Induction.centralCover_candidateFrattiniCoverData_residual {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (E : CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)) : Nonempty (CentralCoverCandidateFrattiniCoverData B T E)

Residual Frattini-cover exact-image data for the canonical affine lift fibres attached to a fixed semantic obstruction evaluation.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniExactImageEquivData_from_frattiniCover {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (E : CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)) : Nonempty (CentralCoverCandidateFrattiniExactImageEquivData B T (centralCover_candidateMiddleObstructionData B T E) (centralCover_candidateMiddleAffineFiberTorsorData B T E).Z (centralCover_candidateMiddleAffineFiberTorsorData B T E).F)

The Frattini-cover packet supplies the Frattini exact-image equivalence.

Aggregate reassembly without the old aggregate axiom

theorem Q2Presentation.Induction.centralCover_candidateConcreteExactImageData_from_splitPackets {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (boundary : CentralCoverCandidateBoundaryCompatibilityData B T) (evaluation : CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)) (frattini : CentralCoverCandidateFrattiniExactImageEquivData B T (centralCover_candidateMiddleObstructionData B T evaluation) (centralCover_candidateMiddleAffineFiberTorsorData B T evaluation).Z (centralCover_candidateMiddleAffineFiberTorsorData B T evaluation).F) : Nonempty (CentralCoverCandidateConcreteExactImageData B T)

Reassemble the aggregate concrete candidate exact-image packet from the three smaller concrete packets.

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

The aggregate concrete candidate exact-image packet, proved from the smaller concrete residual packets rather than from centralCover_candidateConcreteExactImageData.

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

Candidate exact-image residual data routed through the split concrete packets.

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

Candidate semantic R-lift data routed through the split concrete packets.

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

Coherent candidate lift-partition data routed through the split concrete packets.