Canonical candidate obstruction semantic proofs #

This sidecar narrows the three live candidate-side Section 8 semantic residuals to the canonical quotient tower used by the current final route.

The existing residuals in CandidateObstructionSemanticClosers.lean are stated for an arbitrary T : CentralCoverElementaryQuotientTowerData B. The final route, however, builds such a tower from the canonical target tower D : CentralCoverTargetCanonicalQuotientTowerData B. The theorems below therefore give route-ready replacements over D.tower, and reassemble the semantic R-lift packet without calling

centralCover_candidateActualTopToMiddlePostcompData_residual,
centralCover_candidateMiddleExactImageObstructionEvaluationData_residual,
centralCover_candidateTopExactImageAffineFiberEquivData_residual.

The remaining assumptions are the strictly narrower component packets already isolated in the sidecar stack: the actual quotient-frame commuting square, the middle R-lift obstruction map, and the Frattini exact-image equivalence for the selected canonical affine fibres.

Canonical-tower forms of the three semantic residuals #

source

theorem Q2Presentation.Induction.centralCover_candidateActualTopToMiddlePostcompData_from_canonicalQuotientFrameMap {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) :

Nonempty (CentralCoverCandidateActualTopToMiddlePostcompData B D.tower)

Canonical-tower replacement for centralCover_candidateActualTopToMiddlePostcompData_residual.

The tower is not arbitrary: it is the D.tower attached to a supplied canonical target quotient tower. The proof uses the map-level quotient-frame packet, so the quotient map is still the actual Y -> B = Y/R map carried by D.tower.

source

theorem Q2Presentation.Induction.centralCover_candidateMiddleExactImageObstructionEvaluationData_from_canonicalMiddleRLiftMap {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) :

Nonempty (CentralCoverCandidateMiddleExactImageObstructionEvaluationData B D.tower)

Canonical-tower replacement for centralCover_candidateMiddleExactImageObstructionEvaluationData_residual.

The exact-image source is the canonical middle source for D.tower, matching the manuscript's X_Gamma(B) object.

source

theorem Q2Presentation.Induction.centralCover_candidateTopExactImageAffineFiberEquivData_from_canonicalFrattiniCover {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (E : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B D.tower) :

Nonempty (CentralCoverCandidateTopExactImageAffineFiberEquivData B D.tower E)

Canonical-tower replacement for centralCover_candidateTopExactImageAffineFiberEquivData_residual.

For any middle obstruction evaluation over the canonical tower, this reduces the requested top affine-fibre equivalence to the narrower Frattini-cover exact-image packet for that same evaluation.

Combined canonical semantic packet #

source

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

Type

The three candidate semantic objects, tied to the actual canonical target quotient tower.

This is the canonical-tower analogue of the three arbitrary-tower residuals in CandidateObstructionSemanticClosers.lean, with the dependency between the middle obstruction evaluation and the top affine-fibre equivalence made explicit.

actualPostcomp : CentralCoverCandidateActualTopToMiddlePostcompData B D.tower
middleEvaluation : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B D.tower
topAffineFiberEquiv : CentralCoverCandidateTopExactImageAffineFiberEquivData B D.tower self.middleEvaluation

Instances For

source

def Q2Presentation.Induction.CentralCoverCandidateCanonicalSemanticResidualData.rLiftSemanticData {p : FramedPair} {B : MinimalBlock p} {D : CentralCoverTargetCanonicalQuotientTowerData B} (S : CentralCoverCandidateCanonicalSemanticResidualData B D) :

CentralCoverCandidateRLiftSemanticData B D.tower

Reassemble the semantic R-lift packet from the canonical semantic data.

Equations

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

Instances For

source

def Q2Presentation.Induction.CentralCoverCandidateCanonicalSemanticResidualData.liftPartitionData {p : FramedPair} {B : MinimalBlock p} {D : CentralCoverTargetCanonicalQuotientTowerData B} (S : CentralCoverCandidateCanonicalSemanticResidualData B D) :

CentralCoverCandidateLiftPartitionData B

Reassemble the candidate lift partition from the canonical semantic data.

Equations

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

Instances For

source

theorem Q2Presentation.Induction.centralCover_candidateCanonicalSemanticResidualData_from_componentPackets {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) :

Nonempty (CentralCoverCandidateCanonicalSemanticResidualData B D)

Canonical semantic candidate data from the three narrower component packets.

This is the main sidecar decomposition: its axiom closure contains the quotient-frame map, middle obstruction map, and Frattini-cover packets for D.tower, rather than the three arbitrary-tower semantic residuals.

source

theorem Q2Presentation.Induction.centralCover_candidateCanonicalSemanticResidualData_from_canonicalConcreteProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) :

Nonempty (CentralCoverCandidateCanonicalSemanticResidualData B D)

The same canonical semantic packet, obtained from the existing canonical concrete packet. This theorem is useful for comparing the aggregate canonical residual with the split component-packet route above.

source