Local-global conjecture for Apollonian circle packings

DefinitionGeneral linear group action on primitive vectors#✓fully proved

Call \(v \in \mathbb{Z}^4\) primitive when the greatest common divisor of its four entries is \(1\). For every \(X \in \mathrm{GL}_4(\mathbb{Z})\) and every primitive \(v\), the vector \(Xv\) is primitive, so \(\mathrm{GL}_4(\mathbb{Z})\) acts on the primitive vectors of \(\mathbb{Z}^4\) by \(v \mapsto Xv\).

MathlibExt.NumberTheory.LocalGlobalApollonianCirclePackingsWanted.LocalGlobalApollonianCirclePackings.GeneralLinearGroupAction · 16 lines

def GeneralLinearGroupAction : SubMulAction (GL (Fin 4) ℤ) (Fin 4 → ℤ) where
  carrier := { v | Finset.univ.gcd v = 1}
  smul_mem' X v hv := by
    rw [Set.mem_ofPred_eq] at hv ⊢
    apply Int.eq_one_of_dvd_one
    · rw [← Finset.normalize_gcd, ← Int.abs_eq_normalize]
      apply abs_nonneg
    · rw [← hv, Finset.dvd_gcd_iff]
      intro i _
      have key : v i = ((X⁻¹).1 *ᵥ (X.1 *ᵥ v)) i := by simp
      rw [key, mulVec_eq_sum (X.1 *ᵥ v) (X⁻¹).1]
      simp only [op_smul_eq_smul, Finset.sum_apply]
      apply Finset.dvd_sum
      intro i hi
      apply dvd_mul_of_dvd_left
      apply Finset.gcd_dvd hi

Used by 1

Used byDescartes orthogonal group action

DefinitionDescartes matrix#✓fully proved

The Descartes matrix is the \(4 \times 4\) integer matrix \(M\) with \(M_{ii} = 1\) for every \(i\) and \(M_{ij} = -1\) for \(i \ne j\). It is the matrix of the Descartes form: for \(v = (a, b, c, d) \in \mathbb{Z}^4\) one has \(v^{\mathsf T} M v = 2(a^2 + b^2 + c^2 + d^2) - (a + b + c + d)^2\).

def DescartesMatrix : Matrix (Fin 4) (Fin 4) ℤ :=
  !![1, -1, -1, -1;
     -1, 1, -1, -1;
     -1, -1, 1, -1;
     -1, -1, -1, 1]

Used by 3

Used byDescartes orthogonal group · Descartes orthogonal group action · The transformation group preserves integral primitive Descartes quadruples

DefinitionDescartes orthogonal group#✓fully proved

Let \(M\) be the Descartes matrix. The Descartes orthogonal group is the subgroup of \(\mathrm{GL}_4(\mathbb{Z})\) consisting of the matrices \(X\) with \(X^{\mathsf T} M X = M\), that is, the invertible integer matrices that preserve the Descartes form \(2(a^2 + b^2 + c^2 + d^2) - (a + b + c + d)^2\).

def DescartesOrthogonalGroup : Subgroup (GL (Fin 4) ℤ) where
  carrier := {X | star X * DescartesMatrix * X = DescartesMatrix}
  one_mem' := by simp
  inv_mem' hX := by grind [star_inv, Units.inv_mul_cancel_left, Units.mul_inv]
  mul_mem' hX hY := by grind [Units.val_mul, StarMul.star_mul]

Uses 1 · Used by 2

Statement usesDescartes matrix

Used byDescartes orthogonal group action · The transformation group preserves integral primitive Descartes quadruples

DefinitionDescartes orthogonal group action#✓fully proved

Let \(Q\) be the set of vectors \((a, b, c, d) \in \mathbb{Z}^4\) with \((a + b + c + d)^2 = 2(a^2 + b^2 + c^2 + d^2)\) and \(\gcd(a, b, c, d) = 1\). For every matrix \(X\) in the Descartes orthogonal group and every \(v \in Q\), the vector \(Xv\) lies in \(Q\), so the Descartes orthogonal group acts on \(Q\) by \(v \mapsto Xv\).

def DescartesOrthogonalGroupAction : SubMulAction DescartesOrthogonalGroup (Fin 4 → ℤ) where
  carrier := { v | (∑ i, v i) ^ 2 = 2 * ∑ i, v i ^ 2 ∧ Finset.univ.gcd v = 1}
  smul_mem' := by
    rintro ⟨X, hX⟩ v ⟨hv1, hv2⟩
    rw [mem_descartesOrthogonalGroup_iff, Units.coe_star,
      star_eq_conjTranspose, conjTranspose_eq_transpose_of_trivial] at hX
    refine ⟨?_, GeneralLinearGroupAction.smul_mem X hv2⟩
    rw [descartes_iff] at hv1 ⊢
    rwa [Subgroup.mk_smul, GeneralLinearGroup.smul_def,
      vecMul_mulVec, dotProduct_mulVec, vecMul_vecMul, hX]

