Canonical candidate obstruction concrete proofs

This sidecar keeps the candidate Section 8 obstruction data tied to the same canonical target quotient tower used by the target/proper-image route. It is intended as a route-ready replacement for the three live candidate residual axioms on an arbitrary elementary tower: quotient-frame compatibility, the middle R-lift obstruction map, and the Frattini cover equivalence.

The new residual below is indexed by D : CentralCoverTargetCanonicalQuotientTowerData B, so the middle source is the canonical exact-image source for D.tower, the top-to-middle map is the actual quotient-frame map of that tower, and the Frattini datum is an actual exact-image equivalence for the canonical affine fibres attached to the same middle obstruction.

Canonical candidate concrete packet

structure Q2Presentation.Induction.CentralCoverCandidateCanonicalConcreteProofData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Type

Candidate obstruction data for the canonical quotient tower D.tower.

This is deliberately not a packet for an arbitrary bare elementary tower. The three fields are the manuscript-facing objects for the canonical tower:

• quotient-frame commutation for the actual top-to-middle quotient map;
• the R-valued obstruction on the canonical middle exact-image source;
• the top exact-image/affine-fibre equivalence for the canonical affine fibres.

• quotientFrame : CentralCoverCandidateQuotientFrameMapData B D.tower
• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B D.tower
• frattiniEquiv : CentralCoverCandidateFrattiniExactImageEquivData B D.tower self.middleObstruction.obstructionIndexToBaseMapData.O self.middleObstruction.affineFiberTorsorData.Z self.middleObstruction.affineFiberTorsorData.F

axiom Q2Presentation.Induction.centralCover_candidateCanonicalConcreteProofData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverCandidateCanonicalConcreteProofData B D)

The remaining canonical candidate bridge for Section 8.

Unlike the older trio, this is tied to a supplied canonical target quotient tower. It therefore cannot be discharged by inventing data for an unrelated T; the middle exact-image source and the affine fibres are the canonical ones attached to D.tower.

def Q2Presentation.Induction.CentralCoverCandidateCanonicalConcreteProofData.middleEvaluationData {p : FramedPair} {B : MinimalBlock p} {D : CentralCoverTargetCanonicalQuotientTowerData B} (P : CentralCoverCandidateCanonicalConcreteProofData B D) : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B D.tower

The middle obstruction as the explicit obstruction-evaluation packet on the canonical middle exact-image index.

Equations

• P.middleEvaluationData = { obstruction := P.middleObstruction.obstruction }

def Q2Presentation.Induction.CentralCoverCandidateCanonicalConcreteProofData.actualPostcompData {p : FramedPair} {B : MinimalBlock p} {D : CentralCoverTargetCanonicalQuotientTowerData B} (P : CentralCoverCandidateCanonicalConcreteProofData B D) : CentralCoverCandidateActualTopToMiddlePostcompData B D.tower

The quotient-frame field gives actual top-to-middle postcomposition.

Equations

• P.actualPostcompData = Q2Presentation.Induction.CentralCoverCandidateActualTopToMiddlePostcompData.ofQuotientFrameMap P.quotientFrame

def Q2Presentation.Induction.CentralCoverCandidateCanonicalConcreteProofData.topExactImageAffineFiberEquivData {p : FramedPair} {B : MinimalBlock p} {D : CentralCoverTargetCanonicalQuotientTowerData B} (P : CentralCoverCandidateCanonicalConcreteProofData B D) : CentralCoverCandidateTopExactImageAffineFiberEquivData B D.tower P.middleEvaluationData

The Frattini equivalence repackaged as the semantic top exact-image affine-fibre equivalence.

Equations

• P.topExactImageAffineFiberEquivData = { frattiniEquiv := id P.frattiniEquiv }

def Q2Presentation.Induction.CentralCoverCandidateCanonicalConcreteProofData.frattiniCoverData {p : FramedPair} {B : MinimalBlock p} {D : CentralCoverTargetCanonicalQuotientTowerData B} (P : CentralCoverCandidateCanonicalConcreteProofData B D) : CentralCoverCandidateFrattiniCoverData B D.tower P.middleEvaluationData.obstructionEvaluationData

The same Frattini equivalence repackaged as the older cover-data wrapper, but only for the canonical obstruction evaluation coming from this packet.

Equations

• P.frattiniCoverData = { equiv := id P.frattiniEquiv }

def Q2Presentation.Induction.CentralCoverCandidateCanonicalConcreteProofData.rLiftSemanticData {p : FramedPair} {B : MinimalBlock p} {D : CentralCoverTargetCanonicalQuotientTowerData B} (P : CentralCoverCandidateCanonicalConcreteProofData B D) : CentralCoverCandidateRLiftSemanticData B D.tower

Assemble the semantic candidate R-lift packet directly from the canonical concrete proof packet.

Equations

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

def Q2Presentation.Induction.CentralCoverCandidateCanonicalConcreteProofData.liftPartitionData {p : FramedPair} {B : MinimalBlock p} {D : CentralCoverTargetCanonicalQuotientTowerData B} (P : CentralCoverCandidateCanonicalConcreteProofData B D) : CentralCoverCandidateLiftPartitionData B

Assemble the coherent candidate lift-partition packet directly from the canonical concrete proof packet.

Equations

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

Route-ready closures from the canonical packet

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

Canonical quotient-frame map data for the supplied canonical quotient tower.

theorem Q2Presentation.Induction.centralCover_candidateMiddleRLiftObstructionMapData_from_canonicalConcreteProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverCandidateMiddleRLiftObstructionMapData B D.tower)

Canonical middle R-lift obstruction map for the supplied canonical quotient tower.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniCoverData_from_canonicalConcreteProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty ((E : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B D.tower) × CentralCoverCandidateFrattiniCoverData B D.tower E.obstructionEvaluationData)

Canonical Frattini cover data for the obstruction evaluation supplied by the canonical middle R-lift map.

theorem Q2Presentation.Induction.centralCover_candidateRLiftSemanticData_from_canonicalConcreteProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverCandidateRLiftSemanticData B D.tower)

Candidate semantic R-lift data from canonical concrete proofs, avoiding the three older arbitrary-tower candidate residuals.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_canonicalConcreteProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Coherent candidate lift-partition data from canonical concrete proofs.

theorem Q2Presentation.Induction.centralCover_liftTorsorData_fine_from_canonicalConcreteProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverLiftTorsorData B)

Lift-torsor data with the candidate side routed through the supplied canonical quotient tower and canonical candidate concrete proof packet.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_canonicalConcreteProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CoverRealization B)

Cover realization from a supplied canonical quotient tower, with the candidate side routed through the canonical concrete proof packet.