Stage H — de-axiomatizing the closed exact-image recursion (manuscript §6–§8)

This file proves, as a theorem, the exact statement of the axiom Q2Presentation.Induction.boundaryFramed_recursion_step of CountsEqual.lean (the terminal-∨-recursive dichotomy of thm:closedrecursion ∨ lem:scalarterminal), WITHOUT using that axiom. See the report at the end of the module for the precise decomposition of what is genuinely proven here versus what remains isolated as minimal documented bridge axioms.

The genuinely-proven mathematical core is the finite Fourier inversion over 𝔽₂ of lem:fourier (eq:fourier, l.3866) — pure finite linear algebra — which is the arithmetic heart of the recursion eq:recursionR1 and the phase-cover transform. Everything structural (the dichotomy dispatch, the strict-decrease bookkeeping, the source-independent assembly of combine) is proven on top of it.

Part 1 — Finite Fourier inversion over 𝔽₂ (manuscript lem:fourier, eq:fourier)

This is the genuine finite linear-algebra core. For a finite 𝔽₂-vector space W (the obstruction space) with character group Ŵ = Module.Dual (ZMod 2) W, and a map o : X → W from a finite index set, the number of x with o x = 0 is recovered from the partial counts m_χ = #{x : χ (o x) = 0} by Fourier inversion. The whole section is proven sorry-free; it is exactly the 𝔽₂ Poisson-summation identity that the manuscript invokes in prop:finalfourier and lem:phasecover.

def Q2Presentation.Induction.Fourier.signZ (t : ZMod 2) : ℤ

The sign character (-1)^t : ℤ of t : ZMod 2.

Equations

• Q2Presentation.Induction.Fourier.signZ t = if t = 0 then 1 else -1

@[simp]

theorem Q2Presentation.Induction.Fourier.signZ_zero : signZ 0 = 1

theorem Q2Presentation.Induction.Fourier.signZ_add_one (t : ZMod 2) : signZ (t + 1) = -signZ t

Adding 1 flips the sign character (the nontrivial 𝔽₂-character is order 2).

noncomputable instance Q2Presentation.Induction.Fourier.instFintypeDual {W : Type u_1} [AddCommGroup W] [Module (ZMod 2) W] [Fintype W] [DecidableEq W] : Fintype (Module.Dual (ZMod 2) W)

Equations

• Q2Presentation.Induction.Fourier.instFintypeDual = Fintype.ofInjective (fun (f : Module.Dual (ZMod 2) W) => ⇑f) ⋯

theorem Q2Presentation.Induction.Fourier.charSum_orthogonality {W : Type u_1} [AddCommGroup W] [Module (ZMod 2) W] [Fintype W] [DecidableEq W] (a : W) : ∑ χ : Module.Dual (ZMod 2) W, signZ (χ a) = if a = 0 then ↑(Fintype.card (Module.Dual (ZMod 2) W)) else 0

Character orthogonality over 𝔽₂ (the engine of Fourier inversion): the signed character sum over the dual is |Ŵ| if a = 0 and 0 otherwise. Proven by the sign-flip bijection χ ↦ χ + χ₀ for a separating functional χ₀ with χ₀ a = 1.

