9. Central covers, affine fibres, and Fourier inversion🔗

Lemma9.1

Group: Central covers, affine fibres, and Fourier inversion (7)

Group member previews

Preview

Lemma 9.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Lemma 8.2 of the paper (Common scalar character group).

For both sources \Gamma\in\{\GA,\GQ\} one has

|\Hom_{\mathrm{cont}}(\Gamma,\F_2)|=8.

Moreover scalar twisting by any such character preserves the boundary-framed condition for the central double covers used below.

Lean code for Lemma9.1●2 theorems

theoremdefined in GQ2/SectionEight/ScalarCount.lean

complete

theorem GQ2.SectionEight.lemma_8_2_gammaA :
  Nat.card (↑GQ2.GammaA.toProfinite.toTop →ₜ* Multiplicative (ZMod 2)) =
    8

theorem GQ2.SectionEight.lemma_8_2_gammaA :
  Nat.card
      (↑GQ2.GammaA.toProfinite.toTop →ₜ*
        Multiplicative (ZMod 2)) =
    8

**Lemma 8.2, candidate source**: `|Hom_cont(Γ_A, 𝔽₂)| = 8`.  **Proved** over the
the admissible-limit proof/Prop. 2.3 layer: characters of `Γ_A` are `F₄`-generator values killing `N_A`
(`charEquiv`/`cmhEquivFun`), and killing `N_A` is exactly killing `τ`
(`ker_char_NA_le_iff` — the tame relator forces it, and conversely `c(τ) = 1` gives both
relations in exponent-2 abelian quotients, `Marking.wildRel_of_comm2`).  That leaves the free
`𝔽₂³` of `σ, x₀, x₁`-values.

theoremdefined in GQ2/SectionEight/ScalarCount.lean

complete

theorem GQ2.SectionEight.lemma_8_2_local (B : GQ2.BoundaryMaps)
  [CompactSpace GQ2.AbsGalQ2] [TotallyDisconnectedSpace GQ2.AbsGalQ2] :
  Nat.card (GQ2.AbsGalQ2 →ₜ* Multiplicative (ZMod 2)) = 8

theorem GQ2.SectionEight.lemma_8_2_local
  (B : GQ2.BoundaryMaps)
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace
      GQ2.AbsGalQ2] :
  Nat.card
      (GQ2.AbsGalQ2 →ₜ*
        Multiplicative (ZMod 2)) =
    8

**Lemma 8.2, local source**: `|Hom_cont(G_ℚ₂, 𝔽₂)| = 8` (`= |ℚ₂ˣ/(ℚ₂ˣ)²|`).  **Proved**
via the common marked maximal pro-2 quotient: a `BoundaryMaps` witness pins `pro2F` as *the*
maximal pro-2 quotient map (`ker_pro2F`), every `𝔽₂`-character kills the pro-2 kernel
(the maximal pro-p quotient API `proPKernel_le_ker`), so precomposition with `pro2F` bijects characters of `Π` with
characters of `G_ℚ₂`, and `card_char_piBd` finishes.  [Statement amendment (F-owner): the
`BoundaryMaps` hypothesis and the `CompactSpace`/`TotallyDisconnectedSpace` instance
hypotheses on `AbsGalQ2` (the `main_presentation` house pattern) — without the bundle the
count is B4/B5-content outside the §8 proof layer axiom budget.]

Lemma9.2

Group: Central covers, affine fibres, and Fourier inversion (7)

Group member previews

Preview

Lemma 9.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Lemma 8.3 of the paper (Central-cover exact-image transform).

Let \mathcal Y=(Y,L_Y,\pi_Y,\theta_Y) be boundary-framed and let

p:\widetilde Y\twoheadrightarrow Y

be a central double cover. Give it the pulled-back structure

\widetilde L=p^{-1}(L_Y), \qquad \widetilde\pi=\pi_Yp, \qquad \widetilde\theta=\theta_Yp,

and assume the central kernel lies in \ker(\widetilde\pi,\widetilde\theta). Fix an exact-image subgroup J\le Y projecting onto H. If u_\Gamma^\beta(p,J) counts boundary-framed exact-image maps to J whose pullback cover is split, then

8u_\Gamma^\beta(p,J) =\sum_{\substack{\widetilde J\le p^{-1}(J)\\p(\widetilde J)=J}} e_\Gamma^\beta(\widetilde J,\widetilde J\cap\widetilde L, \widetilde\pi|_{\widetilde J}, \widetilde\theta|_{\widetilde J}).

Every term on the right is therefore an ordinary exact-image object in the same global boundary-framed category.

Lean code for Lemma9.2●1 theorem

theoremdefined in GQ2/SectionEight/Partition.lean

complete

