Documentation

GQ2.RecursionSplice

§8 capstone — the Proposition 8.9 two-source splice helpers #

GQ2.SectionEight.prop_8_9 asserts the boxed recursion system ClosedRecursion for both sources B.bA (Γ_A) and B.bF (G_ℚ₂), sharing one witness (μ, G0, DT, phase). Its proof is the final assembly of §8: prop_8_9_aux turns a per-source RecursionInputs bundle (stageR136 + half139 + phase140, with (137)/(138) discharged internally) into ClosedRecursion, and the two sources share the phase witness.

This file keeps the splice in a leaf of the import graph: prop_8_9_of reduces the conclusion to the per-source inputs and shared witness, and the component lemmas construct those inputs from the obstruction, half-torsor, and phase APIs. The final theorem is assembled downstream in GQ2/Prop89Close.lean.

Inputs (per source s ∈ {A, F}, Γ_s ∈ {Γ_A, G_ℚ₂}) #

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

half139 reduced to the source's MLifts-level count (d3 bridge discharged) #

half139_via_radData strips the Prop. 8.9 assembly bridge plumbing (centralOver_equiv/liftsOver_equiv over En.radData) off the half139 obligation, reducing it to the two pure MLifts source facts for the transported lower map ρ' = rhoPrime …:

So a caller feeds half139_of (hence RecursionInputs.half139) directly from the source arithmetic, with no CentralOver/LiftsOver bookkeeping.

