Candidate lift-partition cardinality refinements

Sidecar for the Section 8 candidate lift-partition residual in CentralCoverFineResiduals.lean.

theorem Q2Presentation.Induction.liftPartitionCardinality_of_liftPartition {p : FramedPair} (B : MinimalBlock p) (S : Type) (O : CentralCoverSourceObstructionData B S) (Z : CentralCoverSourceCocycleData B) (F : CentralCoverSourceLiftFibers B S O Z) (P : CentralCoverSourceLiftPartition B S O Z F) : CentralCoverSourceLiftPartitionCardinality B S O Z F

The cardinality shadow of an actual exact-image lift partition.

This is the provable direction of lem:covertransform / prop:finalfourier at the level currently exposed by CentralCoverFineResiduals: once the manuscript has supplied the genuine bijection from boundary-framed surjections to the dependent sum of unobstructed lift fibres, the cardinal equality is immediate.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionCardinality_of_liftPartition {p : FramedPair} (B : MinimalBlock p) (O : CentralCoverSourceObstructionData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd)) (Z : CentralCoverSourceCocycleData B) (F : CentralCoverSourceLiftFibers B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) O Z) (P : CentralCoverSourceLiftPartition B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) O Z F) : Nonempty (CentralCoverSourceLiftPartitionCardinality B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) O Z F)

Candidate specialization of liftPartitionCardinality_of_liftPartition.

This is intentionally conditional on a genuine partition for the same O/Z/F; it is not the overbroad residual that quantified over arbitrary obstruction and fibre data.

structure Q2Presentation.Induction.CentralCoverCandidateLiftPartitionData {p : FramedPair} (B : MinimalBlock p) : Type 1

The manuscript-faithful candidate packet: the obstruction data, cocycle data, lift fibres, and exact-image lift partition are chosen coherently.

This is the narrower residual shape that matches Section 8. The old centralCover_candidateLiftPartitionCardinality is stronger in the wrong way: it asserts the same cardinality for every separately chosen O, Z, and F.

• O : CentralCoverSourceObstructionData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd)
• Z : CentralCoverSourceCocycleData B
• F : CentralCoverSourceLiftFibers B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) self.O self.Z
• partition : CentralCoverSourceLiftPartition B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) self.O self.Z self.F

def Q2Presentation.Induction.CentralCoverCandidateLiftPartitionData.cardinality {p : FramedPair} {B : MinimalBlock p} (D : CentralCoverCandidateLiftPartitionData B) : CentralCoverSourceLiftPartitionCardinality B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) D.O D.Z D.F

The cardinality form follows from the coherent candidate partition.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.CentralCoverCandidateLiftPartitionData.fiberData {p : FramedPair} {B : MinimalBlock p} (D : CentralCoverCandidateLiftPartitionData B) : CentralCoverSourceFiberData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) D.O D.Z

Repackage a coherent candidate partition as the fibre-data interface used by CentralCoverFineResiduals.

Equations

• D.fiberData = Q2Presentation.Induction.fiberData_of_fibersPartition B (Q2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA p.fst p.snd) D.O D.Z D.F D.partition

def Q2Presentation.Induction.CentralCoverCandidateLiftPartitionData.sourceLiftData {p : FramedPair} {B : MinimalBlock p} (D : CentralCoverCandidateLiftPartitionData B) : CentralCoverSourceLiftData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd)

Repackage a coherent candidate partition as the older source-lift interface.

This is the integration path: replace the overbroad arbitrary-cardinality residual by a single nonempty coherent packet of this structure, then assemble the candidate source lift data from it.

Equations

• D.sourceLiftData = Q2Presentation.Induction.sourceLiftData_of_fine B (Q2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA p.fst p.snd) D.O D.Z D.fiberData

theorem Q2Presentation.Induction.centralCover_candidateLiftData_fine_of_liftPartitionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverCandidateLiftPartitionData B) : Nonempty (CentralCoverSourceLiftData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd))

Conditional integration theorem for the coherent candidate packet.

theorem Q2Presentation.Induction.centralCover_candidateLiftData_fine_of_liftPartitionData_nonempty {p : FramedPair} (B : MinimalBlock p) (hD : Nonempty (CentralCoverCandidateLiftPartitionData B)) : Nonempty (CentralCoverSourceLiftData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd))

Nonempty coherent candidate lift-partition data is sufficient for the candidate source-lift packet used downstream.

