**Cluster reciprocity.** For every `a > 0`, the Euler transform `G_a` agrees with the dilated reciprocal cluster series `S(B_aᵛ)` in every degree `≤ n`.

import Definitions.Def_TypeDensity_Basic
import Definitions.Def_TypeDensity_Formula_LawAlgebra
import Definitions.Def_TypeDensity_Formula_StateCombinatorics
import Definitions.Def_TypeDensity_Reciprocity_Defs
import Definitions.Def_TypeDensity_Reciprocity_Quantum
import Definitions.Def_TypeDensity_Reciprocity_Patterns
import Theorems.Thm_TypeDensity_QCongr_qact_scongr
import Theorems.Thm_TypeDensity_coeff_qact_gaussPhi_of_lt
import Theorems.Thm_TypeDensity_qact_qmul
import Theorems.Thm_TypeDensity_qact_qone
import Theorems.Thm_TypeDensity_qact_sub
import Theorems.Thm_TypeDensity_coeff_clusterSer_eq_coeff_qact
import Theorems.Thm_TypeDensity_X_inv_sub_X_zpow_neg_tri_ne_zero
import Theorems.Thm_TypeDensity_crossingQ_zero_zero
import Theorems.Thm_TypeDensity_crossingQ_symm
import Theorems.Thm_TypeDensity_qcongr_crossingQ_mul_qdagger
import Theorems.Thm_TypeDensity_cluster_reciprocity_one
import Theorems.Thm_TypeDensity_coeff_pPow_sub_of_scongr
import Theorems.Thm_TypeDensity_constantCoeff_eulerSer
import Theorems.Thm_TypeDensity_coeff_zero_dilate_recipSer_clusterSer
import Theorems.Thm_TypeDensity_clusterSer_eq_pPow
import Theorems.Thm_TypeDensity_dilate_recipSer_eulerSer_eq_pPow
import Theorems.Thm_TypeDensity_recipSer_qact
import Theorems.Thm_TypeDensity_dilate_codilate
import Theorems.Thm_TypeDensity_recipSer_gaussPhi
import Theorems.Thm_TypeDensity_gaussPhi_dilate
import Theorems.Thm_TypeDensity_gaussPhi_sub
import Theorems.Thm_TypeDensity_gaussPhi_qactRecip_gaussPhiInv
import Theorems.Thm_TypeDensity_eq_zero_of_scalar_mul_eq_zero
import Theorems.Thm_TypeDensity_SCongr_mono
import Mathlib.FieldTheory.RatFunc.Basic
import Mathlib.MeasureTheory.Measure.Haar.Unique
import Mathlib.NumberTheory.ArithmeticFunction.Moebius
import Mathlib.NumberTheory.Padics.PadicIntegers
import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
import Mathlib.RingTheory.MvPowerSeries.Basic
import Mathlib.RingTheory.RamificationInertia.Basic
import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
import Mathlib.FieldTheory.Finite.GaloisField
import Mathlib.RingTheory.AdicCompletion.Algebra
import Mathlib.RingTheory.RegularLocalRing.Defs
import Mathlib.FieldTheory.RatFunc.AsPolynomial
import Mathlib.RingTheory.PowerSeries.Expand
import Mathlib.RingTheory.PowerSeries.Log
set_option autoImplicit false

open TypeDensity

theorem TypeDensity.cluster_reciprocity (n a : ℕ) (ha : 0 < a) :
    SCongr n (eulerSer 0 a) (dilate (recipSer (clusterSer a))) := by sorry