Uses 3 · Used by 1

Statement usesDescartes matrix · Descartes orthogonal group · General linear group action on primitive vectors

Used byThe transformation group preserves integral primitive Descartes quadruples

DefinitionIntegral primitive Descartes quadruple#✓fully proved

An integral primitive Descartes quadruple is a vector \((a, b, c, d) \in \mathbb{Z}^4\) such that \(a + b + c + d > 0\), the Descartes equation \((a + b + c + d)^2 = 2(a^2 + b^2 + c^2 + d^2)\) holds, and \(\gcd(a, b, c, d) = 1\).

def integralPrimitiveDescartesQuadruple : Set (Fin 4 → ℤ) :=
  { v | ∑ i, v i > 0 ∧ (∑ i, v i) ^ 2 = 2 * ∑ i, v i ^ 2 ∧ Finset.univ.gcd v = 1}

Sources

• S. Haag, C. Kertzer, J. Rickards, and K. E. Stange, The local-global conjecture for Apollonian circle packings is false, Annals of Math, 200 (2) 2024, Section 1.1.

Used by 5

Used byCurvature set · Primitive Apollonian circle packing · A packing with no square curvatures · Action of the transformation group on integral primitive Descartes quadruples · The transformation group preserves integral primitive Descartes quadruples

AbbreviationThe Apollonian generator \(S_1\)#✓fully proved

\(S_1\) is the element of \(\mathrm{GL}_4(\mathbb{Z})\) given by the \(4 \times 4\) integer matrix whose first row is \((-1, 2, 2, 2)\) and whose other rows are those of the identity matrix; it is its own inverse. Acting on column vectors, it sends \((a, b, c, d)\) to \((-a + 2b + 2c + 2d, b, c, d)\).

It is one of the four generators of the Apollonian group defined at the start of Section 3 of Haag, Kertzer, Rickards and Stange.

abbrev S₁ : GL (Fin 4) ℤ :=
  ⟨!![-1, 2, 2, 2; 0, 1, 0, 0; 0, 0, 1, 0; 0, 0, 0, 1],
    !![-1, 2, 2, 2; 0, 1, 0, 0; 0, 0, 1, 0; 0, 0, 0, 1],
    by decide, by decide⟩

Used by 2

Used byApollonian group · The transformation group preserves integral primitive Descartes quadruples

AbbreviationThe Apollonian generator \(S_2\)#✓fully proved

\(S_2\) is the element of \(\mathrm{GL}_4(\mathbb{Z})\) given by the \(4 \times 4\) integer matrix whose second row is \((2, -1, 2, 2)\) and whose other rows are those of the identity matrix; it is its own inverse. Acting on column vectors, it sends \((a, b, c, d)\) to \((a, 2a - b + 2c + 2d, c, d)\).

It is one of the four generators of the Apollonian group defined at the start of Section 3 of Haag, Kertzer, Rickards and Stange.

abbrev S₂ : GL (Fin 4) ℤ :=
  ⟨!![1, 0, 0, 0; 2, -1, 2, 2; 0, 0, 1, 0; 0, 0, 0, 1],
    !![1, 0, 0, 0; 2, -1, 2, 2; 0, 0, 1, 0; 0, 0, 0, 1],
    by decide, by decide⟩

Used by 2

Used byApollonian group · The transformation group preserves integral primitive Descartes quadruples

AbbreviationThe Apollonian generator \(S_3\)#✓fully proved

\(S_3\) is the element of \(\mathrm{GL}_4(\mathbb{Z})\) given by the \(4 \times 4\) integer matrix whose third row is \((2, 2, -1, 2)\) and whose other rows are those of the identity matrix; it is its own inverse. Acting on column vectors, it sends \((a, b, c, d)\) to \((a, b, 2a + 2b - c + 2d, d)\).

It is one of the four generators of the Apollonian group defined at the start of Section 3 of Haag, Kertzer, Rickards and Stange.

abbrev S₃ : GL (Fin 4) ℤ :=
  ⟨!![1, 0, 0, 0; 0, 1, 0, 0; 2, 2, -1, 2; 0, 0, 0, 1],
    !![1, 0, 0, 0; 0, 1, 0, 0; 2, 2, -1, 2; 0, 0, 0, 1],
    by decide, by decide⟩

Used by 2

Used byApollonian group · The transformation group preserves integral primitive Descartes quadruples

AbbreviationThe Apollonian generator \(S_4\)#✓fully proved

