Candidate obstruction and Frattini closers

This sidecar continues the Section 8 candidate exact-image split from CandidateExactImageConcreteDataClosers.lean.

The old quotient-frame residual was an implication directly on boundary values. Here it is replaced by a more structural packet: the quotient Y -> B = Y/R must induce a map on the boundary codomains and commute with both the target map q_Y and the fixed boundary frame beta. This is the explicit quotient-frame compatibility suggested by the manuscript's quotient construction around lem:covertransform.

The remaining two packets are intentionally left as the semantic Section 8 content: the R-valued obstruction evaluation and the Frattini exact-image equivalence.

Quotient-frame map compatibility

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

Map-level quotient-frame compatibility for the candidate exact-image stage.

The middle quotient target can have boundary codomain written using its own H and E. Rather than requiring definitional equality with the top target's boundary codomain, this packet records the induced map between the two codomains and the two commutative squares needed by the boundary-frame equation.

• boundaryCodomainMap : p.fst.H × Multiplicative p.fst.E →* T.middleChild.fst.H × Multiplicative T.middleChild.fst.E
• qYMap_commutes (y : p.fst.Y) : self.boundaryCodomainMap (p.fst.qYMap y) = T.middleChild.fst.qYMap (T.topToMiddle y)
• beta_commutes (b : ↑Boundary.toProfinite.toTop) : self.boundaryCodomainMap ((ProfiniteGrp.Hom.hom p.snd.beta) b) = (ProfiniteGrp.Hom.hom T.middleChild.snd.beta) b

def Q2Presentation.Induction.candidateQuotientFrameCompatibilityData_of_frameMap {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateQuotientFrameMapData B T) : CentralCoverCandidateQuotientFrameCompatibilityData B T

A map-level quotient-frame packet supplies the implication-style packet used by the existing concrete candidate data closer.

Equations

• Q2Presentation.Induction.candidateQuotientFrameCompatibilityData_of_frameMap B T D = { postcompose_preserves_boundary := ⋯ }

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

Replacement residual: the quotient map induces the boundary-codomain map and commutes with q_Y and the fixed boundary frame.

This replaces centralCover_candidateQuotientFrameCompatibilityData_residual in the routed candidate exact-image closure.

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

Quotient-frame compatibility, proved from the map-level replacement packet rather than from the older implication-style residual.

Routed aggregate candidate data

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

Candidate concrete exact-image data routed through the map-level quotient frame packet, plus the existing semantic R-lift obstruction and Frattini cover packets.

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

Candidate exact-image residual data routed through the map-level quotient frame replacement.

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

Candidate semantic R-lift data routed through the map-level quotient-frame replacement.

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

Coherent candidate lift-partition data routed through the map-level quotient-frame replacement.