Central-cover realization: residual split for the Section 8 bridge

This module targets the remaining non-local-CFT Section 8 residual centralCover_realization from Q2Presentation/Induction/CentralCovers.lean.

The exact theorem

theorem centralCover_realization_proven {p : FramedPair} (B : MinimalBlock p) :
    Nonempty (CoverRealization B)

cannot be derived from the current Lean library without additional Section 8 orbit-combinatorial input. The reason is visible in the fields of CoverRealization B: Lean must be given actual source-by-source finite lift indices, obstruction maps, Z^1(R)-torsor fibres, boundary-framed surjection bijections, strictly smaller recursive children, and the common partial-count recipe. The current proved files provide the Fourier algebra and the torsor cardinality mechanism, but not those finite exact-image orbit partitions.

The split below follows manuscript reference/q2_manuscript.tex, Section 8 sec:fourier:

• CentralCoverLiftTorsorData is the lift-torsor/orbit half of prop:finalfourier, using lem:affinelifting and the central-cover exact-image partition lem:covertransform.
• CentralCoverPartialRecipe is the source-independent recursive recipe half, corresponding to lem:properimagesubtraction, prop:nonzeroedge, prop:zeroedge, prop:phaseidentity, lem:phasecover, and lem:strictdecrease.

This is also consistent with reference/plan_4turns.md: the plan requires finite-quotient/epimorphism-count semantics and no hidden axioms in accepted main-clean theorems. Accordingly, the theorem below exposes the exact residual axioms in #print axioms centralCover_realization_proven rather than hiding them inside a manufactured inhabitant of CoverRealization.

Residual 1: lift-torsor/orbit realization (prop:finalfourier)

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

The per-source lift-torsor and exact-image orbit data needed for the prop:finalfourier numerator over a fixed minimal block.

This is strictly weaker than CoverRealization B: it contains only the finite lift indices, obstruction maps, Z^1(R) torsor fibres, and the two boundary-framed surjection decompositions. It does not assert any recursive children or any source-independent partial-count recipe.

• XA : Type

  Candidate-source finite lift index X_A.

• finXA : Fintype self.XA
• oA : self.XA → B.obstructionSpace

  Candidate-source R-valued obstruction.

• ZA : Type

  Candidate-source cocycle group Z^1_A(R).

• agZA : AddGroup self.ZA
• zcardA : Nat.card self.ZA = B.zR

  Its size is the block's z_R.

• LiftA : { x : self.XA // self.oA x = 0 } → Type

  Candidate lift fibres over unobstructed exact-image base maps.

• torsorA (x : { x : self.XA // self.oA x = 0 }) : AddTorsor self.ZA (self.LiftA x)
• finLiftA (x : { x : self.XA // self.oA x = 0 }) : Finite (self.LiftA x)
• bijA : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd ≃ (x : { x : self.XA // self.oA x = 0 }) × self.LiftA x

  Candidate lift-torsor decomposition of boundary-framed surjections onto Y.

• XQ : Type

  Local-source finite lift index X_Q.

• finXQ : Fintype self.XQ
• oQ : self.XQ → B.obstructionSpace

  Local-source R-valued obstruction.

• ZQ : Type

  Local-source cocycle group Z^1_Q(R).

• agZQ : AddGroup self.ZQ
• zcardQ : Nat.card self.ZQ = B.zR

  Its size is the same block value z_R.

• LiftQ : { x : self.XQ // self.oQ x = 0 } → Type

  Local lift fibres over unobstructed exact-image base maps.

• torsorQ (x : { x : self.XQ // self.oQ x = 0 }) : AddTorsor self.ZQ (self.LiftQ x)
• finLiftQ (x : { x : self.XQ // self.oQ x = 0 }) : Finite (self.LiftQ x)
• bijQ : boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd ≃ (x : { x : self.XQ // self.oQ x = 0 }) × self.LiftQ x

  Local lift-torsor decomposition of boundary-framed surjections onto Y.

axiom Q2Presentation.Induction.centralCover_liftTorsorData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverLiftTorsorData B)

Residual Section 8 axiom, lift-torsor half.

Manuscript anchors: lem:covertransform, lem:affinelifting, and prop:finalfourier (eq:recursionR1 numerator, including Frattini surjectivity R = Phi(K)).

Residual 2: source-independent partial-count recipe

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

The strictly-smaller recursive targets and the common partial-count recipe for a fixed lift-torsor realization.

This is strictly weaker than CoverRealization B on its own: it has no boundary-framed surjection bijections and no Z^1(R) torsor fibres. It records only the source-independent recursive expression for the per-character partial counts.

• children : List FramedPair

  The strictly-smaller exact-image children targets.

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

  Strict decrease of the marked 2-kernel.

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

  Source-independent partial-count recipe.

• 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 self.children))

  Candidate partial-count realization.

• 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 self.children))

  Local partial-count realization.

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

Residual Section 8 axiom, partial-count half.

Manuscript anchors: lem:properimagesubtraction (eq:recursionR2/eq:recursionR3), prop:nonzeroedge (eq:recursionR4a), prop:zeroedge (eq:recursionR4b, via prop:phaseidentity), lem:phasecover (eq:recursionR5a/eq:phasecovertransform), and lem:strictdecrease.

Reassembly into the existing CoverRealization interface

def Q2Presentation.Induction.coverRealization_of {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) (R : CentralCoverPartialRecipe B T) : CoverRealization B

Reassemble the existing CoverRealization packet from the two strictly smaller Section 8 residuals.

Equations

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

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

The exact statement of the current centralCover_realization axiom, derived from the two exposed Section 8 residuals and not from the old monolithic axiom.

The axiom closure should list the two residuals centralCover_liftTorsorData and centralCover_partialRecipe, and should not list centralCover_realization.

Acceptance checks