theorem GQ2.SectionEight.lemma_8_3 {H E : Type} [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ]
  [TopologicalSpace Γ] {Y : Type} [Group Y] [TopologicalSpace Y]
  [DiscreteTopology Y] [Finite Y] [IsTopologicalGroup Γ]
  [CompactSpace Γ] [TotallyDisconnectedSpace Γ]
  (hfg : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (b : Γ →ₜ* ↥GQ2.boundarySubgroup) (F : GQ2.BoundaryFrame H E)
  (T : GQ2.MarkedTarget H E Y) (C : GQ2.SectionEight.CentralCover Y)
  (hscalar : Nat.card (Γ →ₜ* Multiplicative (ZMod 2)) = 8)
  (J : Subgroup Y) (hJ : Function.Surjective ⇑(T.piY.comp J.subtype)) :
  8 * GQ2.SectionEight.liftableCount b F T C J hJ =
    ∑ᶠ (J' : Subgroup C.cover) (_ :
      J' ∈ {J' | Subgroup.map C.p J' = J}),
      GQ2.SectionEight.exactImageCountOn b F (C.pullTarget T) J'

theorem GQ2.SectionEight.lemma_8_3 {H E : Type}
  [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H]
  [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E]
  {Γ : Type} [Group Γ]
  [TopologicalSpace Γ] {Y : Type}
  [Group Y] [TopologicalSpace Y]
  [DiscreteTopology Y] [Finite Y]
  [IsTopologicalGroup Γ] [CompactSpace Γ]
  [TotallyDisconnectedSpace Γ]
  (hfg :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (b : Γ →ₜ* ↥GQ2.boundarySubgroup)
  (F : GQ2.BoundaryFrame H E)
  (T : GQ2.MarkedTarget H E Y)
  (C : GQ2.SectionEight.CentralCover Y)
  (hscalar :
    Nat.card
        (Γ →ₜ* Multiplicative (ZMod 2)) =
      8)
  (J : Subgroup Y)
  (hJ :
    Function.Surjective
      ⇑(T.piY.comp J.subtype)) :
  8 *
      GQ2.SectionEight.liftableCount b F T
        C J hJ =
    ∑ᶠ (J' : Subgroup C.cover) (_ :
      J' ∈
        {J' | Subgroup.map C.p J' = J}),
      GQ2.SectionEight.exactImageCountOn b
        F (C.pullTarget T) J'

**Central-cover exact-image transform.**  For a scalar central cover, eight times the
liftable count over an image subgroup `J` equals the sum of exact-image counts over the subgroups
of the cover mapping onto `J`.  This is the result currently numbered Lemma 8.3 in the paper
(stable paper identifier `lem-covertransform`).

Proof for Lemma 9.2

uses 1

Proved in §8 of the paper. Ingredients: Lemma 9.1.

Lemma9.3

Group: Central covers, affine fibres, and Fourier inversion (7)

Group member previews

Preview

Lemma 9.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Lemma 8.4 of the paper (Fourier inversion).

Let \Lambda be the character group of a finite \F_2-obstruction space and let o:X\to \Lambda^\vee. If

m_\lambda=\#\{x\in X:\langle\lambda,o(x)\rangle=0\},

then

\#\{x:o(x)=0\} =\frac1{|\Lambda|}\sum_{\lambda\in \Lambda}(2m_\lambda-|X|).

Lean code for Lemma9.3●1 theorem

theoremdefined in GQ2/SectionEight/Fourier.lean

complete

theorem GQ2.SectionEight.lemma_8_4.{u_1, u_2} {X : Type u_1} {W : Type u_2}
  [Finite X] [AddCommGroup W] [Module (ZMod 2) W] [Finite W]
  (o : X → W) :
  ↑(Nat.card (Module.Dual (ZMod 2) W)) * ↑(Nat.card { x // o x = 0 }) =
    ∑ᶠ (φ : Module.Dual (ZMod 2) W),
      (2 * ↑(Nat.card { x // φ (o x) = 0 }) - ↑(Nat.card X))

theorem GQ2.SectionEight.lemma_8_4.{u_1, u_2}
  {X : Type u_1} {W : Type u_2} [Finite X]
  [AddCommGroup W] [Module (ZMod 2) W]
  [Finite W] (o : X → W) :
  ↑(Nat.card (Module.Dual (ZMod 2) W)) *
      ↑(Nat.card { x // o x = 0 }) =
    ∑ᶠ (φ : Module.Dual (ZMod 2) W),
      (2 *
          ↑(Nat.card
              { x // φ (o x) = 0 }) -
        ↑(Nat.card X))

**Lemma 8.4 (Fourier inversion, eq. (125))**, multiplied-out integer form: for a finite
`𝔽₂`-obstruction space `W`, an obstruction assignment `o : X → W` on a finite index set, and
`m_φ = #{x ∣ φ(o(x)) = 0}`,
`|W^∨| · #{x ∣ o(x) = 0} = Σ_{φ ∈ W^∨} (2 m_φ − |X|)`.
(Paper form: divide by `|D|`, `D = W^∨`.)  **Proved** — the `𝔽₂`-character engine of the
final `R`-lifting stage (136).

Lemma9.4

Group: Central covers, affine fibres, and Fourier inversion (7)

Group member previews

Preview

Lemma 9.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Lemma 8.5 of the paper (Constrained quadratic Gauss transform).

Let W,E be finite \F_2-vector spaces, let L:W\twoheadrightarrow E, and let Q:W\to\F_2 be nonsingular with polar form b_Q. For \kappa\in E and \epsilon\in\F_2, put

N(\kappa,\epsilon)=\#\{x\in W:Lx=\kappa,\ Q(x)=\epsilon\}.

For \chi\in E^\vee, let a_\chi be uniquely determined by

b_Q(a_\chi,x)=\chi(Lx).

Then

N(\kappa,\epsilon) =\frac1{2|E|}\left( |W|+G(Q)\sum_{\chi\in E^\vee} (-1)^{\chi(\kappa)+\epsilon+Q(a_\chi)} \right),

where G(Q)=\sum_{x\in W}(-1)^{Q(x)}.

Lean code for Lemma9.4●2 theorems

theoremdefined in GQ2/RecursionSplice.lean

complete

theorem GQ2.SectionEight.lemma_8_5_aggregated.{u_1, u_2, u_3} {W : Type u_1}
  {E : Type u_2} [AddCommGroup W] [Module (ZMod 2) W] [Finite W]
  [AddCommGroup E] [Module (ZMod 2) E] [Finite E] (L : W →ₗ[ZMod 2] E)
  (hL : Function.Surjective ⇑L) (Q : W → ZMod 2)
  (a : Module.Dual (ZMod 2) E → W)
  (ha :
    ∀ (χ : Module.Dual (ZMod 2) E) (x : W),
      GQ2.QuadraticFp2.polar Q (a χ) x = χ (L x))
  {I : Type u_3} [Fintype I] (κ : I → E) (ε : I → ZMod 2) :
  2 * ↑(Nat.card (Module.Dual (ZMod 2) E)) *
      ∑ i, ↑(Nat.card { x // L x = κ i ∧ Q x = ε i }) =
    ↑(Fintype.card I) * ↑(Nat.card W) +
      GQ2.SectionEight.gaussSum Q *
        ∑ᶠ (χ : Module.Dual (ZMod 2) E),
          ∑ i, GQ2.SectionEight.sign (χ (κ i) + ε i + Q (a χ))

theorem GQ2.SectionEight.lemma_8_5_aggregated.{u_1,
    u_2, u_3}
  {W : Type u_1} {E : Type u_2}
  [AddCommGroup W] [Module (ZMod 2) W]
  [Finite W] [AddCommGroup E]
  [Module (ZMod 2) E] [Finite E]
  (L : W →ₗ[ZMod 2] E)
  (hL : Function.Surjective ⇑L)
  (Q : W → ZMod 2)
  (a : Module.Dual (ZMod 2) E → W)
  (ha :
    ∀ (χ : Module.Dual (ZMod 2) E)
      (x : W),
      GQ2.QuadraticFp2.polar Q (a χ) x =
        χ (L x))
  {I : Type u_3} [Fintype I] (κ : I → E)
  (ε : I → ZMod 2) :
  2 *
        ↑(Nat.card
            (Module.Dual (ZMod 2) E)) *
      ∑ i,
        ↑(Nat.card
            { x //
              L x = κ i ∧ Q x = ε i }) =
    ↑(Fintype.card I) * ↑(Nat.card W) +
      GQ2.SectionEight.gaussSum Q *
        ∑ᶠ (χ : Module.Dual (ZMod 2) E),
          ∑ i,
            GQ2.SectionEight.sign
              (χ (κ i) + ε i + Q (a χ))

**The aggregated constrained-Gauss identity** (the Prop. 8.9 assembly, `hgauss` level 1): summing the proved
Gauss engine `lemma_8_5` over a finite index family `I` (the `C`-image `ρ`, each with its own
constraint `(κ_i, ε_i)`) and swapping the resulting double sum gives

  `2·|E^∨|·Σ_i N(κ_i,ε_i) = |I|·|W| + G(Q)·Σ_χ Σ_i (−1)^{χκ_i+ε_i+Q(a_χ)}`.

Pure `𝔽₂`-linear algebra — no frame data.  This is the aggregation step of `hgauss`: with the
concrete correspondences `Σ_i N(κ_i,ε_i) = M`, `|I| = e_Γ(C)`, `|W| = |V|`, `|E^∨| = |D_T|`,
`G(Q) = G0`, and the phase reindex `Σ_i sign(χκ_i+ε_i+Q(a_χ)) = 2·nPhase(phase χ) − e_Γ(C)`
(the Prop 8.8 / (135) content coupled to the witness), it becomes the `hgauss` hypothesis of
`phase140_ofPhaseData`.

theoremdefined in GQ2/SectionEight/Fourier.lean

complete

theorem GQ2.SectionEight.lemma_8_5.{u_1, u_2} {W : Type u_1} {E : Type u_2}
  [AddCommGroup W] [Module (ZMod 2) W] [Finite W] [AddCommGroup E]
  [Module (ZMod 2) E] [Finite E] (L : W →ₗ[ZMod 2] E)
  (hL : Function.Surjective ⇑L) (Q : W → ZMod 2)
  (a : Module.Dual (ZMod 2) E → W)
  (ha :
    ∀ (χ : Module.Dual (ZMod 2) E) (x : W),
      GQ2.QuadraticFp2.polar Q (a χ) x = χ (L x))
  (κ : E) (ε : ZMod 2) :
  2 * ↑(Nat.card (Module.Dual (ZMod 2) E)) *
      ↑(Nat.card { x // L x = κ ∧ Q x = ε }) =
    ↑(Nat.card W) +
      GQ2.SectionEight.gaussSum Q *
        ∑ᶠ (χ : Module.Dual (ZMod 2) E),
          GQ2.SectionEight.sign (χ κ + ε + Q (a χ))

theorem GQ2.SectionEight.lemma_8_5.{u_1, u_2}
  {W : Type u_1} {E : Type u_2}
  [AddCommGroup W] [Module (ZMod 2) W]
  [Finite W] [AddCommGroup E]
  [Module (ZMod 2) E] [Finite E]
  (L : W →ₗ[ZMod 2] E)
  (hL : Function.Surjective ⇑L)
  (Q : W → ZMod 2)
  (a : Module.Dual (ZMod 2) E → W)
  (ha :
    ∀ (χ : Module.Dual (ZMod 2) E)
      (x : W),
      GQ2.QuadraticFp2.polar Q (a χ) x =
        χ (L x))
  (κ : E) (ε : ZMod 2) :
  2 *
        ↑(Nat.card
            (Module.Dual (ZMod 2) E)) *
      ↑(Nat.card
          { x // L x = κ ∧ Q x = ε }) =
    ↑(Nat.card W) +
      GQ2.SectionEight.gaussSum Q *
        ∑ᶠ (χ : Module.Dual (ZMod 2) E),
          GQ2.SectionEight.sign
            (χ κ + ε + Q (a χ))

**Lemma 8.5 (constrained quadratic Gauss transform, eq. (126))**, multiplied-out form:
for finite `𝔽₂`-spaces `W, E`, a surjective linear `L : W ↠ E`, a form `Q : W → 𝔽₂` with
polar form `B_Q`, and **data** `a : E^∨ → W` with the paper's defining property
`B_Q(a_χ, x) = χ(L x)` (the paper produces `a_χ` from nonsingularity of `Q`; the identity
needs only the property), the constrained count `N(κ,ε) = #{x ∣ Lx = κ, Q(x) = ε}`
satisfies `2|E^∨| · N(κ,ε) = |W| + G(Q) · Σ_{χ ∈ E^∨} (−1)^{χ(κ)+ε+Q(a_χ)}`.
(`|E^∨| = |E|` for finite `𝔽₂`-spaces, giving the paper's `1/(2|E|)`-form.)
**Proved** — the affine-fibre engine of the (140)-clause of Prop 8.9.

Lemma9.5

Group: Central covers, affine fibres, and Fourier inversion (7)

Group member previews

Preview

Lemma 9.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Lemma 8.6 of the paper (Radical edge, variation formula, and descent).

Let 0\to T\to M\to V\to0 be the simple-head sequence, and let

p:\widetilde B\twoheadrightarrow B

be a central double cover whose restriction to M has quadratic form with polar radical T and whose restriction to T is zero. The cover determines a canonical edge class

[\varepsilon]\in H^1(B/T,T^\vee).

Its restriction to V is zero, so it is inflated from a unique class

[\bar\varepsilon]\in H^1(C,T^\vee).

For every lower exact-image epimorphism \rho:\Gamma\twoheadrightarrow C and every unrestricted M-lift f, twisting by u\in Z^1_{\Gamma,\rho}(T) changes the scalar obstruction by

\operatorname{ob}(f_u)=\operatorname{ob}(f) +\bigl\langle [u],\rho^*[\bar\varepsilon]\bigr\rangle_\Gamma.

If [\bar\varepsilon]\ne0, the free Z^1_{\Gamma,\rho}(T)-action partitions the unrestricted M-lifts into orbits in each of which exactly one half satisfy the central relation. If [\bar\varepsilon]=0, the cover descends to a central double cover of B/T; conversely, descent forces the edge class to vanish.

Lean code for Lemma9.5●5 declarations

theoremdefined in GQ2/HalfTorsorGammaA.lean

complete

theorem GQ2.SectionEight.LedgerGammaA.half_torsor_gammaA {Bg : Type} [Group Bg]
  [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg]
  (D : GQ2.SectionEight.RadicalCoverData Bg) (hedge : D.NoDescent)
  (ρ : ↑GQ2.GammaA.toProfinite.toTop →ₜ* Bg ⧸ D.M)
  (hρ : Function.Surjective ⇑ρ) :
  2 * Nat.card { f // GQ2.SectionEight.MLifts.Central D f } =
    Nat.card (GQ2.SectionEight.MLifts D ρ)

theorem GQ2.SectionEight.LedgerGammaA.half_torsor_gammaA
  {Bg : Type} [Group Bg]
  [TopologicalSpace Bg]
  [DiscreteTopology Bg] [Finite Bg]
  (D :
    GQ2.SectionEight.RadicalCoverData Bg)
  (hedge : D.NoDescent)
  (ρ :
    ↑GQ2.GammaA.toProfinite.toTop →ₜ*
      Bg ⧸ D.M)
  (hρ : Function.Surjective ⇑ρ) :
  2 *
      Nat.card
        { f //
          GQ2.SectionEight.MLifts.Central
            D f } =
    Nat.card (GQ2.SectionEight.MLifts D ρ)

**Lemma 8.6, `Γ_A` source** (the Γ_A half-torsor proof): with a nonzero radical edge, exactly half of the
unrestricted `M`-lifts of a lower epimorphism `ρ : Γ_A ↠ B/M` satisfy the central relation.
The abstract half-count `CentralObstruction.half_count` fed by the nonzero variation class
(`exists_nonzero_varCoc_gammaA`) and `#H² = 2` (`card_H2_gammaA_eq_two`); the counted lift set is
finite because `Γ_A` is topologically finitely generated.

theoremdefined in GQ2/RadicalEdge/Local.lean

complete

theorem GQ2.SectionEight.RadicalEdgeLocal.half_torsor_local {Bg : Type}
  [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg]
  (D : GQ2.SectionEight.RadicalCoverData Bg) [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (hfg : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (hedge : D.NoDescent) (ρ : GQ2.AbsGalQ2 →ₜ* Bg ⧸ D.M)
  (hρ : Function.Surjective ⇑ρ) :
  2 * Nat.card { f // GQ2.SectionEight.MLifts.Central D f } =
    Nat.card (GQ2.SectionEight.MLifts D ρ)

theorem GQ2.SectionEight.RadicalEdgeLocal.half_torsor_local
  {Bg : Type} [Group Bg]
  [TopologicalSpace Bg]
  [DiscreteTopology Bg] [Finite Bg]
  (D :
    GQ2.SectionEight.RadicalCoverData Bg)
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (hfg :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (hedge : D.NoDescent)
  (ρ : GQ2.AbsGalQ2 →ₜ* Bg ⧸ D.M)
  (hρ : Function.Surjective ⇑ρ) :
  2 *
      Nat.card
        { f //
          GQ2.SectionEight.MLifts.Central
            D f } =
    Nat.card (GQ2.SectionEight.MLifts D ρ)

**Lemma 8.6, local source, engine form** — the half-torsor count for `G_ℚ₂` from
`NoDescent`, via B6.  Consumed by `SectionEight.lemma_8_6_local`.

theoremdefined in GQ2/SectionEight/Partition.lean

complete

theorem GQ2.SectionEight.lemma_8_6_gammaA {Bg : Type} [Group Bg]
  [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg]
  (D : GQ2.SectionEight.RadicalCoverData Bg) (hedge : D.NoDescent)
  (ρ : ↑GQ2.GammaA.toProfinite.toTop →ₜ* Bg ⧸ D.M)
  (hρ : Function.Surjective ⇑ρ) :
  2 * Nat.card { f // GQ2.SectionEight.MLifts.Central D f } =
    Nat.card (GQ2.SectionEight.MLifts D ρ)

theorem GQ2.SectionEight.lemma_8_6_gammaA
  {Bg : Type} [Group Bg]
  [TopologicalSpace Bg]
  [DiscreteTopology Bg] [Finite Bg]
  (D :
    GQ2.SectionEight.RadicalCoverData Bg)
  (hedge : D.NoDescent)
  (ρ :
    ↑GQ2.GammaA.toProfinite.toTop →ₜ*
      Bg ⧸ D.M)
  (hρ : Function.Surjective ⇑ρ) :
  2 *
      Nat.card
        { f //
          GQ2.SectionEight.MLifts.Central
            D f } =
    Nat.card (GQ2.SectionEight.MLifts D ρ)

**Lemma 8.6 (half-torsor count), candidate source**: with a nonzero radical edge, for
every lower *epimorphism* `ρ : Γ_A ↠ B/M`, exactly half of the unrestricted `M`-lifts of
`ρ` satisfy the central relation.  (The degree-one duality making the variation functional
(127) nonzero is §5 content for `Γ_A` — B7 enters through 5.15/5.16.)
[the §8 proof layer statement; proof = O-half.]

theoremdefined in GQ2/SectionEight/Partition.lean

complete

theorem GQ2.SectionEight.lemma_8_6_local {Bg : Type} [Group Bg]
  [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg]
  (D : GQ2.SectionEight.RadicalCoverData Bg) [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (hfg : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (hedge : D.NoDescent) (ρ : GQ2.AbsGalQ2 →ₜ* Bg ⧸ D.M)
  (hρ : Function.Surjective ⇑ρ) :
  2 * Nat.card { f // GQ2.SectionEight.MLifts.Central D f } =
    Nat.card (GQ2.SectionEight.MLifts D ρ)

theorem GQ2.SectionEight.lemma_8_6_local
  {Bg : Type} [Group Bg]
  [TopologicalSpace Bg]
  [DiscreteTopology Bg] [Finite Bg]
  (D :
    GQ2.SectionEight.RadicalCoverData Bg)
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (hfg :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (hedge : D.NoDescent)
  (ρ : GQ2.AbsGalQ2 →ₜ* Bg ⧸ D.M)
  (hρ : Function.Surjective ⇑ρ) :
  2 *
      Nat.card
        { f //
          GQ2.SectionEight.MLifts.Central
            D f } =
    Nat.card (GQ2.SectionEight.MLifts D ρ)

**Lemma 8.6 (half-torsor count), local source**: as `lemma_8_6_gammaA`, for `G_ℚ₂`
(degree-one duality = B6).  The standing §8 side conditions are explicit, following
`lemma_8_2_local` (compactness) and `lemma_8_3` (`hfg`
topological finite generation, the B1-shaped input) precedents — they finitize the counted
`MLifts`.  Proof: the central-obstruction framework's central-obstruction engine + the B6 twist of
`GQ2/RadicalEdgeLocal.lean` (`half_torsor_local`).  Ax: B6, B7.

defdefined in GQ2/SectionEight/Recursion.lean

complete

def GQ2.SectionEight.RecursionFrame.Enrichment.radData {H E : Type}
  [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y]
  {T : GQ2.MarkedTarget H E Y}
  {Blk : GQ2.SectionSeven.MinimalBlock T.LY}
  {RF : GQ2.SectionEight.RecursionFrame T Blk} :
  RF.Enrichment →
    (l : RF.DR) →
      (h : l ≠ RF.zeroDR) → GQ2.SectionEight.RadicalCoverData RF.YB

def GQ2.SectionEight.RecursionFrame.Enrichment.radData
  {H E : Type} [Group H] [CommGroup E]
  {Y : Type} [Group Y] [Finite Y]
  {T : GQ2.MarkedTarget H E Y}
  {Blk :
    GQ2.SectionSeven.MinimalBlock T.LY}
  {RF :
    GQ2.SectionEight.RecursionFrame T
      Blk} :
  RF.Enrichment →
    (l : RF.DR) →
      (h : l ≠ RF.zeroDR) →
        GQ2.SectionEight.RadicalCoverData
          RF.YB

The per-`λ` **Lemma 8.6 datum** assembled from the enrichment: cover `p_λ`, layers
`M_B`/`T_B`, with normality and elementarity derived from the frame and the block.

Proof for Lemma 9.5

Proof uses 2

Proof dependency previews

Preview

Proposition 6.8

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §8 of the paper. Ingredients: Lemma 8.1 Proposition 6.8.

Lemma9.6

Group: Central covers, affine fibres, and Fourier inversion (7)

Group member previews

Preview

Lemma 9.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Lemma 8.7 of the paper (Affine T-lifting equation).

Choose the splitting B/T\cong V\rtimes C above and let

e\in H^2(C,T)

be the class obtained by pulling B\to V\rtimes C back along the zero section C\to V\rtimes C. For a lower exact-image map \rho:\Gamma\twoheadrightarrow C, a class

c\in H^1_{\Gamma,\rho}(V)

is the V-coordinate of an actual M-lift if and only if

\partial_{\Gamma,\rho}(c)=\rho^*e \quad\text{in }H^2_{\Gamma,\rho}(T).

For every such class, the number of raw lifts above it is

\mu=|B^1_{\Gamma,\rho}(V)|\,|Z^1_{\Gamma,\rho}(T)|,

which is independent of \rho and has the same value on the two sources.

Lean code for Lemma9.6●1 theorem

theoremdefined in GQ2/AffineTLift.lean

complete

theorem GQ2.SectionEight.AffineTLift.lemma_8_7_count {Bg : Type} [Group Bg]
  [Finite Bg] {D : GQ2.SectionEight.RadicalCoverData Bg}
  [TopologicalSpace Bg] [DiscreteTopology Bg] {Γ : Type} [Group Γ]
  [TopologicalSpace Γ] [IsTopologicalGroup Γ] (ρ : Γ →ₜ* Bg ⧸ D.M)
  [DistribMulAction Γ (ZMod 2)]
  (Dsc : GQ2.SectionEight.AffineTLift.Descent D)
  (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m)
  (f₀ : GQ2.SectionEight.MLifts D ρ)
  (hf₀ : GQ2.SectionEight.MLifts.Central D f₀) :
  Nat.card
      { f //
        GQ2.SectionEight.MLifts.Central D f ∧
          GQ2.SectionEight.AffineTLift.redT ρ f =
            GQ2.SectionEight.AffineTLift.redT ρ f₀ } =
    Nat.card (GQ2.SectionEight.CentralObstruction.TCocycle D ρ)

theorem GQ2.SectionEight.AffineTLift.lemma_8_7_count
  {Bg : Type} [Group Bg] [Finite Bg]
  {D :
    GQ2.SectionEight.RadicalCoverData Bg}
  [TopologicalSpace Bg]
  [DiscreteTopology Bg] {Γ : Type}
  [Group Γ] [TopologicalSpace Γ]
  [IsTopologicalGroup Γ]
  (ρ : Γ →ₜ* Bg ⧸ D.M)
  [DistribMulAction Γ (ZMod 2)]
  (Dsc :
    GQ2.SectionEight.AffineTLift.Descent
      D)
  (htriv :
    ∀ (γ : Γ) (m : ZMod 2), γ • m = m)
  (f₀ : GQ2.SectionEight.MLifts D ρ)
  (hf₀ :
    GQ2.SectionEight.MLifts.Central D
      f₀) :
  Nat.card
      { f //
        GQ2.SectionEight.MLifts.Central D
            f ∧
          GQ2.SectionEight.AffineTLift.redT
              ρ f =
            GQ2.SectionEight.AffineTLift.redT
              ρ f₀ } =
    Nat.card
      (GQ2.SectionEight.CentralObstruction.TCocycle
        D ρ)

**Lemma 8.7, count form** (the Prop. 8.9 assembly, 2.4c): the central `M`-lifts sharing the `T`-reduction
of a fixed central lift `f₀` number exactly `#Z¹_{Γ,ρ}(T)` — the multiplicity `μ` of (132),
constant over the `V`-coordinate.  (`Central` is automatic on the torsor once `f₀` is central,
by `central_twist_iff`.)  d6 sums this over the liftable `V`-coordinates to reach `zBC`.

Proof for Lemma 9.6

Proof uses 2

Proof dependency previews

Preview

Proposition 6.8

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §8 of the paper. Ingredients: Proposition 6.8 Proposition 6.9.

Proposition9.7

Group: Central covers, affine fibres, and Fourier inversion (7)

Group member previews

Preview

Lemma 9.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Proposition 8.8 of the paper (Completed-square phase identity).

For either source, every lower exact-image map \rho, every b\in H^1_{\Gamma,\rho}(V), and every \chi\in \mathcal X_T,

Q_{\kappa,\Gamma,\rho}(b) +\langle\partial_{\Gamma,\rho} b+\rho^*e,\chi\rangle =Q^0_{\Gamma,\rho}(b+\rho^*a_{\chi,\kappa}) +\iota_\Gamma(\rho^*\Delta_{\chi,\kappa}).

Here Q^0 is the base determinant form and Q_\kappa is the obstruction for the actual scalar pushout class (131).

Lean code for Proposition9.7●1 theorem

theoremdefined in GQ2/AffineTLift.lean

complete

theorem GQ2.SectionEight.AffineTLift.prop_8_8_target {C : Type} [Group C]
  {V : Type} [AddCommGroup V] [DistribMulAction C V] (q : V → ZMod 2)
  (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q) (dat : GQ2.FactorSet C V)
  (hdat : GQ2.IsEquivariantFactorSet q dat) (γ : C → V →+ ZMod 2)
  (δ : C × C → ZMod 2) (a : C → V)
  (ha : ∀ (c d : C), a (c * d) = a c + c • a d)
  (hkill :
    ∀ (c : C) (v : V), GQ2.QuadraticFp2.polar q (a c) v + (γ c) v = 0) :
  ∃ w,
    ∀ (p q' : V × C),
      GQ2.kappa0 dat (GQ2.SectionSix.shear a p)
              (GQ2.SectionSix.shear a q') +
            GQ2.SectionSix.gammaEdge γ (GQ2.SectionSix.shear a p)
              (GQ2.SectionSix.shear a q') +
          GQ2.SectionSix.inflScalar δ (GQ2.SectionSix.shear a p)
            (GQ2.SectionSix.shear a q') =
        GQ2.kappa0 dat p q' +
            GQ2.SectionSix.inflScalar
              (GQ2.SectionEight.AffineTLift.DeltaScalar dat γ δ a) p
              q' +
          (w (p.1 + p.2 • q'.1, p.2 * q'.2) + w p + w q')

theorem GQ2.SectionEight.AffineTLift.prop_8_8_target
  {C : Type} [Group C] {V : Type}
  [AddCommGroup V] [DistribMulAction C V]
  (q : V → ZMod 2)
  (hq : GQ2.QuadraticFp2.IsQuadraticFp2 q)
  (dat : GQ2.FactorSet C V)
  (hdat :
    GQ2.IsEquivariantFactorSet q dat)
  (γ : C → V →+ ZMod 2)
  (δ : C × C → ZMod 2) (a : C → V)
  (ha :
    ∀ (c d : C),
      a (c * d) = a c + c • a d)
  (hkill :
    ∀ (c : C) (v : V),
      GQ2.QuadraticFp2.polar q (a c) v +
          (γ c) v =
        0) :
  ∃ w,
    ∀ (p q' : V × C),
      GQ2.kappa0 dat
              (GQ2.SectionSix.shear a p)
              (GQ2.SectionSix.shear a
                q') +
            GQ2.SectionSix.gammaEdge γ
              (GQ2.SectionSix.shear a p)
              (GQ2.SectionSix.shear a
                q') +
          GQ2.SectionSix.inflScalar δ
            (GQ2.SectionSix.shear a p)
            (GQ2.SectionSix.shear a q') =
        GQ2.kappa0 dat p q' +
            GQ2.SectionSix.inflScalar
              (GQ2.SectionEight.AffineTLift.DeltaScalar
                dat γ δ a)
              p q' +
          (w
                (p.1 + p.2 • q'.1,
                  p.2 * q'.2) +
              w p +
            w q')

**Prop 8.8, target side** (the Prop. 8.9 assembly, 2.6): the edge-killing shear collapses the general
determinant class to `κ⁰ + inf Δ` up to an explicit coboundary.

Proof for Proposition 9.7

Proof uses 2

Proof dependency previews

Preview

Corollary 6.10

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §8 of the paper. Ingredients: Corollary 6.10 Lemma 7.13.

Lemma9.8

Group: Central covers, affine fibres, and Fourier inversion (7)

Group member previews

Preview

Lemma 9.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Lemma 8.9 of the paper (Elementary lifting and exact-image subtraction).

For every \rho\in X_\Gamma(C),

H^2_{\Gamma,\rho}(M)=0, \qquad |Z^1_{\Gamma,\rho}(M)|=2^{2\dim M}.

Consequently

e_\Gamma(B)=2^{2\dim M}e_\Gamma(C) -\sum_{\substack{J<B\\J\twoheadrightarrow C}}e_\Gamma(J),

where each J has the boundary-framed structure induced from B. For every proper J<B occurring in this sum,

|J\cap L_B|=|J\cap M|\,|L_C| \le \frac{|M|}{2}|L_C| =\frac{|L_B|}{2}<|L_Y|.

Lean code for Lemma9.8●3 theorems

theoremdefined in GQ2/Prop89Close.lean

complete

theorem GQ2.SectionEight.prop_8_9 {H E : Type} [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E] (B : GQ2.BoundaryMaps) {Y : Type}
  [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y]
  (T : GQ2.MarkedTarget H E Y)
  (Blk : GQ2.SectionSeven.MinimalBlock T.LY)
  (hE2 : ∀ (e : E), e ^ 2 = 1)
  (En : (GQ2.blockFrameImpl T Blk hE2).Enrichment)
  (F : GQ2.BoundaryFrame H E)
  [CompactSpace ↑GQ2.GammaA.toProfinite.toTop]
  [TotallyDisconnectedSpace ↑GQ2.GammaA.toProfinite.toTop]
  [IsTopologicalGroup ↑GQ2.GammaA.toProfinite.toTop]
  [CompactSpace GQ2.AbsGalQ2] [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  [IsTopologicalGroup GQ2.AbsGalQ2]
  (hfgF : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (hheadA : Function.Surjective fun γ => (F.frameMap (B.bA γ)).1)
  (hheadF : Function.Surjective fun γ => (F.frameMap (B.bF γ)).1)
  (hsimple :
    ∀ (W : AddSubgroup En.Vmod),
      (∀ (g : (GQ2.blockFrameImpl T Blk hE2).YC), ∀ w ∈ W, g • w ∈ W) →
        W = ⊥ ∨ W = ⊤)
  (hVne : ∃ v, v ≠ 0) (hnt : ∃ g v, g • v ≠ v) (G0 : ℤ)
  (hGaussZA :
    ∀ (l : (GQ2.blockFrameImpl T Blk hE2).DR)
      (h : l ≠ (GQ2.blockFrameImpl T Blk hE2).zeroDR),
      GQ2.SectionEight.GaussZResidue B.bA F En l h G0)
  (hGaussZF :
    ∀ (l : (GQ2.blockFrameImpl T Blk hE2).DR)
      (h : l ≠ (GQ2.blockFrameImpl T Blk hE2).zeroDR),
      GQ2.SectionEight.GaussZResidue B.bF F En l h G0) :
  ∃ μ G0' DT x phase,
    0 < Nat.card DT ∧
      GQ2.SectionEight.ClosedRecursion (GQ2.blockFrameImpl T Blk hE2)
          B.bA F μ G0' DT phase ∧
        GQ2.SectionEight.ClosedRecursion (GQ2.blockFrameImpl T Blk hE2)
          B.bF F μ G0' DT phase

theorem GQ2.SectionEight.prop_8_9 {H E : Type}
  [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H]
  [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E]
  (B : GQ2.BoundaryMaps) {Y : Type}
  [Group Y] [TopologicalSpace Y]
  [DiscreteTopology Y] [Finite Y]
  (T : GQ2.MarkedTarget H E Y)
  (Blk :
    GQ2.SectionSeven.MinimalBlock T.LY)
  (hE2 : ∀ (e : E), e ^ 2 = 1)
  (En :
    (GQ2.blockFrameImpl T Blk
        hE2).Enrichment)
  (F : GQ2.BoundaryFrame H E)
  [CompactSpace
      ↑GQ2.GammaA.toProfinite.toTop]
  [TotallyDisconnectedSpace
      ↑GQ2.GammaA.toProfinite.toTop]
  [IsTopologicalGroup
      ↑GQ2.GammaA.toProfinite.toTop]
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  [IsTopologicalGroup GQ2.AbsGalQ2]
  (hfgF :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (hheadA :
    Function.Surjective fun γ =>
      (F.frameMap (B.bA γ)).1)
  (hheadF :
    Function.Surjective fun γ =>
      (F.frameMap (B.bF γ)).1)
  (hsimple :
    ∀ (W : AddSubgroup En.Vmod),
      (∀
          (g :
            (GQ2.blockFrameImpl T Blk
                hE2).YC),
          ∀ w ∈ W, g • w ∈ W) →
        W = ⊥ ∨ W = ⊤)
  (hVne : ∃ v, v ≠ 0)
  (hnt : ∃ g v, g • v ≠ v) (G0 : ℤ)
  (hGaussZA :
    ∀
      (l :
        (GQ2.blockFrameImpl T Blk hE2).DR)
      (h :
        l ≠
          (GQ2.blockFrameImpl T Blk
              hE2).zeroDR),
      GQ2.SectionEight.GaussZResidue B.bA
        F En l h G0)
  (hGaussZF :
    ∀
      (l :
        (GQ2.blockFrameImpl T Blk hE2).DR)
      (h :
        l ≠
          (GQ2.blockFrameImpl T Blk
              hE2).zeroDR),
      GQ2.SectionEight.GaussZResidue B.bF
        F En l h G0) :
  ∃ μ G0' DT x phase,
    0 < Nat.card DT ∧
      GQ2.SectionEight.ClosedRecursion
          (GQ2.blockFrameImpl T Blk hE2)
          B.bA F μ G0' DT phase ∧
        GQ2.SectionEight.ClosedRecursion
          (GQ2.blockFrameImpl T Blk hE2)
          B.bF F μ G0' DT phase

**Proposition 8.9 (closed exact-image recursion)**: for the concrete block frame of a
boundary-framed target with a §7 simple-head block, there are **shared** data
`(μ, G⁰, D_T)` and a **per-`λ`** phase family such that the boxed system (136)–(142) holds
for **both sources**.  Every count on the right sides concerns a target with strictly
smaller marked 2-kernel, so the system is a closed deterministic recursion (paper, end of
§8).  [the §8 proof layer statement — relocated & amended at the Prop. 8.9 assembly, see the module docstring; proof =
the Prop. 8.9 assembly.  Verified axioms: std-3 + {B6, B7} (within the App. D ≤ {B6, B7, B9}
budget; B9 never enters).]

theoremdefined in GQ2/RecursionSplice.lean

complete

theorem GQ2.SectionEight.prop_8_9_of {H E : Type} [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E] (B : GQ2.BoundaryMaps)
  [CompactSpace ↑GQ2.GammaA.toProfinite.toTop]
  [TotallyDisconnectedSpace ↑GQ2.GammaA.toProfinite.toTop]
  [IsTopologicalGroup ↑GQ2.GammaA.toProfinite.toTop]
  [CompactSpace GQ2.AbsGalQ2] [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  [IsTopologicalGroup GQ2.AbsGalQ2] {Y : Type} [Group Y]
  [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y]
  {T : GQ2.MarkedTarget H E Y}
  {Blk : GQ2.SectionSeven.MinimalBlock T.LY}
  (RF : GQ2.SectionEight.RecursionFrame T Blk)
  (F : GQ2.BoundaryFrame H E) (μ : ℕ) (G0 : ℤ) (DT : Type) [Fintype DT]
  (phase :
    (l : RF.DR) →
      l ≠ RF.zeroDR → DT → GQ2.SectionEight.CentralCover RF.YC)
  (hfgA : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (hheadA : Function.Surjective fun γ => (F.frameMap (B.bA γ)).1)
  (hfgF : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (hheadF : Function.Surjective fun γ => (F.frameMap (B.bF γ)).1)
  (inpA : GQ2.SectionEight.RecursionInputs RF B.bA F μ G0 DT phase)
  (inpF : GQ2.SectionEight.RecursionInputs RF B.bF F μ G0 DT phase) :
  ∃ μ' G0' DT' x phase',
    GQ2.SectionEight.ClosedRecursion RF B.bA F μ' G0' DT' phase' ∧
      GQ2.SectionEight.ClosedRecursion RF B.bF F μ' G0' DT' phase'

theorem GQ2.SectionEight.prop_8_9_of {H E : Type}
  [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H]
  [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E]
  (B : GQ2.BoundaryMaps)
  [CompactSpace
      ↑GQ2.GammaA.toProfinite.toTop]
  [TotallyDisconnectedSpace
      ↑GQ2.GammaA.toProfinite.toTop]
  [IsTopologicalGroup
      ↑GQ2.GammaA.toProfinite.toTop]
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  [IsTopologicalGroup GQ2.AbsGalQ2]
  {Y : Type} [Group Y]
  [TopologicalSpace Y]
  [DiscreteTopology Y] [Finite Y]
  {T : GQ2.MarkedTarget H E Y}
  {Blk :
    GQ2.SectionSeven.MinimalBlock T.LY}
  (RF :
    GQ2.SectionEight.RecursionFrame T Blk)
  (F : GQ2.BoundaryFrame H E) (μ : ℕ)
  (G0 : ℤ) (DT : Type) [Fintype DT]
  (phase :
    (l : RF.DR) →
      l ≠ RF.zeroDR →
        DT →
          GQ2.SectionEight.CentralCover
            RF.YC)
  (hfgA :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (hheadA :
    Function.Surjective fun γ =>
      (F.frameMap (B.bA γ)).1)
  (hfgF :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (hheadF :
    Function.Surjective fun γ =>
      (F.frameMap (B.bF γ)).1)
  (inpA :
    GQ2.SectionEight.RecursionInputs RF
      B.bA F μ G0 DT phase)
  (inpF :
    GQ2.SectionEight.RecursionInputs RF
      B.bF F μ G0 DT phase) :
  ∃ μ' G0' DT' x phase',
    GQ2.SectionEight.ClosedRecursion RF
        B.bA F μ' G0' DT' phase' ∧
      GQ2.SectionEight.ClosedRecursion RF
        B.bF F μ' G0' DT' phase'

**Prop 8.9, reduced to the per-source `RecursionInputs` + shared witness** (the splice
backbone).
Given the shared phase witness `(μ, G0, DT, phase)`, the two per-source side-condition triples, and
the two `RecursionInputs` bundles, the boxed system holds for both sources — each via
`prop_8_9_aux`.  The component lemmas below construct the two `RecursionInputs`.

theoremdefined in GQ2/SectionEight/Recursion.lean

complete

theorem GQ2.SectionEight.prop_8_9_aux {H E : Type} [Group H]
  [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E]
  [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type}
  [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y]
  {T : GQ2.MarkedTarget H E Y}
  {Blk : GQ2.SectionSeven.MinimalBlock T.LY}
  (RF : GQ2.SectionEight.RecursionFrame T Blk) {Γ : Type} [Group Γ]
  [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ]
  [TotallyDisconnectedSpace Γ]
  (hfg : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (b : Γ →ₜ* ↥GQ2.boundarySubgroup) (F : GQ2.BoundaryFrame H E)
  (hscalar : Nat.card (Γ →ₜ* Multiplicative (ZMod 2)) = 8)
  (hhead : Function.Surjective fun γ => (F.frameMap (b γ)).1) (μ : ℕ)
  (G0 : ℤ) (DT : Type) [Fintype DT]
  (phase :
    (l : RF.DR) →
      l ≠ RF.zeroDR → DT → GQ2.SectionEight.CentralCover RF.YC)
  (inp : GQ2.SectionEight.RecursionInputs RF b F μ G0 DT phase) :
  GQ2.SectionEight.ClosedRecursion RF b F μ G0 DT phase

theorem GQ2.SectionEight.prop_8_9_aux {H E : Type}
  [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H]
  [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E]
  {Y : Type} [Group Y]
  [TopologicalSpace Y]
  [DiscreteTopology Y] [Finite Y]
  {T : GQ2.MarkedTarget H E Y}
  {Blk :
    GQ2.SectionSeven.MinimalBlock T.LY}
  (RF :
    GQ2.SectionEight.RecursionFrame T Blk)
  {Γ : Type} [Group Γ]
  [TopologicalSpace Γ]
  [IsTopologicalGroup Γ] [CompactSpace Γ]
  [TotallyDisconnectedSpace Γ]
  (hfg :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (b : Γ →ₜ* ↥GQ2.boundarySubgroup)
  (F : GQ2.BoundaryFrame H E)
  (hscalar :
    Nat.card
        (Γ →ₜ* Multiplicative (ZMod 2)) =
      8)
  (hhead :
    Function.Surjective fun γ =>
      (F.frameMap (b γ)).1)
  (μ : ℕ) (G0 : ℤ) (DT : Type)
  [Fintype DT]
  (phase :
    (l : RF.DR) →
      l ≠ RF.zeroDR →
        DT →
          GQ2.SectionEight.CentralCover
            RF.YC)
  (inp :
    GQ2.SectionEight.RecursionInputs RF b
      F μ G0 DT phase) :
  GQ2.SectionEight.ClosedRecursion RF b F
    μ G0 DT phase

**The Prop 8.9 assembly step** (the Prop. 8.9 assembly): given the source-side input bundle, the boxed
system holds — with **(138) discharged from the proved `lemma_8_3`** (the eight-lift
partition, instantiated at each scalar cover `p_λ` over the `B`-stage target).  The
side conditions (`Γ` profinite + t.f.g. `hfg`, `#Hom(Γ,𝔽₂) = 8`) are exactly `lemma_8_3`'s;
both real sources satisfy them (`lemma_8_2` and the boundary-frame data).

Proof for Lemma 9.8

Proof uses 6

Proof dependency previews

Preview

Lemma 7.12

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §8 of the paper. Ingredients: Lemma 8.2 Lemma 9.2 Lemma 9.3 Lemma 9.5 Lemma 7.12 Proposition 9.7.