source
theorem GQ2.SectionEight.half139_via_radData {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hlem86M : ∀ (ρ : BoundaryLifts b F RF.TC), 2 * Nat.card { f : MLifts (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ) // MLifts.Central (En.radData l h) f } = Nat.card (MLifts (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ))) (hMcountM : ∀ (ρ : BoundaryLifts b F RF.TC), Nat.card (MLifts (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) = Nat.card ↥RF.MB ^ 2) :
2 * RF.zBC b F l h = Nat.card ↥RF.MB ^ 2 * exactImageCount b F RF.TC
source
theorem GQ2.SectionEight.zBC_eq_sum_centralOver {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (l : RF.DR) (h : l ≠ RF.zeroDR) :
RF.zBC b F l h = ∑ᶠ (ρ : BoundaryLifts b F RF.TC), Nat.card (RF.CentralOver b F l h ρ)

The zBC fibration over the lower exact-image map ρ: zBC = Σ_ρ #CentralOver(ρ). Both the (139) and (140) counts rest on this (it is the first step inside half139_of); extracted here so the (140) hfib datum zBC = μ·M gets it too — zBC = Σ_ρ #CentralOver = Σ_ρ μ·M_ρ = μ·M.

phase140 reduced to a clean "phase datum" (the lemma_8_5/8.7 analog of stageR136_of) #

hfib level 2 — the per-ρ μ-partition of the central M-lifts #

source
theorem GQ2.SectionEight.central_card_eq_reductions_mul_tcocycle {Bg : Type} [Group Bg] [Finite Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] {D : RadicalCoverData Bg} {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [DistribMulAction Γ (ZMod 2)] [ContinuousSMul Γ (ZMod 2)] (ρ : Γ →ₜ* Bg ⧸ D.M) (Dsc : AffineTLift.Descent D) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) :
Nat.card { f : MLifts D ρ // MLifts.Central D f } = Nat.card ↑(Set.range fun (f : { f : MLifts D ρ // MLifts.Central D f }) => AffineTLift.redT ρ ↑f) * Nat.card (CentralObstruction.TCocycle D ρ)

The per-ρ μ-partition (the Prop. 8.9 assembly, hfib level 2): in the zero-edge regime the central M-lifts of a lower map ρ split into the fibres of the T-reduction map red_T, and each (nonempty) fibre is a free Z¹_{Γ,ρ}(T)-torsor of size μ = #Z¹(T) (lemma_8_7_count, Central constant by central_twist_iff). Hence the central-lift count factors as (#achievable central T-reductions) · μ. Summed over the C-image ρ (via zBC_eq_sum_centralOver, after transport through centralOver_equiv) and combined with the μ-independence #Z¹(T) = μ, this is the (140) hfib datum zBC = μ·M fed to phase140_ofPhaseData; here M = Σ_ρ #achievable central T-reductions is the constrained count of lemma_8_5.

source
theorem GQ2.SectionEight.centralOver_card_eq_reductions_mul_tcocycle {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [DistribMulAction Γ (ZMod 2)] [ContinuousSMul Γ (ZMod 2)] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (l : RF.DR) (h : l ≠ RF.zeroDR) (D : RadicalCoverData RF.YB) (hD : D.M = RF.MB) (hC : D.C = RF.scalarCover l h) (ρ : BoundaryLifts b F RF.TC) (Dsc : AffineTLift.Descent D) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) :
Nat.card (RF.CentralOver b F l h ρ) = Nat.card ↑(Set.range fun (f : { f : MLifts D (RF.rhoPrime b F D hD ρ) // MLifts.Central D f }) => AffineTLift.redT (RF.rhoPrime b F D hD ρ) ↑f) * Nat.card (CentralObstruction.TCocycle D (RF.rhoPrime b F D hD ρ))

The per-ρ μ-partition, in bridge vocabulary (the Prop. 8.9 assembly): transporting central_card_eq_reductions_mul_tcocycle through centralOver_equiv, the zBC-fibre #CentralOver(ρ) (the summand of zBC_eq_sum_centralOver) factors as (#achievable central T-reductions of ρ' = rhoPrime …) · #Z¹(T). This is the per-fibre form of the (140) hfib datum: once #Z¹(T) = μ is shown ρ-independent, summing over ρ gives zBC = μ · M with M = Σ_ρ #achievable central T-reductions (the lemma_8_5 count).

source
theorem GQ2.SectionEight.zBC_eq_mu_mul_reductionCount {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [DistribMulAction Γ (ZMod 2)] [ContinuousSMul Γ (ZMod 2)] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (l : RF.DR) (h : l ≠ RF.zeroDR) (D : RadicalCoverData RF.YB) (hD : D.M = RF.MB) (hC : D.C = RF.scalarCover l h) (Dsc : AffineTLift.Descent D) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (μ : ℕ) (hμ : ∀ (ρ : BoundaryLifts b F RF.TC), Nat.card (CentralObstruction.TCocycle D (RF.rhoPrime b F D hD ρ)) = μ) :
RF.zBC b F l h = μ * ∑ᶠ (ρ : BoundaryLifts b F RF.TC), Nat.card ↑(Set.range fun (f : { f : MLifts D (RF.rhoPrime b F D hD ρ) // MLifts.Central D f }) => AffineTLift.redT (RF.rhoPrime b F D hD ρ) ↑f)

The (140) hfib datum, reduced to μ-independence (the Prop. 8.9 assembly). Summing the per-ρ μ-partition (centralOver_card_eq_reductions_mul_tcocycle) over the C-image via zBC_eq_sum_centralOver and factoring out the common μ (hypothesis hμ: the T-cocycle count #Z¹(T) is ρ-independent — the source 5.15/5.16 fact) gives the (140) fibration zBC = μ · M, with M = Σ_ρ #achievable central T-reductions. This is exactly the hfib argument of phase140_ofPhaseData: the (140) fibration is now reduced to the single source input hμ (and M is the lemma_8_5 constrained count fed to hgauss).

hgauss level 1 — aggregating the Gauss engine lemma_8_5 over the ρ-family #

source
theorem GQ2.SectionEight.lemma_8_5_aggregated {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), 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 : I, ↑(Nat.card { x : W // L x = κ i ∧ Q x = ε i }) = ↑(Fintype.card I) * ↑(Nat.card W) + gaussSum Q * ∑ᶠ (χ : Module.Dual (ZMod 2) E), ∑ i : I, 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.

The capstone (140) reducer — phase140 from the concrete correspondences #

Discharging the polar data a_χ from nonsingularity (the En.hns supply) #

source
theorem GQ2.SectionEight.enrichment_card_Vmod {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} (RF : RecursionFrame T Blk) (En : RF.Enrichment) [Finite ↥RF.MB] :
Nat.card En.Vmod = Nat.card ↥RF.MB / Nat.card ↥RF.TBsub

The |V| = |M_B|/|T_B| match (the Prop. 8.9 assembly): the enrichment's descent M_B ↠ V with ker = T_B gives |V| = |M_B|/|T_B| by the first isomorphism theorem — discharging the hWV cardinality match of phase140_of_nonsingular directly from En (with W := En.Vmod).

Paper-tag ledger (auto-generated by paperforge; do not edit) #