Semantic candidate construction pieces

@[reducible, inline]

abbrev Q2Presentation.Induction.centralCoverCandidateSource {p : FramedPair} : Type

Candidate source set for the fixed boundary-framed target.

Equations

• Q2Presentation.Induction.centralCoverCandidateSource = Q2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA p.fst p.snd

@[reducible, inline]

abbrev Q2Presentation.Induction.centralCoverCandidateMiddleSource {p : FramedPair} {B : MinimalBlock p} (T : CentralCoverElementaryQuotientTowerData B) : Type

Candidate source set for the middle quotient B = Y/R in a realized tower.

Equations

• Q2Presentation.Induction.centralCoverCandidateMiddleSource T = Q2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA T.middleChild.fst T.middleChild.snd

def Q2Presentation.Induction.centralCover_candidateCanonicalCocycleData {p : FramedPair} (B : MinimalBlock p) : CentralCoverSourceCocycleData B

Canonical candidate cocycle data: the concrete group from CentralCoverFineResiduals together with its proved cardinality.

Equations

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

def Q2Presentation.Induction.centralCover_candidateRegularLiftFibers {p : FramedPair} (B : MinimalBlock p) (O : CentralCoverSourceObstructionData B centralCoverCandidateSource) (Z : CentralCoverSourceCocycleData B) : CentralCoverSourceLiftFibers B centralCoverCandidateSource O Z

Regular candidate lift fibres over any obstruction datum, using a chosen Z^1 group as the acting torsor.

Equations

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

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

Exact-image base quotient packet.

This is the candidate-side map that quotients a top exact-image map to the middle target B = Y/R in the realized tower. It is not currently derivable from CentralCoverElementaryQuotientTowerData, because that tower contains the quotient homomorphism of finite targets but not the boundary-frame compatibility proofs needed to build a boundaryFramedSurj.

• baseOfTop : centralCoverCandidateSource → centralCoverCandidateMiddleSource T

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

Obstruction-index-to-base packet.

The obstruction index is the manuscript exact-image base index X_Gamma(B), equipped with the R-valued obstruction map and its forgetful map to the middle exact-image source set.