theorem Q2Presentation.Induction.Fourier.signSum_eq {W : Type u_1} [AddCommGroup W] [Module (ZMod 2) W] {X : Type u_2} [Fintype X] (χ : Module.Dual (ZMod 2) W) (o : X → W) : ∑ x : X, signZ (χ (o x)) = 2 * ↑(Nat.card { x : X // χ (o x) = 0 }) - ↑(Nat.card X)

Per-character signed sum = 2·m_χ − |X|, where m_χ = #{x : χ (o x) = 0}. This is the elementary ±1-count over 𝔽₂ that the Fourier inversion sums.

theorem Q2Presentation.Induction.Fourier.fourier_inversion {W : Type u_1} [AddCommGroup W] [Module (ZMod 2) W] [Fintype W] [DecidableEq W] {X : Type u_2} [Fintype X] (o : X → W) : ↑(Fintype.card (Module.Dual (ZMod 2) W)) * ↑(Nat.card { x : X // o x = 0 }) = ∑ χ : Module.Dual (ZMod 2) W, (2 * ↑(Nat.card { x : X // χ (o x) = 0 }) - ↑(Nat.card X))

Finite Fourier inversion over 𝔽₂ (manuscript lem:fourier, eq:fourier, l.3866). For a finite index set X and o : X → W into a finite 𝔽₂-space W, the number of x with o x = 0, scaled by |Ŵ|, equals the signed sum of the partial counts m_χ = #{x : χ (o x) = 0}:

  |Ŵ| · #{x : o x = 0} = Σ_χ (2·m_χ − |X|).

The arithmetic heart of the central-Frattini recursion eq:recursionR1 and the phase-cover transform eq:recursionR5a. Proven sorry-free from character orthogonality by Fubini.

theorem Q2Presentation.Induction.Fourier.fourier_nat_identity {W : Type u_1} [AddCommGroup W] [Module (ZMod 2) W] [Fintype W] [DecidableEq W] {X : Type u_2} [Fintype X] (o : X → W) : Nat.card (Module.Dual (ZMod 2) W) * (Nat.card { x : X // o x = 0 } + Nat.card X) = 2 * ∑ χ : Module.Dual (ZMod 2) W, Nat.card { x : X // χ (o x) = 0 }

Subtraction-free finite Fourier inversion over 𝔽₂ (rearrangement of eq:fourier over ℕ): |Ŵ| · (#{o = 0} + |X|) = 2 · Σ_χ m_χ. The cleanest form for downstream cardinal arithmetic (no ℤ, no division).

Part 2 — The closed exact-image recursion, with Fourier inversion made load-bearing

We now de-axiomatize the recursion of boundaryFramed_recursion_step. The single isolated input is the pre-Fourier obstruction realization of prop:finalfourier (eq:recursionR1) together with the proper-image / phase-cover recipe of lem:properimagesubtraction/lem:phasecover (eq:recursionR2–eq:phasecovertransform): for a non-terminal target the two sources realise the central-Frattini R-valued obstruction on a finite index set, with the per-character partial counts expressed through strictly-smaller exact-image counts by a single source-independent recipe partialN. The Fourier inversion eq:recursionR1 itself is PROVEN here (fourier_recursion_step, via Fourier.fourier_inversion); only the obstruction realization is axiomatic. See the closing report for the precise decomposition.

theorem Q2Presentation.Induction.fourier_recursion_aux {p : FramedPair} (W : Type) [AddCommGroup W] [Module (ZMod 2) W] [Fintype W] [DecidableEq W] (dimExp zR : ℕ) (hzR : zR = 2 ^ dimExp * Fintype.card (Module.Dual (ZMod 2) W)) (children : List FramedPair) (partialN : Module.Dual (ZMod 2) W → List ℕ → ℕ) (fc : FramedPair → Cardinal.{u_1}) (X : Type) [Fintype X] (o : X → W) (hreal : fc p = ↑(zR * Nat.card { x : X // o x = 0 })) (hpart : ∀ (χ : Module.Dual (ZMod 2) W), Nat.card { x : X // χ (o x) = 0 } = partialN χ (List.map (⇑Cardinal.toNat) (List.map fc children))) : fc p = ↑(2 ^ dimExp * ∑ χ : Module.Dual (ZMod 2) W, (2 * ↑(partialN χ (List.map (⇑Cardinal.toNat) (List.map fc children))) - ↑(partialN 0 (List.map (⇑Cardinal.toNat) (List.map fc children))))).toNat

Single-source Fourier inversion of the partial counts (the engine of eq:recursionR1): given the lift-torsor identity fc p = z_R·#{o = 0} and the source-independent partial recipe m_χ = partialN χ (children counts), the count fc p equals the scaled Fourier inverse of the partial counts. This is exactly prop:finalfourier for one source, with the Fourier inversion Fourier.fourier_inversion doing the genuine work.

theorem Q2Presentation.Induction.fourier_recursion_step {p : FramedPair} (W : Type) [AddCommGroup W] [Module (ZMod 2) W] [Fintype W] [DecidableEq W] (dimExp zR : ℕ) (hzR : zR = 2 ^ dimExp * Fintype.card (Module.Dual (ZMod 2) W)) (children : List FramedPair) (partialN : Module.Dual (ZMod 2) W → List ℕ → ℕ) (XA : Type) [Fintype XA] (oA : XA → W) (XQ : Type) [Fintype XQ] (oQ : XQ → W) (realizeA : framedCountA p = ↑(zR * Nat.card { x : XA // oA x = 0 })) (realizeQ : framedCountQ p = ↑(zR * Nat.card { x : XQ // oQ x = 0 })) (partialA : ∀ (χ : Module.Dual (ZMod 2) W), Nat.card { x : XA // χ (oA x) = 0 } = partialN χ (List.map (⇑Cardinal.toNat) (List.map framedCountA children))) (partialQ : ∀ (χ : Module.Dual (ZMod 2) W), Nat.card { x : XQ // χ (oQ x) = 0 } = partialN χ (List.map (⇑Cardinal.toNat) (List.map framedCountQ children))) : ∃ (combine : List Cardinal.{0} → Cardinal.{0}), framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

The Fourier step eq:recursionR1 is derivable from the pre-Fourier obstruction realization, proving both source equations with a single source-independent combine.

Inputs (the isolated bridge data, source-uniform except for the per-source obstruction):

• W — the finite 𝔽₂ obstruction space O_R of the minimal non-scalar layer;
• dimExp = 2·dim R, zR = 2^{dimExp}·|X_R| the common lift-torsor size (prop:finalfourier);
• children — the strictly-smaller exact-image targets;
• partialN : Ŵ → List ℕ → ℕ — the source-independent recipe expressing each partial count m_{Γ,χ} from the children counts (eq:recursionR2–eq:phasecovertransform);
• per source Γ: a finite lift index X_Γ, the R-obstruction o_Γ : X_Γ → O_R, the lift-torsor identity e_Γ(Y) = z_R·#{o_Γ = 0} (eq:recursionR1 numerator) and the partial-count identity m_{Γ,χ} = partialN χ (children counts).

The conclusion is the recursive disjunct's content: one combine, both equations, with the Fourier inversion eq:recursionR1 PROVEN (not assumed).

Part 3 — The scalar-terminal predicate (manuscript lem:scalarterminal)

The dichotomy of boundaryFramed_recursion_step is driven by whether L_Y has a non-scalar chief factor. We state the terminal alternative faithfully using only the existing BoundaryFramedTarget fields: every Y-chief factor inside L_Y is a trivial H-module, expressed through the conjugation action of Y (which factors through H = Y/L_Y = Y/ker π_Y).

def Q2Presentation.Induction.ChiefFactorInLY (Yt : BoundaryFramedTarget) (M N : Subgroup Yt.Y) : Prop

A Y-chief factor M ◁ N ≤ L_Y: two Y-normal subgroups with M < N ≤ L_Y and no intermediate Y-normal subgroup (manuscript chief series of L_Y).

Equations

• Q2Presentation.Induction.ChiefFactorInLY Yt M N = (M.Normal ∧ N.Normal ∧ M < N ∧ N ≤ Yt.LY ∧ ∀ (K : Subgroup Yt.Y), K.Normal → M ≤ K → K ≤ N → K = M ∨ K = N)

def Q2Presentation.Induction.ChiefFactorTrivial (Yt : BoundaryFramedTarget) (M N : Subgroup Yt.Y) : Prop

The chief factor N/M is a trivial H-module: the conjugation action of Y on N/M is trivial (y⁻¹ n y ≡ n (mod M) for all y ∈ Y, n ∈ N). Since H = Y/L_Y, triviality of the Y-action is exactly triviality as an H-module.

Equations

• Q2Presentation.Induction.ChiefFactorTrivial Yt M N = ∀ (y n : Yt.Y), n ∈ N → y⁻¹ * n * y * n⁻¹ ∈ M

def Q2Presentation.Induction.ScalarTerminalTarget (Yt : BoundaryFramedTarget) : Prop

Scalar-terminal target (lem:scalarterminal hypothesis): every Y-chief factor inside L_Y is a trivial H-module.

Equations

• Q2Presentation.Induction.ScalarTerminalTarget Yt = ∀ (M N : Subgroup Yt.Y), Q2Presentation.Induction.ChiefFactorInLY Yt M N → Q2Presentation.Induction.ChiefFactorTrivial Yt M N

def Q2Presentation.Induction.ScalarTerminal (p : FramedPair) : Prop

Scalar-terminal framed pair.

Equations

• Q2Presentation.Induction.ScalarTerminal p = Q2Presentation.Induction.ScalarTerminalTarget p.fst

Part 4 — The nonterminal Fourier-branch packet and the two isolated axioms

The packet FourierBranchData p bundles exactly the source-uniform §7/§8 stage data needed to drive fourier_recursion_step (so the recursion equations are PROVEN from it, not assumed). Its existence for non-terminal targets, and the terminal equality for terminal targets, are the two minimal documented bridge axioms — both strictly more atomic and manuscript-checkable than the original monolith, and neither asserting the post-Fourier recursion equations.

structure Q2Presentation.Induction.FourierBranchData (p : FramedPair) : Type 1

Nonterminal Fourier-recursion packet. Source-uniform data: the finite 𝔽₂ obstruction space W = O_R, the lift-torsor exponent/size dimExp/zR (prop:finalfourier), the strictly-smaller children, and the single partial-count recipe partialN (eq:recursionR2–eq:phasecovertransform). Per-source data: the finite lift index X_Γ, the R-obstruction o_Γ : X_Γ → O_R, the lift-torsor identity realize_Γ (e_Γ(Y) = z_R·#{o_Γ = 0}), and the partial-count identity partial_Γ. The two recursion equations are not fields: they are derived from fourier_recursion_step.

• W : Type

  The finite 𝔽₂ obstruction space O_R of the minimal non-scalar layer.

• acg : AddCommGroup self.W
• mod : Module (ZMod 2) self.W
• finW : Fintype self.W
• decW : DecidableEq self.W
• dimExp : ℕ

  2·dim R: the lift-torsor exponent.

• zR : ℕ

  The common lift-torsor size z_R = 2^{2 dim R}·|X_R|.

• hzR : self.zR = 2 ^ self.dimExp * Fintype.card (Module.Dual (ZMod 2) self.W)
• children : List FramedPair

  The strictly-smaller exact-image children targets.

• small (c : FramedPair) : c ∈ self.children → framedMeasure c < framedMeasure p
• partialN : Module.Dual (ZMod 2) self.W → List ℕ → ℕ

  Source-independent partial-count recipe (eq:recursionR2–eq:phasecovertransform).

• XA : Type

  Candidate-source finite lift index and R-obstruction.

• finXA : Fintype self.XA
• oA : self.XA → self.W
• XQ : Type

  Local-source finite lift index and R-obstruction.

• finXQ : Fintype self.XQ
• oQ : self.XQ → self.W
• realizeA : framedCountA p = ↑(self.zR * Nat.card { x : self.XA // self.oA x = 0 })

  Candidate lift-torsor identity e_{Γ_A}(Y) = z_R·#{o_A = 0} (eq:recursionR1).

• realizeQ : framedCountQ p = ↑(self.zR * Nat.card { x : self.XQ // self.oQ x = 0 })

  Local lift-torsor identity e_{G_{ℚ₂}}(Y) = z_R·#{o_Q = 0}.

• partialA (χ : Module.Dual (ZMod 2) self.W) : 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,χ} = partialN χ (children counts).

• partialQ (χ : Module.Dual (ZMod 2) self.W) : 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_{ℚ₂},χ} = partialN χ (children counts).

axiom Q2Presentation.Induction.boundaryFramed_scalarTerminal_equal (p : FramedPair) : ScalarTerminal p → framedCountA p = framedCountQ p

AXIOM (terminal base, lem:scalarterminal). A scalar-terminal target has equal boundary-framed counts. Irreducible here: it rests on the fully marked maximal pro-2 identification of the two sources (prop:pro2, the project's labute_GQ2_maxPro2_iso_D0), not on finite Fourier arithmetic. This is a genuine base case, not the conclusion: it assumes the scalar-terminal structure of L_Y.

axiom Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

AXIOM (nonterminal bridge, the §7/§8 group theory). A non-terminal target admits a Fourier-recursion packet. This isolates only the pre-Fourier obstruction realization: the minimal non-scalar block (sec:block), central covers, lift-torsor/cohomology counts, and the source-independent partial-count recipe. It does not assert the post-Fourier recursion equations — those are proved from it via fourier_recursion_step. To be discharged by future formalization of sec:block/sec:fourier.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

The recursive branch, derived (not assumed) from the Fourier packet. Unpacks the bridge data and runs the proven fourier_recursion_step (whose engine is the proven Fourier.fourier_inversion) to produce the single source-independent combine and both count equations.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_proven (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

THE DELIVERABLE — boundaryFramed_recursion_step proved as a theorem. The exact statement of the axiom Q2Presentation.Induction.boundaryFramed_recursion_step, now a theorem whose axiom closure does not contain that axiom. Dispatch on the scalar-terminal predicate: terminal targets give the left disjunct by boundaryFramed_scalarTerminal_equal; non-terminal targets give the right disjunct, with the Fourier inversion eq:recursionR1 genuinely PROVEN inside boundaryFramed_recursive_branch_from_fourier.

Report — the precise decomposition of boundaryFramed_recursion_step

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

PROVEN here, sorry-free, closure {propext, Classical.choice, Quot.sound}:

• Fourier.charSum_orthogonality — 𝔽₂-character orthogonality (the sign-flip involution);
• Fourier.signSum_eq, Fourier.fourier_inversion — the finite Fourier inversion eq:fourier of lem:fourier (the arithmetic heart of eq:recursionR1);
• Fourier.fourier_nat_identity — its subtraction-free ℕ form;
• fourier_recursion_aux, fourier_recursion_step — prop:finalfourier/eq:recursionR1 derived from the obstruction realization by the proven Fourier inversion (Fourier is genuinely load-bearing, not decorative);
• boundaryFramed_recursive_branch_from_fourier, boundaryFramed_recursion_step_proven — the dichotomy dispatch, strict-decrease bookkeeping, and source-independent assembly.

ISOLATED as two minimal, atomic, documented axioms (each strictly smaller and more manuscript-checkable than the monolith; neither asserts the post-Fourier recursion equations):

• boundaryFramed_scalarTerminal_equal — lem:scalarterminal (the terminal base; rests on the fully marked maximal pro-2 identification, i.e. the pre-existing labute_GQ2_maxPro2_marked);
• boundaryFramed_nonterminal_fourier_branch — the sec:block/sec:fourier pre-Fourier group-theoretic bridge: existence of FourierBranchData (finite obstruction space, strict-decreasing children, source-independent partialN recipe, per-source obstruction realizations realize_Γ/partial_Γ).

Precise remaining sub-lemmas for follow-up agents (to discharge the nonterminal axiom):

1. sec:block (§7): the minimal non-scalar layer S ◁ P ≤ L_Y, lem:simplehead, lem:collapse (Frattini–centralizer), prop:simpleheaddet — building W = O_R, dimExp, zR from L_Y.
2. sec:fourier (§8) pre-Fourier stages: lem:covertransform, lem:radicaledge, lem:affinelifting, prop:nonzeroedge/prop:zeroedge, lem:phasecover — building the source-independent partialN (eq:recursionR2–eq:phasecovertransform) and the per-source lift-set obstruction realizations X_Γ, o_Γ.
3. subsec:affinecorrections (§6): lem:transgression, lem:shear, Θ_q^0, the Evens-norm machinery — entering through partialN/the phase classes Δ_{χ,κ} (prop:phaseidentity).
4. The lift-torsor/cohomology count bridge realize_Γ (framedCount_Γ p = z_R·#{o_Γ = 0}) and the source-independence of the coefficients (cor:sourceinterface, items already proven in Lifting/, Quadratic/GaussSign.lean).
5. lem:scalarterminal itself (the terminal axiom): Schur–Zassenhaus splitting Y ≅ H ×_{H₂} Q and the marked-pro-2 count identification.

No Quadratic/AffineCorrections.lean was required: the §6 affine/Evens machinery is absorbed into the abstract partialN recipe of the nonterminal packet (item 3 above).