\(S_4\) is the element of \(\mathrm{GL}_4(\mathbb{Z})\) given by the \(4 \times 4\) integer matrix whose fourth row is \((2, 2, 2, -1)\) and whose other rows are those of the identity matrix; it is its own inverse. Acting on column vectors, it sends \((a, b, c, d)\) to \((a, b, c, 2a + 2b + 2c - d)\).

It is one of the four generators of the Apollonian group defined at the start of Section 3 of Haag, Kertzer, Rickards and Stange.

abbrev S₄ : GL (Fin 4) ℤ :=
  ⟨!![1, 0, 0, 0; 0, 1, 0, 0; 0, 0, 1, 0; 2, 2, 2, -1],
    !![1, 0, 0, 0; 0, 1, 0, 0; 0, 0, 1, 0; 2, 2, 2, -1],
    by decide, by decide⟩

Used by 2

Used byApollonian group · The transformation group preserves integral primitive Descartes quadruples

DefinitionApollonian group#✓fully proved

The Apollonian group is the subgroup of \(\mathrm{GL}_4(\mathbb{Z})\) generated by the four matrices \(S_1, S_2, S_3, S_4\), where \(S_i\) agrees with the \(4 \times 4\) identity matrix except in row \(i\), which has entry \(-1\) in column \(i\) and entry \(2\) in each of the other three columns.

def ApollonianGroup : Subgroup (GL (Fin 4) ℤ) := Subgroup.closure {S₁, S₂, S₃, S₄}

Sources

• S. Haag, C. Kertzer, J. Rickards, and K. E. Stange, The local-global conjecture for Apollonian circle packings is false, Annals of Math, 200 (2) 2024, start of Section 3.

Uses 4 · Used by 2

Statement usesThe Apollonian generator \(S_1\) · The Apollonian generator \(S_2\) · The Apollonian generator \(S_3\) · The Apollonian generator \(S_4\)

Used byThe transformation group · The transformation group preserves integral primitive Descartes quadruples

DefinitionThe transformation group#✓fully proved

The transformation group is the subgroup of \(\mathrm{GL}_4(\mathbb{Z})\) generated by the Apollonian group together with all \(4 \times 4\) permutation matrices.

def TransformationGroup : Subgroup (GL (Fin 4) ℤ) :=
  ApollonianGroup ⊔ permMatrixHom.toHomUnits.range

Uses 1 · Used by 5

Statement usesApollonian group

Used byCurvature set · Primitive Apollonian circle packing · A packing with no square curvatures · Action of the transformation group on integral primitive Descartes quadruples · The transformation group preserves integral primitive Descartes quadruples

TheoremThe transformation group preserves integral primitive Descartes quadruples#✓fully proved

For every \(g\) in the transformation group, \(g\) maps the set of integral primitive Descartes quadruples into itself: if \(v \in \mathbb{Z}^4\) is an integral primitive Descartes quadruple, then so is \(g v\).

theorem transformationGroup_smul_integralPrimitiveDescartesQuadruple
    (g : GL (Fin 4) ℤ) (hg : g ∈ TransformationGroup) :
    g • integralPrimitiveDescartesQuadruple ⊆ integralPrimitiveDescartesQuadruple

Uses 10 · Used by 1

Statement usesThe transformation group · Integral primitive Descartes quadruple

Proof usesApollonian group · Descartes matrix · Descartes orthogonal group · Descartes orthogonal group action · The Apollonian generator \(S_1\) · The Apollonian generator \(S_2\) · The Apollonian generator \(S_3\) · The Apollonian generator \(S_4\)

Used byAction of the transformation group on integral primitive Descartes quadruples

DefinitionAction of the transformation group on integral primitive Descartes quadruples#✓fully proved

Each element \(g\) of the transformation group sends an integral primitive Descartes quadruple \(v\) to \(g v\), by matrix–vector multiplication: this is the restriction of the action of the transformation group on \(\mathbb{Z}^4\) to the set of integral primitive Descartes quadruples, which is closed under the action.

def TransformationGroupAction : SubMulAction TransformationGroup (Fin 4 → ℤ) where
  carrier := integralPrimitiveDescartesQuadruple
  smul_mem' X v hv :=
    transformationGroup_smul_integralPrimitiveDescartesQuadruple X X.2 ⟨v, hv, rfl⟩

Uses 3 · Used by 3

Statement usesThe transformation group · Integral primitive Descartes quadruple · The transformation group preserves integral primitive Descartes quadruples

Used byCurvature set · Primitive Apollonian circle packing · A packing with no square curvatures

DefinitionPrimitive Apollonian circle packing#✓fully proved

