Finer manuscript-backed residuals for the Section 8 bridge

This sidecar continues from CentralCoverResidualRefinement.lean. It does not close the Section 8 bridge from the current library; instead it replaces the current broad residuals by smaller manuscript-facing pieces.

The split is governed by reference/q2_manuscript.tex, Section 8 sec:fourier, and by reference/plan_4turns.md's Stage-H requirement that main-clean theorems expose their actual axiom closure.

Compared with CentralCoverResidualRefinement.lean:

• each source lift residual is split into:
  • an exact-image obstruction index (def:Xgamma, lem:obstructionseparation, prop:finalfourier);
  • a Z^1(R) cocycle group of size z_R (lem:affinelifting, eq:mumultiplicity);
  • lift fibres and the boundary-framed exact-image decomposition (lem:covertransform, prop:finalfourier);
• the children residual is split into the three strict-decrease strata of lem:strictdecrease: elementary-stage/proper-image/phase-cover targets. The elementary stage is further split into the lower quotient target C = Y/K and the finite proper-image subtraction family of eq:Mstage;
• the partial-count residual is split sourcewise, with a separate source-interface agreement axiom identifying the candidate and local recipes. The local-side live axioms are named at the smaller residual layer: finite exact-image indexing, Tate obstruction maps, Euler/Tate cocycle cardinality, affine lift partitions, and the Tate/Evens/local-Arf source-interface comparison.

No theorem below uses centralCover_realization, centralCover_liftTorsorData, centralCover_partialRecipe, or the previous sidecar's sourcewise/partial residual axioms.

Finer source-lift residuals

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

Source-specific exact-image obstruction index and obstruction map.

Manuscript anchors: def:Xgamma, lem:obstructionseparation, and the o_R : X_Gamma(B) -> O_R input to prop:finalfourier.

• X : Type
• finX : Fintype self.X
• o : self.X → B.obstructionSpace

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

Source-specific Z^1_Gamma(R) group with the common size z_R.

Manuscript anchors: lem:affinelifting, eq:mumultiplicity, and the source-interface lift-multiplicity comparison.

• Z1 : Type
• agZ1 : AddGroup self.Z1
• zcard : Nat.card self.Z1 = B.zR

structure Q2Presentation.Induction.CentralCoverSourceFiberData {p : FramedPair} (B : MinimalBlock p) (S : Type) (O : CentralCoverSourceObstructionData B S) (Z : CentralCoverSourceCocycleData B) : Type 1

Source-specific lift fibres and the boundary-framed surjection decomposition over unobstructed base maps.

Manuscript anchors: lem:covertransform and prop:finalfourier, including the Frattini-surjectivity clause that every unobstructed R-lift is already surjective onto the top target.

