Finer residuals for the Section 8 central-cover realization

Q2Presentation/Induction/CentralCoverRealization.lean already replaces the monolithic Section 8 axiom centralCover_realization by two residuals:

• centralCover_liftTorsorData;
• centralCover_partialRecipe.

This sidecar refines those two residuals further. It does not use the vacuity diagnostic route through an underconstrained MinimalBlock; the data below is the explicit Section 8 exact-image/lift data required by the manuscript.

Manuscript anchors are reference/q2_manuscript.tex, Section 8 sec:fourier:

• sourcewise lift torsor packets: def:Xgamma, lem:covertransform, lem:affinelifting, and prop:finalfourier;
• strict recursive children: lem:strictdecrease;
• shared partial-count recipe: lem:properimagesubtraction, prop:nonzeroedge, prop:zeroedge, prop:phaseidentity, and lem:phasecover.

This matches reference/plan_4turns.md's finite-quotient/epimorphism-count architecture and its #print axioms discipline: the final theorem in this file has the same target statement as centralCover_realization, but its closure exposes only the finer manuscript residuals below, not the earlier coarser residuals.

Sourcewise lift-torsor packets

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

A single-source version of the lift-torsor/orbit data in CentralCoverLiftTorsorData.

For a source-specific boundary-framed surjection set S, this is exactly the data asserted in manuscript prop:finalfourier: finite exact-image base maps, the R-valued obstruction, a Z^1(R) group of size z_R, lift fibres that are torsors under that group, and a bijection from boundary-framed surjections onto the unobstructed lift fibres.

• X : Type
• finX : Fintype self.X
• o : self.X → B.obstructionSpace
• Z : Type
• agZ : AddGroup self.Z
• zcard : Nat.card self.Z = B.zR
• Lift : { x : self.X // self.o x = 0 } → Type
• torsor (x : { x : self.X // self.o x = 0 }) : AddTorsor self.Z (self.Lift x)
• finLift (x : { x : self.X // self.o x = 0 }) : Finite (self.Lift x)
• bij : S ≃ (x : { x : self.X // self.o x = 0 }) × self.Lift x

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

Candidate-source lift residual (Gamma_A).

Manuscript anchors: def:Xgamma, lem:covertransform, lem:affinelifting, and prop:finalfourier, specialized to the candidate source and its boundary package.

axiom Q2Presentation.Induction.centralCover_localLiftData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverSourceLiftData B (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd))

Local-source lift residual (G_{Q_2}).

Manuscript anchors: the same sourcewise part of sec:fourier, specialized to the local source and its boundary package.

def Q2Presentation.Induction.liftTorsorData_of_sourceData {p : FramedPair} (B : MinimalBlock p) (A : CentralCoverSourceLiftData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd)) (Q : CentralCoverSourceLiftData B (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd)) : CentralCoverLiftTorsorData B

Combine the two sourcewise lift packets into the coarser residual type from CentralCoverRealization.lean.

Equations

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

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

The coarser lift residual follows from the two sourcewise packets.

Finer partial-count residuals

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

Strictly smaller recursive targets, isolated from the partial-count formula.

Manuscript anchor: lem:strictdecrease.

• children : List FramedPair
• small (c : FramedPair) : c ∈ self.children → framedMeasure c < framedMeasure p

axiom Q2Presentation.Induction.centralCover_childrenData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverChildrenData B)

Strict-decrease residual for Section 8 exact-image children.

structure Q2Presentation.Induction.CentralCoverPartialSkeleton {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) : Type

The shared source-independent partial-count function, before asserting that either source realizes it.

Manuscript anchors: the algebraic expression assembled from lem:properimagesubtraction, prop:nonzeroedge, prop:zeroedge, prop:phaseidentity, and lem:phasecover.

• partialN : Module.Dual (ZMod 2) B.obstructionSpace → List ℕ → ℕ

axiom Q2Presentation.Induction.centralCover_partialSkeleton {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) : Nonempty (CentralCoverPartialSkeleton B T C)

Shared partial-recipe residual, before sourcewise realization.

structure Q2Presentation.Induction.CentralCoverCandidatePartialRealization {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (N : CentralCoverPartialSkeleton B T C) : Prop

Candidate-source realization of the shared partial-count recipe.

• partialA (chi : Module.Dual (ZMod 2) B.obstructionSpace) : Nat.card { x : T.XA // chi (T.oA x) = 0 } = N.partialN chi (List.map (⇑Cardinal.toNat) (List.map framedCountA C.children))

structure Q2Presentation.Induction.CentralCoverLocalPartialRealization {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (N : CentralCoverPartialSkeleton B T C) : Prop

Local-source realization of the shared partial-count recipe.

• partialQ (chi : Module.Dual (ZMod 2) B.obstructionSpace) : Nat.card { x : T.XQ // chi (T.oQ x) = 0 } = N.partialN chi (List.map (⇑Cardinal.toNat) (List.map framedCountQ C.children))

axiom Q2Presentation.Induction.centralCover_candidatePartialRealization {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (N : CentralCoverPartialSkeleton B T C) : Nonempty (CentralCoverCandidatePartialRealization B T C N)

Candidate partial-count residual.

Manuscript anchors: the candidate-source instances of eq:recursionR2--eq:phasecovertransform.

axiom Q2Presentation.Induction.centralCover_localPartialRealization {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (N : CentralCoverPartialSkeleton B T C) : Nonempty (CentralCoverLocalPartialRealization B T C N)

Local partial-count residual.

Manuscript anchors: the local-source instances of eq:recursionR2--eq:phasecovertransform, with source-independence supplied by the same N.partialN.

def Q2Presentation.Induction.partialRecipe_of_refined {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (N : CentralCoverPartialSkeleton B T C) (A : CentralCoverCandidatePartialRealization B T C N) (Q : CentralCoverLocalPartialRealization B T C N) : CentralCoverPartialRecipe B T

Reassemble the coarser CentralCoverPartialRecipe residual from the finer children/skeleton/source-realization residuals.

Equations

• Q2Presentation.Induction.partialRecipe_of_refined B T C N A Q = { children := C.children, small := ⋯, partialN := N.partialN, partialA := ⋯, partialQ := ⋯ }

theorem Q2Presentation.Induction.centralCover_partialRecipe_refined {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) : Nonempty (CentralCoverPartialRecipe B T)

The coarser partial residual follows from the finer residuals, without using centralCover_partialRecipe.

Full reassembly using only the finer residuals

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

Same target statement as centralCover_realization, but with the coarser residuals refined away.

The axiom closure should contain the six finer residuals above, and should not contain centralCover_realization, centralCover_liftTorsorData, or centralCover_partialRecipe.