A primitive Apollonian circle packing is an orbit of the transformation group acting on the set of integral primitive Descartes quadruples.

def PrimitiveApollonianCirclePacking :=
  MulAction.orbitRel.Quotient TransformationGroup integralPrimitiveDescartesQuadruple

Uses 3 · Used by 4

Statement usesThe transformation group · Action of the transformation group on integral primitive Descartes quadruples · Integral primitive Descartes quadruple

Used byCurvature set · Missing curvature set · Number of missing curvatures · Infinitely many packings with many missing curvatures

DefinitionCurvature set#✓fully proved

Let \(A\) be a primitive Apollonian circle packing, viewed as an orbit of integral primitive Descartes quadruples. The curvature set of \(A\) is the set of all integers that occur as an entry of some quadruple in \(A\).

def curvatureSet (A : PrimitiveApollonianCirclePacking) : Set ℤ :=
  ⋃ v ∈ A.orbit, Set.range v.1

Uses 4 · Used by 2

Statement usesPrimitive Apollonian circle packing · The transformation group · Action of the transformation group on integral primitive Descartes quadruples · Integral primitive Descartes quadruple

Used byMissing curvature set · A packing with no square curvatures

TheoremA packing with no square curvatures#●ready to prove

Let \(\mathcal{A}\) be the primitive Apollonian circle packing generated by the integral primitive Descartes quadruple \((-3, 5, 8, 8)\). For every integer \(n\), \(n^2\) does not belong to the curvature set of \(\mathcal{A}\).

public theorem_wanted theorem_1_6 : ∀ n, n ^ 2 ∉ curvatureSet ⟦⟨![-3, 5, 8, 8], by decide⟩⟧

Sources

• S. Haag, C. Kertzer, J. Rickards, and K. E. Stange, The local-global conjecture for Apollonian circle packings is false, Annals of Math, 200 (2) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_local_global_apollonian_circle_packings of the lean-eval benchmark.

Uses 4

Statement usesThe transformation group · Action of the transformation group on integral primitive Descartes quadruples · Curvature set · Integral primitive Descartes quadruple

DefinitionMissing curvature set#✓fully proved

Let \(A\) be a primitive Apollonian circle packing. The missing curvature set of \(A\) is the set of positive integers \(n\) that do not lie in the curvature set of \(A\) but are congruent modulo \(24\) to some element of the curvature set of \(A\).

def missingCurvatureSet (A : PrimitiveApollonianCirclePacking) : Set ℤ :=
  {n | n > 0 ∧ n ∉ curvatureSet A ∧ ∃ k ∈ curvatureSet A, k ≡ n [ZMOD 24]}

Sources

• S. Haag, C. Kertzer, J. Rickards, and K. E. Stange, The local-global conjecture for Apollonian circle packings is false, Annals of Math, 200 (2) 2024, start of Section 1.2.

Uses 2 · Used by 1

Statement usesPrimitive Apollonian circle packing · Curvature set

Used byNumber of missing curvatures

DefinitionNumber of missing curvatures#✓fully proved

For a primitive Apollonian circle packing \(A\) and a real number \(N\), the number of missing curvatures of \(A\) up to \(N\) is the number of elements \(n\) of the missing curvature set of \(A\) with \(n \le N\), regarded as a real number.

noncomputable def missingCurvatures (A : PrimitiveApollonianCirclePacking) (N : ℝ) : ℝ :=
  (missingCurvatureSet A ∩ {x | x ≤ N}).ncard

Uses 2 · Used by 1

Statement usesPrimitive Apollonian circle packing · Missing curvature set

Used byInfinitely many packings with many missing curvatures

TheoremInfinitely many packings with many missing curvatures#●ready to prove

For a primitive Apollonian circle packing \(\mathcal{A}\) and a real number \(N\), let \(M_{\mathcal{A}}(N)\) be the number of missing curvatures of \(\mathcal{A}\) up to \(N\). There are infinitely many primitive Apollonian circle packings \(\mathcal{A}\) such that \(\sqrt{N} = O(M_{\mathcal{A}}(N))\) as \(N\) tends to infinity. In other words, for these packings the number of missing curvatures up to \(N\) is \(\Omega(\sqrt{N})\).

public theorem_wanted theorem_1_3 : {A : PrimitiveApollonianCirclePacking |
    Real.sqrt =O[Filter.atTop] missingCurvatures A}.Infinite

Sources

• S. Haag, C. Kertzer, J. Rickards, and K. E. Stange, The local-global conjecture for Apollonian circle packings is false, Annals of Math, 200 (2) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_local_global_apollonian_circle_packings of the lean-eval benchmark.

Uses 2

Statement usesPrimitive Apollonian circle packing · Number of missing curvatures

17 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.