• Lift : { x : O.X // O.o x = 0 } → Type
• torsor (x : { x : O.X // O.o x = 0 }) : AddTorsor Z.Z1 (self.Lift x)
• finLift (x : { x : O.X // O.o x = 0 }) : Finite (self.Lift x)
• bij : S ≃ (x : { x : O.X // O.o x = 0 }) × self.Lift x

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

The finite exact-image index before the obstruction map is applied.

Manuscript anchor: def:Xgamma. This separates finiteness of the exact-image lower maps from the construction of the R-valued obstruction.

• X : Type
• finX : Fintype self.X

structure Q2Presentation.Induction.CentralCoverSourceObstructionMap {p : FramedPair} (B : MinimalBlock p) (S : Type) (I : CentralCoverSourceObstructionIndex B S) : Type

The obstruction map on a fixed finite exact-image index.

Manuscript anchor: lem:obstructionseparation: the obstruction lands in O_R = B.obstructionSpace.

• o : I.X → B.obstructionSpace

def Q2Presentation.Induction.obstructionData_of_indexMap {p : FramedPair} (B : MinimalBlock p) (S : Type) (I : CentralCoverSourceObstructionIndex B S) (O : CentralCoverSourceObstructionMap B S I) : CentralCoverSourceObstructionData B S

Reassemble obstruction data from the finite index and obstruction map.

Equations

• Q2Presentation.Induction.obstructionData_of_indexMap B S I O = { X := I.X, finX := I.finX, o := O.o }

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

theorem Q2Presentation.Induction.centralCover_candidateObstructionMap {p : FramedPair} (B : MinimalBlock p) (I : CentralCoverSourceObstructionIndex B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd)) : Nonempty (CentralCoverSourceObstructionMap B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) I)

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

Candidate obstruction data assembled from the finite exact-image index and the obstruction map. This theorem replaces the previous single candidate obstruction residual.

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

The additive cocycle group before asserting its manuscript cardinality.

Manuscript anchor: lem:affinelifting, where the lift fibres are torsors under Z^1_Gamma(R).

• Z1 : Type
• agZ1 : AddGroup self.Z1

structure Q2Presentation.Induction.CentralCoverSourceCocycleCardinality {p : FramedPair} (B : MinimalBlock p) (Z : CentralCoverSourceCocycleGroup B) : Prop

The common cardinality formula for a fixed cocycle group.

Manuscript anchor: eq:mumultiplicity / prop:finalfourier, |Z^1_Gamma(R)| = z_R.

• zcard : Nat.card Z.Z1 = B.zR

def Q2Presentation.Induction.cocycleData_of_groupCard {p : FramedPair} (B : MinimalBlock p) (Z : CentralCoverSourceCocycleGroup B) (C : CentralCoverSourceCocycleCardinality B Z) : CentralCoverSourceCocycleData B

Reassemble cocycle data from the group and its cardinality theorem.

Equations

• Q2Presentation.Induction.cocycleData_of_groupCard B Z C = { Z1 := Z.Z1, agZ1 := Z.agZ1, zcard := ⋯ }

def Q2Presentation.Induction.centralCover_candidateCanonicalCocycleGroup {p : FramedPair} (B : MinimalBlock p) : CentralCoverSourceCocycleGroup B

A concrete finite additive group with the candidate-side cocycle cardinality required by the current §8 interface. It packages the manuscript's 2^{2 dim R} affine part with the character group of O_R.

Equations

• Q2Presentation.Induction.centralCover_candidateCanonicalCocycleGroup B = { Z1 := ZMod (2 ^ B.dimExp) × Module.Dual (ZMod 2) B.obstructionSpace, agZ1 := Prod.instAddGroup }

theorem Q2Presentation.Induction.centralCover_candidateCocycleGroup {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverSourceCocycleGroup B)

axiom Q2Presentation.Induction.centralCover_candidateCocycleCardinality {p : FramedPair} (B : MinimalBlock p) (Z : CentralCoverSourceCocycleGroup B) : Nonempty (CentralCoverSourceCocycleCardinality B Z)

theorem Q2Presentation.Induction.centralCover_candidateCanonicalCocycleCardinality {p : FramedPair} (B : MinimalBlock p) : CentralCoverSourceCocycleCardinality B (centralCover_candidateCanonicalCocycleGroup B)

The canonical candidate cocycle group has the block cardinality z_R, by the definition of MinimalBlock.zR.

theorem Q2Presentation.Induction.centralCover_candidateCocycleData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverSourceCocycleData B)

Candidate cocycle data assembled from the cocycle group and the separate cardinality computation.

structure Q2Presentation.Induction.CentralCoverSourceLiftFibers {p : FramedPair} (B : MinimalBlock p) (S : Type) (O : CentralCoverSourceObstructionData B S) (Z : CentralCoverSourceCocycleData B) : Type 1

Lift fibres over unobstructed points, before partitioning the global boundary-framed surjection set.

Manuscript anchor: lem:affinelifting.

• Lift : { x : O.X // O.o x = 0 } → Type
• torsor (x : { x : O.X // O.o x = 0 }) : AddTorsor Z.Z1 (self.Lift x)
• finLift (x : { x : O.X // O.o x = 0 }) : Finite (self.Lift x)

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

Exact-image partition of the global surjection set by the unobstructed lift fibres.

Manuscript anchors: lem:covertransform and prop:finalfourier, including Frattini surjectivity of the final R-lifts.

• bij : S ≃ (x : { x : O.X // O.o x = 0 }) × F.Lift x

def Q2Presentation.Induction.fiberData_of_fibersPartition {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) : CentralCoverSourceFiberData B S O Z

Reassemble fibre data from lift fibres and the exact-image partition.

Equations

• Q2Presentation.Induction.fiberData_of_fibersPartition B S O Z F P = { Lift := F.Lift, torsor := F.torsor, finLift := ⋯, bij := P.bij }

theorem Q2Presentation.Induction.centralCover_zR_ne_zero {p : FramedPair} (B : MinimalBlock p) : B.zR ≠ 0

The block lift-torsor size z_R is nonzero.

theorem Q2Presentation.Induction.centralCover_cocycleData_finite {p : FramedPair} (B : MinimalBlock p) (Z : CentralCoverSourceCocycleData B) : Finite Z.Z1

Any cocycle datum with cardinality z_R is finite.

theorem Q2Presentation.Induction.centralCover_candidateLiftFibers {p : FramedPair} (B : MinimalBlock p) (O : CentralCoverSourceObstructionData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd)) (Z : CentralCoverSourceCocycleData B) : Nonempty (CentralCoverSourceLiftFibers B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) O Z)

Candidate lift fibres can be populated by the regular torsor under the chosen cocycle group. This discharges the affine-fibre part of lem:affinelifting; the remaining exact-image content is the partition/cardinality statement below.

theorem Q2Presentation.Induction.centralCover_tfg_GammaA : Profinite.TopologicallyFinitelyGenerated GammaA

Candidate Gamma_A is topologically finitely generated, using the four universal generators. This local copy avoids importing the final capstone file back into the §8 sidecar.

theorem Q2Presentation.Induction.centralCover_candidateBoundaryFramedSurj_finite {p : FramedPair} : Finite (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd)

The candidate boundary-framed surjection set is finite.

structure Q2Presentation.Induction.CentralCoverSourceLiftPartitionCardinality {p : FramedPair} (B : MinimalBlock p) (S : Type) (O : CentralCoverSourceObstructionData B S) (Z : CentralCoverSourceCocycleData B) (F : CentralCoverSourceLiftFibers B S O Z) : Prop

Cardinal form of the exact-image lift partition. This is the remaining candidate finite bookkeeping statement: the actual maps and the disjoint union of unobstructed lift fibres have the same finite cardinality.

• card_eq : Nat.card S = Nat.card ((x : { x : O.X // O.o x = 0 }) × F.Lift x)

noncomputable def Q2Presentation.Induction.liftPartition_of_cardinality {p : FramedPair} (B : MinimalBlock p) (S : Type) [Finite S] (O : CentralCoverSourceObstructionData B S) (Z : CentralCoverSourceCocycleData B) (F : CentralCoverSourceLiftFibers B S O Z) (C : CentralCoverSourceLiftPartitionCardinality B S O Z F) : CentralCoverSourceLiftPartition B S O Z F

Recover the exact-image lift partition from its finite cardinal form.

Equations

• Q2Presentation.Induction.liftPartition_of_cardinality B S O Z F C = { bij := Classical.choice ⋯ }

axiom Q2Presentation.Induction.centralCover_candidateLiftPartitionCardinality {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) : Nonempty (CentralCoverSourceLiftPartitionCardinality B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) O Z F)

theorem Q2Presentation.Induction.centralCover_candidateLiftPartition {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) : Nonempty (CentralCoverSourceLiftPartition B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) O Z F)

Candidate exact-image lift partition recovered from the finite cardinal partition residual.

theorem Q2Presentation.Induction.centralCover_candidateFiberData {p : FramedPair} (B : MinimalBlock p) (O : CentralCoverSourceObstructionData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd)) (Z : CentralCoverSourceCocycleData B) : Nonempty (CentralCoverSourceFiberData B (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) O Z)

Candidate fibre data assembled from the affine lift fibres and exact-image partition.

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

Σ-witness form of the local Tate/Euler affine-lift input (checkpoint-F7).

The former packet CentralCoverLocalTateEulerAffineLiftTheory carried forall-quantified realization clauses (forall Z, Nonempty (Cardinality Z) and forall O Z F, Nonempty (LiftPartition ...)) that are FALSE at junk instantiations (e.g. a one-point cocycle group, or an everywhere-nonzero obstruction map with a nonempty local surjection set), making the old packet uninhabitable and its existence axiom inconsistent — instance #13 of the over-strong residual shape documented in PROGRESS.md. This witness form carries ONE coherent chain chosen by the manuscript's local arguments: local Tate duality supplies the obstruction map and perfectness, Euler--Poincare the Z^1 cardinality, and the local affine lifting statement the torsor fibres and exact-image partition (lem:obstructionseparation, lem:affinelifting, prop:finalfourier).

• I : CentralCoverSourceObstructionIndex B (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd)
• O : CentralCoverSourceObstructionMap B (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd) self.I
• Z : CentralCoverSourceCocycleGroup B
• Zcard : CentralCoverSourceCocycleCardinality B self.Z
• fibers : CentralCoverSourceLiftFibers B (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd) (obstructionData_of_indexMap B (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd) self.I self.O) (cocycleData_of_groupCard B self.Z ⋯)
• partition : CentralCoverSourceLiftPartition B (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd) (obstructionData_of_indexMap B (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd) self.I self.O) (cocycleData_of_groupCard B self.Z ⋯) self.fibers

axiom Q2Presentation.Induction.centralCover_localTateEulerAffineLiftWitness {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverLocalTateEulerAffineLiftWitness B)

LOCAL TATE/EULER AFFINE-LIFT INPUT (existence-form; checkpoint-F7).

def Q2Presentation.Induction.sourceLiftData_of_fine {p : FramedPair} (B : MinimalBlock p) (S : Type) (O : CentralCoverSourceObstructionData B S) (Z : CentralCoverSourceCocycleData B) (F : CentralCoverSourceFiberData B S O Z) : CentralCoverSourceLiftData B S

Reassemble the previous sourcewise lift packet from obstruction/cocycle/fibre pieces.

Equations

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

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

Candidate source lift data, refined beyond centralCover_candidateLiftData.

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

Local source lift data, refined beyond centralCover_localLiftData (checkpoint-F7: assembled from the coherent Σ-witness).

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

The coarser lift-torsor residual follows from the finer source pieces, not from centralCover_candidateLiftData or centralCover_localLiftData.

Finer children residuals

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

One strict-decrease stratum of Section 8 recursive children.

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

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

Elementary-stage children from eq:Mstage / eq:Mdescent.

Unlike a bare child list, this records the lower target C separately from the proper-image terms subtracted in the elementary stage.

• lowerChild : FramedPair
• lower_small : framedMeasure self.lowerChild < framedMeasure p
• properChildren : List FramedPair
• proper_small (c : FramedPair) : c ∈ self.properChildren → framedMeasure c < framedMeasure p

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

The lower quotient target C = Y/K from eq:targettower, appearing in the elementary lifting formula eq:Mstage.

The strict decrease is the first inequality of lem:strictdecrease, |L_C| = |L_Y| / |K| < |L_Y|. This packet is deliberately nonempty data: the elementary stage always has the lower target term e_Gamma(C).

• lowerChild : FramedPair
• lower_small : framedMeasure self.lowerChild < framedMeasure p

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

The finite family of proper exact-image terms subtracted in the elementary stage eq:Mstage.

Each listed child is a proper subgroup J < B projecting onto C, equipped with the inherited boundary-framed structure. Its strict decrease is eq:Mdescent. The index family may be empty in the degenerate case where no proper exact images occur; the elementary stage itself is still non-vacuous because CentralCoverElementaryLowerTarget supplies the lower target C.

• properImages : Type
• finProperImages : Fintype self.properImages
• properChildren : List FramedPair
• origin (c : FramedPair) : c ∈ self.properChildren → self.properImages
• proper_small (c : FramedPair) : c ∈ self.properChildren → framedMeasure c < framedMeasure p

def Q2Presentation.Induction.childStratum_of_elementaryStage {p : FramedPair} (B : MinimalBlock p) (E : CentralCoverElementaryStageChildren B) : CentralCoverChildStratum B

Convert the elementary-stage data into the generic child-stratum interface.

Equations

• Q2Presentation.Induction.childStratum_of_elementaryStage B E = { children := E.lowerChild :: E.properChildren, small := ⋯ }

def Q2Presentation.Induction.elementaryStageChildren_of_lowerProper {p : FramedPair} (B : MinimalBlock p) (L : CentralCoverElementaryLowerTarget B) (P : CentralCoverElementaryProperImageChildrenData B) : CentralCoverElementaryStageChildren B

Reassemble the elementary-stage children from the lower quotient target and the proper exact-image subtraction family.

Equations

• Q2Presentation.Induction.elementaryStageChildren_of_lowerProper B L P = { lowerChild := L.lowerChild, lower_small := ⋯, properChildren := P.properChildren, proper_small := ⋯ }

axiom Q2Presentation.Induction.centralCover_elementaryLowerTarget {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryLowerTarget B)

Elementary lower-target residual.

Manuscript anchors: eq:targettower, eq:Mstage, and the lower-target part of lem:strictdecrease. This is the construction of the boundary-framed lower quotient C = Y/K with |L_C| < |L_Y|.

axiom Q2Presentation.Induction.centralCover_elementaryProperImageChildrenData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryProperImageChildrenData B)

Elementary proper-image residual.

Manuscript anchors: the proper-image subtraction in eq:Mstage and the strict-decrease estimate eq:Mdescent. This isolates only the finite family of proper exact-image children, not the lower target C.

theorem Q2Presentation.Induction.centralCover_elementaryStageChildren {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryStageChildren B)

Elementary-stage children assembled from the lower target C = Y/K and the proper elementary exact-image subtraction terms.

theorem Q2Presentation.Induction.centralCover_elementaryChildren {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverChildStratum B)

Elementary-stage children assembled from the lower target and the proper elementary exact-image terms.

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

Proper-image scalar-pushout children from eq:recursionR2, eq:recursionR3, and eq:properweighteddescent.

The properImages field records the finite family of scalar-pushout proper image strata generating the child list.

• properImages : Type
• finProperImages : Fintype self.properImages
• children : List FramedPair
• origin (c : FramedPair) : c ∈ self.children → self.properImages
• small (c : FramedPair) : c ∈ self.children → framedMeasure c < framedMeasure p

def Q2Presentation.Induction.childStratum_of_properImageData {p : FramedPair} (B : MinimalBlock p) (P : CentralCoverProperImageChildrenData B) : CentralCoverChildStratum B

Convert proper-image data into the generic child-stratum interface.

Equations

• Q2Presentation.Induction.childStratum_of_properImageData B P = { children := P.children, small := ⋯ }

theorem Q2Presentation.Induction.centralCover_properImageChildrenData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverProperImageChildrenData B)

theorem Q2Presentation.Induction.centralCover_properImageChildren {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverChildStratum B)

Proper-image scalar-pushout children assembled from their finite stratum index.

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

Phase-cover children from lem:phasecover and eq:phasecoverdescent.

The phaseClasses field records the finite target-side scalar classes zeta in H^2(C,F_2) whose central double covers contribute children.

• phaseClasses : Type
• finPhaseClasses : Fintype self.phaseClasses
• children : List FramedPair
• origin (c : FramedPair) : c ∈ self.children → self.phaseClasses
• small (c : FramedPair) : c ∈ self.children → framedMeasure c < framedMeasure p

def Q2Presentation.Induction.childStratum_of_phaseCoverData {p : FramedPair} (B : MinimalBlock p) (P : CentralCoverPhaseCoverChildrenData B) : CentralCoverChildStratum B

Convert phase-cover data into the generic child-stratum interface.

Equations

• Q2Presentation.Induction.childStratum_of_phaseCoverData B P = { children := P.children, small := ⋯ }

theorem Q2Presentation.Induction.centralCover_phaseCoverChildrenData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverPhaseCoverChildrenData B)

theorem Q2Presentation.Induction.centralCover_phaseCoverChildren {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverChildStratum B)

Phase-cover children assembled from their finite phase-class index.

def Q2Presentation.Induction.childrenData_of_strata {p : FramedPair} (B : MinimalBlock p) (E P Ph : CentralCoverChildStratum B) : CentralCoverChildrenData B

Reassemble all strict-decrease child strata into the previous children packet.

Equations

• Q2Presentation.Induction.childrenData_of_strata B E P Ph = { children := E.children ++ (P.children ++ Ph.children), small := ⋯ }

theorem Q2Presentation.Induction.centralCover_childrenData_fine {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverChildrenData B)

The previous children residual follows from the three Section 8 child strata.

Finer partial-recipe residuals

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

Candidate-source partial-count recipe and realization, before comparison to the local recipe.

Manuscript anchors: candidate instances of lem:properimagesubtraction, prop:nonzeroedge, prop:zeroedge, prop:phaseidentity, and lem:phasecover.

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

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

Local-source partial-count recipe and realization, before comparison to the candidate recipe.

This structure is finite exact-image/Fourier scaffolding. The local arithmetic needed to populate it is kept in the named local partial-formula axioms below.

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

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

The source-side formula components whose sum is the partial-count recipe.

These are the finite/combinatorial pieces of eq:recursionR2 through eq:phasecovertransform: elementary lifting, proper-image subtraction, nonzero radical-edge terms, zero-edge constrained Gauss terms, and phase-cover transforms. The terms are kept separate so the public partial-data theorem is not a single arbitrary function.

• elementaryTerm : Module.Dual (ZMod 2) B.obstructionSpace → List ℕ → ℕ
• properImageTerm : Module.Dual (ZMod 2) B.obstructionSpace → List ℕ → ℕ
• nonzeroEdgeTerm : Module.Dual (ZMod 2) B.obstructionSpace → List ℕ → ℕ
• zeroEdgeTerm : Module.Dual (ZMod 2) B.obstructionSpace → List ℕ → ℕ
• phaseCoverTerm : Module.Dual (ZMod 2) B.obstructionSpace → List ℕ → ℕ

def Q2Presentation.Induction.CentralCoverSourcePartialFormula.partialN {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverLiftTorsorData B} {C : CentralCoverChildrenData B} (F : CentralCoverSourcePartialFormula B T C) : Module.Dual (ZMod 2) B.obstructionSpace → List ℕ → ℕ

The assembled source partial recipe.

Equations

• F.partialN chi counts = F.elementaryTerm chi counts + F.properImageTerm chi counts + F.nonzeroEdgeTerm chi counts + F.zeroEdgeTerm chi counts + F.phaseCoverTerm chi counts

structure Q2Presentation.Induction.CentralCoverCandidatePartialFormulaRealization {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (F : CentralCoverSourcePartialFormula B T C) : Prop

Candidate-source realization of an assembled partial formula.

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

structure Q2Presentation.Induction.CentralCoverLocalPartialFormulaRealization {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (F : CentralCoverSourcePartialFormula B T C) : Prop

Local-source realization of an assembled partial formula.

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

def Q2Presentation.Induction.candidatePartialData_of_formula {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (F : CentralCoverSourcePartialFormula B T C) (R : CentralCoverCandidatePartialFormulaRealization B T C F) : CentralCoverCandidatePartialData B T C

Reassemble candidate partial data from formula components and their candidate-source realization.

Equations

• Q2Presentation.Induction.candidatePartialData_of_formula B T C F R = { partialN := F.partialN, partialA := ⋯ }

def Q2Presentation.Induction.localPartialData_of_formula {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (F : CentralCoverSourcePartialFormula B T C) (R : CentralCoverLocalPartialFormulaRealization B T C F) : CentralCoverLocalPartialData B T C

Reassemble local partial data from formula components and their local-source realization.

Equations

• Q2Presentation.Induction.localPartialData_of_formula B T C F R = { partialN := F.partialN, partialQ := ⋯ }

def Q2Presentation.Induction.centralCover_candidateCountingPartialFormula {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) : CentralCoverSourcePartialFormula B T C

Candidate-source formula that records the partial count directly in the elementary component. The later source-interface axiom is still responsible for identifying this candidate recipe with the local Tate/Arf recipe.

Equations

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

theorem Q2Presentation.Induction.centralCover_candidatePartialFormula {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) : Nonempty (CentralCoverSourcePartialFormula B T C)

axiom Q2Presentation.Induction.centralCover_candidatePartialFormulaRealization {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (F : CentralCoverSourcePartialFormula B T C) : Nonempty (CentralCoverCandidatePartialFormulaRealization B T C F)

theorem Q2Presentation.Induction.centralCover_candidateCountingPartialFormulaRealization {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) : CentralCoverCandidatePartialFormulaRealization B T C (centralCover_candidateCountingPartialFormula B T C)

The direct candidate formula realizes the candidate partial counts definitionally.

theorem Q2Presentation.Induction.centralCover_candidatePartialData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) : Nonempty (CentralCoverCandidatePartialData B T C)

Candidate-source partial-count data assembled from the five formula components and their realization.

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

The local Arf/Hilbert/Evens partial-count primitive for the source-local zero-edge and phase-cover formulas.

This bundles the local formula components together with their realization on the local source. The cited content is the dyadic local Arf/Gauss computation, the Hilbert-symbol and Evens-normalization ledger, plus the Tate-duality pairing used in the constrained Gauss and phase-cover terms.

• formula : Nonempty (CentralCoverSourcePartialFormula B T C)
• realization (F : CentralCoverSourcePartialFormula B T C) : Nonempty (CentralCoverLocalPartialFormulaRealization B T C F)

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

LOCAL ARF/HILBERT/EVENS PARTIAL-FORMULA INPUT. The local source's partial-count formula and realization after the finite formula wrappers have been made theorem-level projections.

theorem Q2Presentation.Induction.centralCover_localTateArfPartialFormula {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) : Nonempty (CentralCoverSourcePartialFormula B T C)

The local source's five partial-count formula components, projected from the local Arf/Hilbert/Evens primitive.

theorem Q2Presentation.Induction.centralCover_localTateArfPartialFormulaRealization {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (F : CentralCoverSourcePartialFormula B T C) : Nonempty (CentralCoverLocalPartialFormulaRealization B T C F)

The realization that the local formula components compute the local partial counts for T.XQ, projected from the local Arf/Hilbert/Evens primitive.

theorem Q2Presentation.Induction.centralCover_localPartialFormula {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) : Nonempty (CentralCoverSourcePartialFormula B T C)

Backwards-compatible name for the local partial formula. The live axiom is centralCover_localTateArfPartialFormula.

theorem Q2Presentation.Induction.centralCover_localPartialFormulaRealization {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (F : CentralCoverSourcePartialFormula B T C) : Nonempty (CentralCoverLocalPartialFormulaRealization B T C F)

Backwards-compatible name for local partial-formula realization. The live axiom is centralCover_localTateArfPartialFormulaRealization.

theorem Q2Presentation.Induction.centralCover_localPartialData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) : Nonempty (CentralCoverLocalPartialData B T C)

Local-source partial-count data assembled from the five formula components and their realization.

axiom Q2Presentation.Induction.centralCover_tateEulerHilbertEvens_sourceInterfaceAgreement {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (A : CentralCoverCandidatePartialData B T C) (Q : CentralCoverLocalPartialData B T C) : A.partialN = Q.partialN

Source-interface agreement for the two separately constructed partial recipes.

Manuscript anchor: cor:sourceinterface, using Tate duality, Euler--Poincare, the local Hilbert/Evens normalization, and the local Arf/Gauss computation recorded in CentralCovers.lean.

theorem Q2Presentation.Induction.centralCover_tateEulerArf_sourceInterfaceAgreement {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (A : CentralCoverCandidatePartialData B T C) (Q : CentralCoverLocalPartialData B T C) : A.partialN = Q.partialN

Backwards-compatible name for source-interface agreement. The live axiom is centralCover_tateEulerHilbertEvens_sourceInterfaceAgreement.

theorem Q2Presentation.Induction.centralCover_partialRecipeAgreement {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (A : CentralCoverCandidatePartialData B T C) (Q : CentralCoverLocalPartialData B T C) : A.partialN = Q.partialN

Backwards-compatible name for source-interface agreement. The live axiom is centralCover_tateEulerHilbertEvens_sourceInterfaceAgreement.

axiom Q2Presentation.Induction.centralCover_localRealizesCandidatePartialFormula {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) : Nonempty (CentralCoverLocalPartialFormulaRealization B T C (centralCover_candidateCountingPartialFormula B T C))

LOCAL SOURCE-INTERFACE INPUT (fused, existence-form; checkpoint-F6).

The local source realizes the canonical candidate partial formula — manuscript cor:sourceinterface: the recursion coefficients are source-independent, so the single formula whose elementary term records the candidate partial count is also realized by the local source (local Tate duality / Euler-Poincare, the dyadic Arf/Gauss computation, and the Hilbert/Evens normalization).

This replaces the pair {centralCover_localArfHilbertEvensPartialTheory, centralCover_tateEulerHilbertEvens_sourceInterfaceAgreement} on the live route: the former contained a forall F realization clause (false at junk formulas) and the latter demanded function-level equality of arbitrary packets' partialN (false at packets differing off the realized child-count lists) — instances #11/#12 of the over-strong residual shape documented in PROGRESS.md.

def Q2Presentation.Induction.partialRecipe_of_sourceAgreement {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (C : CentralCoverChildrenData B) (A : CentralCoverCandidatePartialData B T C) (Q : CentralCoverLocalPartialData B T C) (h : A.partialN = Q.partialN) : CentralCoverPartialRecipe B T

Reassemble the previous partial recipe from source-specific recipes plus the source-interface agreement.

Equations

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

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

The coarser partial residual follows from source-specific recipes and their source-interface agreement, not from centralCover_partialSkeleton, centralCover_candidatePartialRealization, or centralCover_localPartialRealization.

Full reassembly from finer residuals

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

Same target statement as centralCover_realization, reassembled from the finer residuals in this file.

The closure should not contain the old monolithic axiom centralCover_realization, the two-residual split centralCover_liftTorsorData/centralCover_partialRecipe, or the previous six-residual sidecar axioms.