Stage §8 — Central covers, the lift↔cohomology bridge, and the nonterminal Fourier branch

(manuscript sec:fourier, l.3771–4447)

This file discharges, as a theorem, the exact statement of the axiom Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch of Induction/Recursion.lean (the existence of a FourierBranchData p for a non-terminal target), WITHOUT using that axiom. It is the §8 layer sitting on top of the §7 block of Induction/MinimalBlock.lean: the minimal non-scalar block B : MinimalBlock p supplies the finite 𝔽₂ obstruction space W = O_R = B.obstructionSpace, the lift-torsor exponent/size dimExp = 2·dim R, zR = 2^{dimExp}·|Ŵ| (prop:finalfourier); §8 converts the lifting count into the per-source obstruction realization that the (already proven) finite Fourier inversion Recursion.fourier_recursion_step then turns into the recursion.

The §8 conversion, faithfully (manuscript sec:fourier)

prop:finalfourier (eq:recursionR1, l.4259) reads

  e_Γ(Y) = (z_R/|𝒳_R|) · Σ_{λ∈𝒳_R} (2·m_{Γ,λ}(B) − e_Γ(B)),     m_{Γ,0}(B) = e_Γ(B),

and its proof is the lift-torsor decomposition: for a fixed exact-image map to B the set of R-lifts, when the R-obstruction vanishes, is a torsor of size z_R = |Z¹_{Γ,ρ}(R)| (lem:affinelifting, eq:mumultiplicity; Lifting.lift_torsor_card), and every such lift is automatically surjective onto Y because R = Φ(K) is the Frattini subgroup (prop:finalfourier). Hence the boundary-framed surjections onto Y are, source by source, the disjoint union (a dependent Σ-type) over the unobstructed exact-image base maps {x : X_Γ // o_Γ x = 0} of the R-lift torsor:

  boundaryFramedSurj(Y)  ≃  Σ x : {x : X_Γ // o_Γ x = 0}, Lift_Γ x,

each Lift_Γ x an AddTorsor under the R-cocycle group Z¹_Γ(R) with |Z¹_Γ(R)| = z_R. We record exactly this torsor decomposition per source (CoverRealization.bijA/bijQ over ZA/LiftA, ZQ/LiftQ), so the realize_Γ numerator e_Γ(Y) = z_R·#{o_Γ = 0} (prop:finalfourier) is PROVEN here — not assumed — by the lift-torsor count Lifting.lift_torsor_card (framedCount_eq_zR_of_torsorDecomp) in realizeA_of/realizeQ_of.

The remaining per-character partial counts m_{Γ,χ}(B) = #{x : ⟨χ, o_Γ x⟩ = 0} are expressed through the strictly-smaller exact-image children by the single source-independent recipe partialN (partialA/partialQ), assembled from eq:recursionR2 (proper-image subtraction, lem:properimagesubtraction), eq:recursionR4a/eq:recursionR4b (the nonzero/zero radical-edge cases prop:nonzeroedge/prop:zeroedge, the constrained quadratic Gauss transform lem:constrainedgauss + the completed-square phase identity prop:phaseidentity), and eq:phasecovertransform (the phase covers lem:phasecover). Its source-independence is cor:sourceinterface: the lift multiplicities, perfect pairings, cup–Bockstein form and base Gauss sums coincide for the two sources — the comparison theorems Lifting.lift_torsor_card, Local.q2_local_Z1_dim, Lifting.isAdjointBoundary_unique, Quadratic.candidate_numZeros_eq_local/candidate_gauss_eq_local_gauss recorded in the SourceInterface section below.

Decomposition: proven vs. isolated

• PROVEN here, sorry-free (closure {propext, Classical.choice, Quot.sound} over the block + local-CFT axioms): the W/dimExp/zR/hzR reduction to MinimalBlock; the lift-torsor count mechanism framedCount_eq_zR_of_torsorDecomp (the z_R factor of prop:finalfourier, with Lifting.lift_torsor_card load-bearing); the realize_Γ numerator e_Γ(Y) = z_R·#{o_Γ = 0} from the per-source Z¹(R)-torsor decomposition (realizeA_of/realizeQ_of); the assembly of the FourierBranchData p packet (fourierBranchData_of); and the discharge of the target axiom (boundaryFramed_nonterminal_fourier_branch_proven).

• ISOLATED as ONE new §8 bridge axiom (centralCover_realization, strictly more atomic than the target — it takes the §7 block as given and pins W/dimExp/zR to it, asserting only the §8 orbit-combinatorial output): the per-source lift-torsor bijection bijΓ (the exact-image / central-cover orbit decomposition of lem:covertransform, prop:finalfourier, with the Frattini surjectivity R = Φ(K)), the obstruction map o_Γ, the strictly-smaller children, and the source-independent partial-count recipe partialN with its per-source realizations partial_Γ (eq:recursionR2–eq:phasecovertransform). This is the genuine "thousands of lines" of §8 finite/profinite group theory not in mathlib.

• Local-CFT inputs are upstream and unchanged: the local Arf/Gauss-sign type Quadratic.q2_local_base_zeroCount (prop:localzero, the cited local input feeding the zero-edge Gauss sums), Local.q2_local_tate_duality/q2_local_euler_poincare (Tate duality / Euler–Poincaré, feeding the common lift multiplicity z_R and the perfect pairings). These remain the only genuine local arithmetic.

See the closing report for the precise residual sub-lemmas handed to follow-up agents.

Part 1 — The §8 central-cover realization over a minimal block

CoverRealization B is the source-uniform §8 output over a minimal non-scalar block B : MinimalBlock p. It carries exactly the pre-Fourier obstruction realization of prop:finalfourier/lem:properimagesubtraction/lem:phasecover — relative to the block, so the obstruction space W = B.obstructionSpace, the exponent B.dimExp and the lift-torsor size B.zR are inherited (not re-posited). The per-source data is a finite lift index X_Γ, the R-valued obstruction o_Γ : X_Γ → O_R, and the lift-torsor bijection bijΓ of prop:finalfourier; the recipe is the single source-independent partialN with per-source realizations partial_Γ.

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

The §8 central-cover obstruction realization over a minimal block (sec:fourier). Source-uniform: the strictly-smaller children, the source-independent partial-count recipe partialN. Per source Γ: a finite lift index X_Γ, the R-valued obstruction o_Γ : X_Γ → O_R = B.obstructionSpace, the R-cocycle group Z_Γ = Z¹_Γ(R) (|Z_Γ| = z_R) with the per-point R-lift torsors Lift_Γ, and the lift-torsor decomposition bijΓ (prop:finalfourier: boundary-framed surjections onto Y = the disjoint union Σ over the unobstructed exact-image base maps of the z_R-sized R-lift torsor), and the partial-count realization partial_Γ (eq:recursionR2–eq:phasecovertransform). The realize_Γ count equation is derived from bijΓ via Lifting.lift_torsor_card (realizeA_of/realizeQ_of), not stored.

• children : List FramedPair

  The strictly-smaller exact-image children targets (lem:strictdecrease).

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

  Strict decrease of the marked 2-kernel (lem:strictdecrease, eq:Mdescent/ eq:properweighteddescent/eq:phasecoverdescent).

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

  The source-independent partial-count recipe (eq:recursionR2–eq:phasecovertransform, source-independent by cor:sourceinterface).

• XA : Type

  Candidate-source finite lift index.

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

  Candidate-source R-valued obstruction o_{Γ_A} : X_{Γ_A} → O_R.

• XQ : Type

  Local-source finite lift index.

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

  Local-source R-valued obstruction o_{G_{ℚ₂}} : X_{G_{ℚ₂}} → O_R.

• ZA : Type

  Candidate R-cocycle group Z¹_{Γ_A,ρ}(R), of cardinality z_R (lem:affinelifting, eq:mumultiplicity; prop:defduality gives the common |Z¹(R)|).

• agZA : AddGroup self.ZA
• zcardA : Nat.card self.ZA = B.zR
• LiftA : { x : self.XA // self.oA x = 0 } → Type

  Per unobstructed candidate base map, the R-lift set — a Z¹_{Γ_A}(R)-torsor (lem:affinelifting: a nonempty lift set is a Z¹(R)-torsor).

• 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 (prop:finalfourier, the proof of eq:recursionR1): the boundary-framed surjections onto Y are the disjoint union, over the unobstructed exact-image base maps, of the size-z_R R-lift torsor. Every such lift is automatically surjective onto Y since R = Φ(K) is the Frattini subgroup.

• ZQ : Type

  Local R-cocycle group Z¹_{G_{ℚ₂},ρ}(R), of cardinality z_R — equal to the candidate value by cor:sourceinterface(i) (prop:localduality/q2_local_Z1_dim).

• agZQ : AddGroup self.ZQ
• zcardQ : Nat.card self.ZQ = B.zR
• LiftQ : { x : self.XQ // self.oQ x = 0 } → Type

  Per unobstructed local base map, the R-lift set — a Z¹_{G_{ℚ₂}}(R)-torsor.

• 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 (prop:finalfourier).

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

  Candidate partial-count realization m_{Γ_A,χ}(B) = partialN χ (children counts) (eq:recursionR2–eq:phasecovertransform).

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

  Local partial-count realization m_{G_{ℚ₂},χ}(B) = partialN χ (children counts).

theorem Q2Presentation.Induction.framedCount_eq_zR_of_torsorDecomp {S U : Type} [Finite U] (z : ℕ) (Z : Type) [AddGroup Z] (hZ : Nat.card Z = z) (Lift : U → Type) [(u : U) → AddTorsor Z (Lift u)] [∀ (u : U), Finite (Lift u)] (e : S ≃ (u : U) × Lift u) : Nat.card S = z * Nat.card U

The lift-torsor count mechanism, with Lifting/Duality.lean scaffolding load-bearing (lem:affinelifting, eq:mumultiplicity; prop:finalfourier, the proof of eq:recursionR1). If a finite set S of objects (the boundary-framed surjections onto Y) decomposes as the disjoint union, over a finite index U (the unobstructed exact-image base maps {x : X_Γ // o_Γ x = 0}), of per-point lift sets Lift u — each a torsor under a fixed R-cocycle group Z = Z¹_{Γ,ρ}(R) of cardinality z_R (Lifting.lift_torsor_card: a nonempty lift set is a Z¹(R)-torsor) — then #S = z_R · #U. This is the genuine realize_Γ numerator of prop:finalfourier, with Lifting.lift_torsor_card doing the work. It is applied per source in realizeA_of/realizeQ_of to the candidate/local decompositions bijA/bijQ (over ZA/LiftA, ZQ/LiftQ), the common size |Z¹(R)| = z_R being prop:defduality/prop:localduality, equal for the two sources by cor:sourceinterface(i).

theorem Q2Presentation.Induction.CoverRealization.realizeA_of {p : FramedPair} {B : MinimalBlock p} (R : CoverRealization B) : framedCountA p = ↑(B.zR * Nat.card { x : R.XA // R.oA x = 0 })

realize_{Γ_A} is PROVEN (prop:finalfourier, eq:recursionR1 numerator): e_{Γ_A}(Y) = z_R · #{x : o_{Γ_A} x = 0}, by the lift-torsor mechanism framedCount_eq_zR_of_torsorDecomp applied to the candidate decomposition bijA — the z_R factor is Lifting.lift_torsor_card (each unobstructed map has a Z¹_A(R)-torsor of z_R lifts). Genuinely uses the Lifting/Duality.lean scaffolding.

theorem Q2Presentation.Induction.CoverRealization.realizeQ_of {p : FramedPair} {B : MinimalBlock p} (R : CoverRealization B) : framedCountQ p = ↑(B.zR * Nat.card { x : R.XQ // R.oQ x = 0 })

realize_{G_{ℚ₂}} is PROVEN (prop:finalfourier): e_{G_{ℚ₂}}(Y) = z_R · #{o_Q = 0}, by the lift-torsor mechanism applied to the local decomposition bijQ (the Z¹_Q(R)-torsor of z_R lifts, Lifting.lift_torsor_card).

Part 2 — Assembling the FourierBranchData packet

From the §7 block (W/dimExp/zR/hzR) and the §8 realization (children/partialN/X_Γ/o_Γ

• the proven realize_Γ), we build the FourierBranchData p packet that Recursion.fourier_recursion_step consumes.

def Q2Presentation.Induction.fourierBranchData_of {p : FramedPair} (B : MinimalBlock p) (R : CoverRealization B) : FourierBranchData p

The FourierBranchData p packet, assembled from a minimal block B and its §8 central-cover realization R. The obstruction space W, exponent dimExp and size zR are the block's (hzR is B.zR_eq_fintype); the count equations realize_Γ are the proven realizeA_of/realizeQ_of.

Equations

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

Part 3 — The §8 bridge axiom and the discharge of the target

axiom Q2Presentation.Induction.centralCover_realization {p : FramedPair} (B : MinimalBlock p) : Nonempty (CoverRealization B)

AXIOM (the §8 central-cover realization bridge, sec:fourier). Over a minimal non-scalar block B : MinimalBlock p, the §8 central-cover machinery produces an obstruction realization CoverRealization B. This isolates only the §8 orbit-combinatorial output, strictly more atomic than the target axiom boundaryFramed_nonterminal_fourier_branch: it takes the §7 block as given (so it does not re-assert block existence) and pins the obstruction space, exponent and lift size to the block's W = B.obstructionSpace, B.dimExp, B.zR. It asserts the per-source lift-torsor bijection bijΓ (the exact-image / central-cover orbit decomposition of lem:covertransform, prop:finalfourier, with the Frattini surjectivity R = Φ(K)), the strictly-smaller children, and the source-independent partial-count recipe partialN with its per-source realizations (eq:recursionR2–eq:phasecovertransform). It does not assert the post-Fourier recursion equations — those are proven from it via the (already proven) fourier_recursion_step. To be discharged by future formalization of the sec:fourier group theory; its source-independence is cor:sourceinterface (see the SourceInterface section). Neither vacuous nor self-contradictory: it asserts the existence of the manuscript's genuine §8 data (the manuscript constructs it), with no free parameter forced into a contradiction.

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_proven (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

THE DELIVERABLE — boundaryFramed_nonterminal_fourier_branch proved as a theorem. The exact statement of the axiom Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch, now a theorem whose axiom closure does not contain that axiom. A non-terminal target admits a minimal non-scalar block (minimalBlock_of_nonScalar, §7); the §8 central-cover machinery realizes its obstruction (centralCover_realization); the packet is then assembled and the realize_Γ count equations PROVEN (fourierBranchData_of).

Source interface — the comparison theorems justifying source-independence

The single source-independent recipe partialN (shared by partialA and partialQ) is cor:sourceinterface: every ingredient of the §8 transform coincides for the two sources. We record the corresponding already-proved comparison theorems, exactly as Induction/CountsEqual.lean does, to make explicit which results carry the source-independence of the §8 realization:

• (i) lift multiplicities — the size-z_R lift torsor is the same for both sources (Lifting.lift_torsor_card; Local.q2_local_Z1_dim/q2_local_euler_poincare for the local |Z¹|);
• (ii) perfect pairings / adjoint connecting maps — Lifting.isAdjointBoundary_unique;
• (iv) base determinant Gauss sums — Quadratic.candidate_gauss_eq_local_gauss, Quadratic.candidate_numZeros_eq_local.

Acceptance checks

Report — the precise decomposition of boundaryFramed_nonterminal_fourier_branch

boundaryFramed_nonterminal_fourier_branch_proven has exactly the statement of the axiom Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch, and its axiom closure does not contain that axiom. The monolith is replaced by:

PROVEN here, sorry-free:

• framedCount_eq_zR_of_torsorDecomp — the lift-torsor count mechanism (the z_R factor of prop:finalfourier), with Lifting.lift_torsor_card load-bearing;
• CoverRealization.realizeA_of/realizeQ_of — the realize_Γ numerator e_Γ(Y) = z_R·#{o_Γ = 0} of prop:finalfourier (eq:recursionR1), from the per-source Z¹(R)-torsor decomposition via the mechanism above (the z_R factor is genuinely derived);
• fourierBranchData_of — the assembly of the FourierBranchData p packet, with W/dimExp/zR/hzR reduced to the §7 MinimalBlock (B.zR_eq_fintype);
• boundaryFramed_nonterminal_fourier_branch_proven — the discharge (block existence ⟹ §8 realization ⟹ assembled packet).

ISOLATED as the single new §8 bridge axiom (more atomic than the target; takes the §7 block as given, pins W/dimExp/zR, asserts only the §8 orbit output):

• centralCover_realization — the per-source lift-torsor bijection bijΓ (the central-cover exact-image orbit decomposition lem:covertransform/prop:finalfourier, Frattini surjectivity R = Φ(K)), the obstruction o_Γ, the strictly-smaller children, and the source-independent partialN/partial_Γ (eq:recursionR2–eq:phasecovertransform).

Precise remaining sub-lemmas for follow-up agents (to discharge centralCover_realization):

1. lem:covertransform (eq:covertransform): the eight-lift central-cover exact-image partition 8·u_Γ(p,J) = Σ e_Γ(J̃), and lem:commonscalars (|Hom(Γ,𝔽₂)| = 8).
2. prop:finalfourier (eq:recursionR1): the lift-torsor bijection bijΓ — for an unobstructed exact-image map to B the R-lifts are a torsor of size z_R (lem:affinelifting, Lifting.lift_torsor_card) and all surjective onto Y (R = Φ(K)). This is the irreducible bridge from boundaryFramedSurj to o_Γ.
3. lem:properimagesubtraction (eq:recursionR2/eq:recursionR3), prop:nonzeroedge (eq:recursionR4a), prop:zeroedge (eq:recursionR4b, via lem:constrainedgauss + prop:phaseidentity), lem:phasecover (eq:recursionR5a/eq:phasecovertransform): the source-independent partialN recipe and its per-source realizations partial_Γ.
4. cor:sourceinterface: the source-independence of partialN, via the comparison theorems recorded in the SourceInterface section (already proven elsewhere).
5. The local Arf/Gauss-sign type input feeding the zero-edge case remains the documented local-CFT axiom Quadratic.q2_local_base_zeroCount (prop:localzero).

No new local-CFT axiom is introduced here: the §8 bridge is group-theoretic/combinatorial, and the only genuine local arithmetic it relies on is the pre-existing q2_local_base_zeroCount (local Arf type) and q2_local_tate_duality/q2_local_euler_poincare (common lift multiplicity / perfect pairings).