• O : CentralCoverSourceObstructionData B centralCoverCandidateSource
• indexToBase : { x : self.O.X // self.O.o x = 0 } → centralCoverCandidateMiddleSource T

structure Q2Presentation.Induction.CentralCoverCandidateAffineFiberTorsorData {p : FramedPair} (B : MinimalBlock p) (O : CentralCoverSourceObstructionData B centralCoverCandidateSource) : Type 1

Affine fibre torsor packet.

This is the theorem-level part of lem:affinelifting: after the obstruction datum is fixed, the candidate lift fibres are the regular torsors under the canonical candidate Z^1(R) group, and each fibre has the common cardinality z_R.

• Z : CentralCoverSourceCocycleData B
• F : CentralCoverSourceLiftFibers B centralCoverCandidateSource O self.Z
• fiber_card (x : { x : O.X // O.o x = 0 }) : Nat.card (self.F.Lift x) = B.zR

def Q2Presentation.Induction.centralCover_candidateCanonicalAffineFiberTorsorData {p : FramedPair} (B : MinimalBlock p) (O : CentralCoverSourceObstructionData B centralCoverCandidateSource) : CentralCoverCandidateAffineFiberTorsorData B O

The canonical candidate affine fibre torsor, built from the already-proved candidate cocycle cardinality.

Equations

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

theorem Q2Presentation.Induction.centralCover_candidateAffineFiberTorsorData {p : FramedPair} (B : MinimalBlock p) (O : CentralCoverSourceObstructionData B centralCoverCandidateSource) : Nonempty (CentralCoverCandidateAffineFiberTorsorData B O)

The affine fibre torsor packet is theorem-level for the candidate source.

structure Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (O : CentralCoverSourceObstructionData B centralCoverCandidateSource) (Z : CentralCoverSourceCocycleData B) (F : CentralCoverSourceLiftFibers B centralCoverCandidateSource O Z) : Type

Frattini exact-image surjectivity packet.

This is the remaining exact-image content of prop:finalfourier: the unobstructed affine lift fibres partition the top exact-image maps, and the Frattini identity R = Phi(K) makes every unobstructed final R-lift surjective onto the top target.

• partition : CentralCoverSourceLiftPartition B centralCoverCandidateSource O Z F

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

Semantic candidate-side final R-lift packet.

The exact-image partition used by the recursion is not merely an abstract cardinality equivalence. In the manuscript it comes from the central R = Phi(K) cover over the realized quotient tower Y -> B = Y/R -> C = Y/K, the obstruction map of lem:covertransform, the affine lift equation of lem:affinelifting, and the Frattini-surjectivity argument in prop:finalfourier.

The packet is now split into the four manuscript-facing pieces above: exact-image base quotient, obstruction-index-to-base map, affine fibre torsor, and Frattini exact-image surjectivity.

• exactImageBaseQuotient : CentralCoverCandidateExactImageBaseQuotientData B T
• obstructionIndexToBase : CentralCoverCandidateObstructionIndexToBaseMapData B T
• affineFiberTorsor : CentralCoverCandidateAffineFiberTorsorData B self.obstructionIndexToBase.O
• frattiniExactImage : CentralCoverCandidateFrattiniExactImageSurjectivityData B T self.obstructionIndexToBase.O self.affineFiberTorsor.Z self.affineFiberTorsor.F

Refined residual packet

The old residual in CentralCoverFineResiduals.lean, centralCover_candidateLiftPartitionCardinality, quantifies over arbitrary, separately supplied obstruction data, cocycle data, and lift fibres. That is not the manuscript shape of lem:covertransform and prop:finalfourier.

The theorem-level affine fibre construction supplies the regular torsor under candidate Z^1(R). The remaining residuals are the target/source semantic pieces that the current API does not expose: quotienting top exact-image maps to the middle target, matching the obstruction index to lower exact-image maps, and the Frattini exact-image partition.

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

CANDIDATE EXACT-IMAGE BASE QUOTIENT INPUT.

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

CANDIDATE OBSTRUCTION-INDEX-TO-BASE INPUT.

axiom Q2Presentation.Induction.centralCover_candidateFrattiniExactImageSurjectivityData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (O : CentralCoverSourceObstructionData B centralCoverCandidateSource) (Z : CentralCoverSourceCocycleData B) (F : CentralCoverSourceLiftFibers B centralCoverCandidateSource O Z) : Nonempty (CentralCoverCandidateFrattiniExactImageSurjectivityData B T O Z F)

CANDIDATE FRATTINI EXACT-IMAGE INPUT.

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

REFINED CANDIDATE R-LIFT INPUT.

Manuscript anchors: def:Xgamma, lem:covertransform, lem:affinelifting, and prop:finalfourier. This theorem-level packet now reassembles the smaller residuals above instead of hiding them in one axiom.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_refined {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverCandidateLiftPartitionData B)

The refined packet is now a theorem from the semantic R-lift data. The obstruction index is supplied by the exact-image base packet, not by a PUnit/zero-obstruction shortcut.

structure Q2Presentation.Induction.CentralCoverCandidateLiftPartitionCardinalityPacket {p : FramedPair} (B : MinimalBlock p) : Type 1

The cardinality shadow of a coherent candidate lift-partition packet.

• O : CentralCoverSourceObstructionData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd)
• Z : CentralCoverSourceCocycleData B
• F : CentralCoverSourceLiftFibers B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) self.O self.Z
• cardinality : CentralCoverSourceLiftPartitionCardinality B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) self.O self.Z self.F

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionCardinality_refined {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverCandidateLiftPartitionCardinalityPacket B)

Cardinality statement for the coherently chosen candidate packet.

This deliberately does not prove centralCover_candidateLiftPartitionCardinality for arbitrary independently chosen O, Z, and F.

theorem Q2Presentation.Induction.centralCover_candidateLiftData_fine_refined {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverSourceLiftData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd))

Candidate source-lift data reassembled from the coherent refined packet.

This is the downstream replacement for the candidate side of centralCover_candidateLiftData_fine; its axiom closure names the coherent packet above instead of the old arbitrary-cardinality residual.

theorem Q2Presentation.Induction.centralCover_liftTorsorData_fine_refined {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverLiftTorsorData B)

Lift-torsor data with the candidate side routed through the coherent candidate lift-partition packet.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_refined {p : FramedPair} (B : MinimalBlock p) : Nonempty (CoverRealization B)

Full central-cover realization reassembled with the refined candidate lift-partition packet.

The proof intentionally reuses the existing child and partial-recipe refinements without editing their supervisor-owned integration file.