2607.20422v1 / SharpDistance.lean

all files

import Mathlib.NumberTheory.NumberField.CMField
import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
import Mathlib.NumberTheory.NumberField.Norm
import Mathlib.NumberTheory.NumberField.House
import Mathlib.Geometry.Euclidean.Projection
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

open scoped BigOperators ComplexConjugate InnerProductSpace

namespace SharpDistance

open NumberField

noncomputable section

/-! A self-contained formal proof of Theorem 1.1. -/

/-! The paper's naïve Euclidean objects. -/

abbrev Point := EuclideanSpace ℝ (Fin 2)

def point (x y : ℝ) : Point := !₂[x, y]

@[simp] lemma point_zero (x y : ℝ) : point x y 0 = x := by simp [point]
@[simp] lemma point_one (x y : ℝ) : point x y 1 = y := by simp [point]

structure RealLine where
  base : Point
  direction : Point
  direction_ne_zero : direction ≠ 0

def RealLine.carrier (ℓ : RealLine) : Set Point :=
  Set.range fun t : ℝ ↦ ℓ.base + t • ℓ.direction

def pointLineDist (p : Point) (ℓ : RealLine) : ℝ :=
  Metric.infDist p ℓ.carrier

lemma RealLine.base_mem (ℓ : RealLine) : ℓ.base ∈ ℓ.carrier :=
  ⟨0, by simp [RealLine.carrier]⟩

lemma RealLine.carrier_nonempty (ℓ : RealLine) : ℓ.carrier.Nonempty :=
  ⟨ℓ.base, ℓ.base_mem⟩

lemma pointLineDist_ge_inner_div_norm (p : Point) (ℓ : RealLine) (normal : Point)
    (hnormal : normal ≠ 0) (horth : ⟪(ℓ.direction), normal⟫_ℝ = 0) :
    |⟪p - ℓ.base, normal⟫_ℝ| / ‖normal‖ ≤ pointLineDist p ℓ := by
  rw [pointLineDist, Metric.le_infDist ℓ.carrier_nonempty]
  intro q hq
  obtain ⟨t, rfl⟩ := hq
  have hinner :
      ⟪p - (ℓ.base + t • ℓ.direction), normal⟫_ℝ =
        ⟪p - ℓ.base, normal⟫_ℝ := by
    rw [sub_add_eq_sub_sub, inner_sub_left, real_inner_smul_left, horth, mul_zero, sub_zero]
  rw [← hinner, dist_eq_norm]
  exact (div_le_iff₀ (norm_pos_iff.mpr hnormal)).2
    (abs_real_inner_le_norm (p - (ℓ.base + t • ℓ.direction)) normal)

lemma pointLineDist_self (ℓ : RealLine) : pointLineDist ℓ.base ℓ = 0 := by
  apply le_antisymm
  · exact Metric.infDist_le_dist_of_mem ℓ.base_mem |>.trans_eq (dist_self _)
  · exact Metric.infDist_nonneg

lemma pointLineDist_eq_zero_of_mem {p : Point} {ℓ : RealLine}
    (hp : p ∈ ℓ.carrier) : pointLineDist p ℓ = 0 := by
  apply le_antisymm
  · exact (Metric.infDist_le_dist_of_mem hp).trans_eq (dist_self _)
  · exact Metric.infDist_nonneg

variable {K : Type*} [Field K] [NumberField K] [NumberField.IsTotallyReal K]

def realEmbedding (φ : K →ₐ[ℚ] ℂ) : K →+* ℝ :=
  (NumberField.IsTotallyReal.complexEmbedding_isReal φ.toRingHom).embedding

lemma coe_realEmbedding (φ : K →ₐ[ℚ] ℂ) (x : K) :
    ((realEmbedding φ x : ℝ) : ℂ) = φ x :=
  ComplexEmbedding.IsReal.coe_embedding_apply
    (NumberField.IsTotallyReal.complexEmbedding_isReal φ.toRingHom) x

lemma trace_sq_eq_sum_real_embeddings (z : K) :
    ((Algebra.trace ℚ K (z ^ 2) : ℚ) : ℝ) =
      ∑ φ : K →ₐ[ℚ] ℂ, (realEmbedding φ z) ^ 2 := by
  have h := trace_eq_sum_embeddings (K := ℚ) (L := K) ℂ (x := z ^ 2)
  have h' :
      (((Algebra.trace ℚ K (z ^ 2) : ℚ) : ℝ) : ℂ) =
        ∑ φ : K →ₐ[ℚ] ℂ, (((realEmbedding φ z) ^ 2 : ℝ) : ℂ) := by
    calc
      _ = algebraMap ℚ ℂ (Algebra.trace ℚ K (z ^ 2)) := by simp
      _ = ∑ φ : K →ₐ[ℚ] ℂ, φ (z ^ 2) := h
      _ = ∑ φ : K →ₐ[ℚ] ℂ, (((realEmbedding φ z) ^ 2 : ℝ) : ℂ) := by
        apply Finset.sum_congr rfl
        intro φ _
        rw [map_pow, ← coe_realEmbedding]
        norm_num
  exact Complex.ofReal_injective (by simpa using h')

lemma trace_sq_eq_zero_iff (z : K) :
    Algebra.trace ℚ K (z ^ 2) = 0 ↔ z = 0 := by
  constructor
  · intro hz
    have hs : ∑ φ : K →ₐ[ℚ] ℂ, (realEmbedding φ z) ^ 2 = 0 := by
      rw [← trace_sq_eq_sum_real_embeddings]
      simp [hz]
    have hall : ∀ φ : K →ₐ[ℚ] ℂ, (realEmbedding φ z) ^ 2 = 0 := by
      intro φ
      exact (Finset.sum_eq_zero_iff_of_nonneg (fun _ _ ↦ sq_nonneg _)).mp hs φ
        (Finset.mem_univ φ)
    let φ : K →ₐ[ℚ] ℂ :=
      (Classical.choice (inferInstance : Nonempty (K →+* ℂ))).toRatAlgHom
    have : realEmbedding φ z = 0 := sq_eq_zero_iff.mp (hall φ)
    exact (realEmbedding φ).injective (by simpa using this)
  · rintro rfl
    simp

abbrev IntegerIndex (K : Type*) [Field K] [NumberField K] :=
  Module.Free.ChooseBasisIndex ℤ (𝓞 K)

lemma exists_integerBasis_trace_ne_zero (hd : 0 < Module.finrank ℚ K) :
    ∃ j : IntegerIndex K,
      Algebra.trace ℤ (𝓞 K) (NumberField.RingOfIntegers.basis K j) ≠ 0 := by
  by_contra h
  push_neg at h
  have ht : Algebra.trace ℤ (𝓞 K) = 0 := by
    apply (NumberField.RingOfIntegers.basis K).ext
    intro i
    simp [h i]
  have h1 := LinearMap.congr_fun ht (1 : 𝓞 K)
  have hrank : 0 < Module.finrank ℤ (𝓞 K) := by
    rwa [NumberField.RingOfIntegers.rank]
  have hone : Algebra.trace ℤ (𝓞 K) (1 : 𝓞 K) =
      (Module.finrank ℤ (𝓞 K) : ℤ) := by
    rw [Algebra.trace]
    have hlmul : (Algebra.lmul ℤ (𝓞 K)) 1 = 1 := by
      ext x
      simp
    rw [LinearMap.comp_apply]
    change LinearMap.trace ℤ (𝓞 K) ((Algebra.lmul ℤ (𝓞 K)) 1) = _
    rw [hlmul, LinearMap.trace_one]
  rw [hone] at h1
  simp only [LinearMap.zero_apply] at h1
  omega

structure TraceBasisData (K : Type*) [Field K] [NumberField K] where
  pivot : IntegerIndex K
  pivot_trace_ne_zero :
    Algebra.trace ℤ (𝓞 K) (NumberField.RingOfIntegers.basis K pivot) ≠ 0

def traceBasisData (hd : 0 < Module.finrank ℚ K) : TraceBasisData K :=
  ⟨(exists_integerBasis_trace_ne_zero hd).choose,
    (exists_integerBasis_trace_ne_zero hd).choose_spec⟩

abbrev TraceIndex (B : TraceBasisData K) := {i : IntegerIndex K // i ≠ B.pivot}

def traceGenerator (B : TraceBasisData K) (i : TraceIndex B) : 𝓞 K :=
  (Algebra.trace ℤ (𝓞 K) (NumberField.RingOfIntegers.basis K B.pivot)) •
      NumberField.RingOfIntegers.basis K i.1 -
    (Algebra.trace ℤ (𝓞 K) (NumberField.RingOfIntegers.basis K i.1)) •
      NumberField.RingOfIntegers.basis K B.pivot

lemma trace_traceGenerator (B : TraceBasisData K) (i : TraceIndex B) :
    Algebra.trace ℤ (𝓞 K) (traceGenerator B i) = 0 := by
  rw [traceGenerator, map_sub, map_zsmul, map_zsmul]
  simp [smul_eq_mul, mul_comm]

def linearCombo {ι : Type*} [Fintype ι] (g : ι → 𝓞 K) (c : ι → ℕ) : 𝓞 K :=
  ∑ i, (c i) • g i

lemma linearCombo_integerBasis_injective :
    Function.Injective
      (linearCombo (K := K) (NumberField.RingOfIntegers.basis K)) := by
  classical
  intro c c' h
  funext i
  have hi := congrArg (fun z : 𝓞 K ↦
    (NumberField.RingOfIntegers.basis K).repr z i) h
  simp only [linearCombo, map_sum, map_nsmul,
    (NumberField.RingOfIntegers.basis K).repr_self] at hi
  simpa [Finsupp.single_apply] using hi

lemma linearCombo_traceGenerator_injective (B : TraceBasisData K) :
    Function.Injective (linearCombo (K := K) (traceGenerator B)) := by
  classical
  intro c c' h
  funext i
  have hi := congrArg (fun z : 𝓞 K ↦
    (NumberField.RingOfIntegers.basis K).repr z i.1) h
  have ht := B.pivot_trace_ne_zero
  simp only [linearCombo, map_sum, map_nsmul, traceGenerator,
    map_sub, map_smul, (NumberField.RingOfIntegers.basis K).repr_self,
    Finsupp.single_apply] at hi
  have hcoe (x : TraceIndex B) : (x.1 = i.1) = (x = i) :=
    propext Subtype.ext_iff.symm
  simp [Finset.sum_apply, Finsupp.single_apply, i.2, hcoe] at hi
  exact hi.resolve_right ht

lemma card_integerIndex :
    Fintype.card (IntegerIndex K) = Module.finrank ℚ K := by
  rw [← Module.finrank_eq_card_basis (NumberField.RingOfIntegers.basis K),
    NumberField.RingOfIntegers.rank]

lemma card_traceIndex (B : TraceBasisData K) :
    Fintype.card (TraceIndex B) = Module.finrank ℚ K - 1 := by
  classical
  rw [← card_integerIndex (K := K)]
  simp [TraceIndex]

abbrev ACoeff (B : TraceBasisData K) (m : ℕ) :=
  TraceIndex B → Fin (m ^ 2 + 1)

abbrev YCoeff (K : Type*) [Field K] [NumberField K] (m : ℕ) :=
  IntegerIndex K → Fin (m + 1)

abbrev ArithmeticSource (B : TraceBasisData K) (m : ℕ) :=
  ACoeff B m × YCoeff K m

def aZero (B : TraceBasisData K) {m : ℕ} (c : ACoeff B m) : 𝓞 K :=
  linearCombo (traceGenerator B) fun i ↦ c i

def yHalf {m : ℕ} (c : YCoeff K m) : 𝓞 K :=
  linearCombo (NumberField.RingOfIntegers.basis K) fun i ↦ c i

def sourceA (B : TraceBasisData K) {m : ℕ} (s : ArithmeticSource B m) : 𝓞 K :=
  2 * aZero B s.1

def sourceY {B : TraceBasisData K} {m : ℕ} (s : ArithmeticSource B m) : 𝓞 K :=
  2 * yHalf s.2

def sourceX (B : TraceBasisData K) {m : ℕ} (s : ArithmeticSource B m) : 𝓞 K :=
  aZero B s.1 + 2 * yHalf s.2 ^ 2

lemma trace_aZero (B : TraceBasisData K) {m : ℕ} (c : ACoeff B m) :
    Algebra.trace ℤ (𝓞 K) (aZero B c) = 0 := by
  simp only [aZero, linearCombo, map_sum, map_nsmul, trace_traceGenerator,
    nsmul_zero, Finset.sum_const_zero]

lemma aZero_injective (B : TraceBasisData K) {m : ℕ} :
    Function.Injective (aZero B : ACoeff B m → 𝓞 K) := by
  intro c c' h
  have hc := linearCombo_traceGenerator_injective B h
  funext i
  apply Fin.ext
  exact congrFun hc i

lemma yHalf_injective {m : ℕ} :
    Function.Injective (yHalf (K := K) : YCoeff K m → 𝓞 K) := by
  intro c c' h
  have hc := linearCombo_integerBasis_injective h
  funext i
  apply Fin.ext
  exact congrFun hc i

lemma fieldTrace_aZero (B : TraceBasisData K) {m : ℕ} (c : ACoeff B m) :
    Algebra.trace ℚ K (aZero B c : K) = 0 := by
  rw [← Algebra.coe_trace_int]
  simp [trace_aZero]

lemma sourceQ_identity (B : TraceBasisData K) {m : ℕ} (s : ArithmeticSource B m) :
    2 * sourceX B s - sourceY s ^ 2 = sourceA B s := by
  simp [sourceX, sourceY, sourceA]
  ring

lemma sourceXY_injective (B : TraceBasisData K) {m : ℕ} :
    Function.Injective (fun s : ArithmeticSource B m ↦ (sourceX B s, sourceY s)) := by
  intro s t h
  have hy : yHalf s.2 = yHalf t.2 := by
    have := congrArg Prod.snd h
    simpa [sourceY] using (mul_left_cancel₀ (show (2 : 𝓞 K) ≠ 0 by norm_num) this)
  have hsnd : s.2 = t.2 := yHalf_injective hy
  have hx : aZero B s.1 = aZero B t.1 := by
    have := congrArg Prod.fst h
    simpa [sourceX, hy] using this
  have hfst : s.1 = t.1 := aZero_injective B hx
  exact Prod.ext hfst hsnd

lemma card_arithmeticSource (B : TraceBasisData K) (m : ℕ) :
    Fintype.card (ArithmeticSource B m) =
      (m ^ 2 + 1) ^ (Module.finrank ℚ K - 1) *
        (m + 1) ^ Module.finrank ℚ K := by
  classical
  simp [ArithmeticSource, ACoeff, YCoeff, Fintype.card_fun, card_traceIndex,
    card_integerIndex]

def sourceD (B : TraceBasisData K) {m : ℕ}
    (s t : ArithmeticSource B m) : 𝓞 K :=
  sourceX B s - sourceX B t + sourceY s * (sourceY t - sourceY s)

lemma sourceD_identity (B : TraceBasisData K) {m : ℕ}
    (s t : ArithmeticSource B m) :
    sourceD B s t =
      aZero B s.1 - aZero B t.1 - 2 * (yHalf t.2 - yHalf s.2) ^ 2 := by
  simp [sourceD, sourceX, sourceY]
  ring

lemma sourceD_ne_zero (B : TraceBasisData K) {m : ℕ}
    {s t : ArithmeticSource B m} (hst : s ≠ t) :
    sourceD B s t ≠ 0 := by
  intro hD
  have heqO :
      aZero B s.1 - aZero B t.1 =
        2 * (yHalf t.2 - yHalf s.2) ^ 2 := by
    rw [sourceD_identity] at hD
    linear_combination hD
  have heqK :
      (aZero B s.1 : K) - (aZero B t.1 : K) =
        2 * ((yHalf t.2 : K) - (yHalf s.2 : K)) ^ 2 := by
    have hc := congrArg (fun z : 𝓞 K ↦ (z : K)) heqO
    simpa only [map_sub, map_mul, map_pow, map_ofNat] using hc
  have htr := congrArg (Algebra.trace ℚ K) heqK
  have hsq :
      Algebra.trace ℚ K (((yHalf t.2 : K) - (yHalf s.2 : K)) ^ 2) = 0 := by
    rw [map_sub, fieldTrace_aZero, fieldTrace_aZero, sub_zero] at htr
    symm at htr
    rw [show (2 : K) * ((yHalf t.2 : K) - (yHalf s.2 : K)) ^ 2 =
      (2 : ℚ) • (((yHalf t.2 : K) - (yHalf s.2 : K)) ^ 2) by
        rw [Algebra.smul_def]
        norm_num,
      map_smul] at htr
    norm_num at htr ⊢
    exact htr
  have hhalfK : (yHalf t.2 : K) = (yHalf s.2 : K) := by
    have := (trace_sq_eq_zero_iff ((yHalf t.2 : K) - (yHalf s.2 : K))).mp hsq
    exact sub_eq_zero.mp this
  have hhalf : yHalf t.2 = yHalf s.2 := by
    exact_mod_cast hhalfK
  have hsnd : t.2 = s.2 := yHalf_injective hhalf
  have ha : aZero B s.1 = aZero B t.1 := by
    rw [hhalf] at heqO
    exact sub_eq_zero.mp (by simpa using heqO)
  have hfst : s.1 = t.1 := aZero_injective B ha
  apply hst
  exact Prod.ext hfst hsnd.symm

def aConstant (B : TraceBasisData K) : ℝ :=
  max 1 (∑ i : TraceIndex B, NumberField.house (traceGenerator B i : K))

def yConstant (K : Type*) [Field K] [NumberField K] : ℝ :=
  max 1 (∑ i : IntegerIndex K,
    NumberField.house (NumberField.RingOfIntegers.basis K i : K))

lemma one_le_aConstant (B : TraceBasisData K) : 1 ≤ aConstant B :=
  le_max_left _ _

lemma aConstant_pos (B : TraceBasisData K) : 0 < aConstant B :=
  zero_lt_one.trans_le (one_le_aConstant B)

lemma one_le_yConstant : 1 ≤ yConstant K :=
  le_max_left _ _

lemma yConstant_pos : 0 < yConstant K :=
  zero_lt_one.trans_le (one_le_yConstant (K := K))

lemma house_sub_le (x y : K) :
    NumberField.house (x - y) ≤ NumberField.house x + NumberField.house y := by
  simpa [sub_eq_add_neg, NumberField.house] using
    NumberField.house_add_le x (-y)

lemma house_linearCombo_le {ι : Type*} [Fintype ι]
    (g : ι → 𝓞 K) (c : ι → ℕ) (q : ℕ) (hc : ∀ i, c i ≤ q) :
    NumberField.house ((linearCombo g c : 𝓞 K) : K) ≤
      q * ∑ i, NumberField.house (g i : K) := by
  classical
  calc
    NumberField.house ((linearCombo g c : 𝓞 K) : K) =
        NumberField.house (∑ i, (c i) * (g i : K)) := by
          congr 1
          simp [linearCombo]
    _ ≤ ∑ i, NumberField.house ((c i) * (g i : K)) := by
      simpa using NumberField.house_sum_le_sum_house Finset.univ
        (fun i ↦ (c i) * (g i : K))
    _ = ∑ i, (c i : ℝ) * NumberField.house (g i : K) := by
      apply Finset.sum_congr rfl
      intro i _
      simpa using NumberField.house_nat_mul (g i : K) (c i)
    _ ≤ ∑ i, (q : ℝ) * NumberField.house (g i : K) := by
      apply Finset.sum_le_sum
      intro i hi
      apply mul_le_mul_of_nonneg_right
      · exact_mod_cast hc i
      · exact NumberField.house_nonneg _
    _ = q * ∑ i, NumberField.house (g i : K) := by
      rw [Finset.mul_sum]

lemma house_aZero_le (B : TraceBasisData K) {m : ℕ} (c : ACoeff B m) :
    NumberField.house (aZero B c : K) ≤ (m : ℝ) ^ 2 * aConstant B := by
  calc
    NumberField.house (aZero B c : K) ≤
        (m ^ 2 : ℕ) * ∑ i, NumberField.house (traceGenerator B i : K) := by
      apply house_linearCombo_le
      intro i
      omega
    _ ≤ (m : ℝ) ^ 2 * aConstant B := by
      norm_num [Nat.cast_pow]
      exact mul_le_mul_of_nonneg_left (le_max_right _ _) (sq_nonneg _)

lemma house_yHalf_le {m : ℕ} (c : YCoeff K m) :
    NumberField.house (yHalf c : K) ≤ (m : ℝ) * yConstant K := by
  calc
    NumberField.house (yHalf c : K) ≤
        m * ∑ i, NumberField.house (NumberField.RingOfIntegers.basis K i : K) := by
      apply house_linearCombo_le
      intro i
      omega
    _ ≤ (m : ℝ) * yConstant K := by
      apply mul_le_mul_of_nonneg_left (le_max_right _ _) (Nat.cast_nonneg _)

lemma house_sourceY_le (B : TraceBasisData K) {m : ℕ} (s : ArithmeticSource B m) :
    NumberField.house (sourceY s : K) ≤
      2 * yConstant K * m := by
  calc
    NumberField.house (sourceY s : K) =
        NumberField.house (2 * (yHalf s.2 : K)) := by
      simp only [sourceY, map_mul, map_ofNat]
    _ = 2 * NumberField.house (yHalf s.2 : K) := by
      simpa using NumberField.house_nat_mul (yHalf s.2 : K) 2
    _ ≤ 2 * ((m : ℝ) * yConstant K) := by
      gcongr
      exact house_yHalf_le s.2
    _ = 2 * yConstant K * m := by ring

lemma house_sourceX_le (B : TraceBasisData K) {m : ℕ} (s : ArithmeticSource B m) :
    NumberField.house (sourceX B s : K) ≤
      (aConstant B + 2 * yConstant K ^ 2) * m ^ 2 := by
  calc
    NumberField.house (sourceX B s : K) =
        NumberField.house ((aZero B s.1 : K) + 2 * (yHalf s.2 : K) ^ 2) := by
      simp only [sourceX, map_add, map_mul, map_pow, map_ofNat]
    _ ≤ NumberField.house (aZero B s.1 : K) +
        NumberField.house (2 * (yHalf s.2 : K) ^ 2) :=
      NumberField.house_add_le _ _
    _ ≤ (m : ℝ) ^ 2 * aConstant B +
        2 * (NumberField.house (yHalf s.2 : K) ^ 2) := by
      gcongr
      · exact house_aZero_le B s.1
      · calc
          NumberField.house (2 * (yHalf s.2 : K) ^ 2) =
              2 * NumberField.house ((yHalf s.2 : K) ^ 2) := by
            simpa using NumberField.house_nat_mul ((yHalf s.2 : K) ^ 2) 2
          _ ≤ 2 * NumberField.house (yHalf s.2 : K) ^ 2 := by
            gcongr
            exact NumberField.house_pow_le (yHalf s.2 : K) 2
    _ ≤ (m : ℝ) ^ 2 * aConstant B +
        2 * (((m : ℝ) * yConstant K) ^ 2) := by
      have hh := house_yHalf_le s.2
      have hhn := NumberField.house_nonneg (yHalf s.2 : K)
      have hmn : 0 ≤ (m : ℝ) * yConstant K :=
        mul_nonneg (Nat.cast_nonneg _) (le_trans (by norm_num) one_le_yConstant)
      nlinarith [sq_nonneg
        (NumberField.house (yHalf s.2 : K) - (m : ℝ) * yConstant K)]
    _ = (aConstant B + 2 * yConstant K ^ 2) * m ^ 2 := by ring

lemma house_sourceD_le (B : TraceBasisData K) {m : ℕ}
    (s t : ArithmeticSource B m) :
    NumberField.house (sourceD B s t : K) ≤
      (2 * aConstant B + 12 * yConstant K ^ 2) * m ^ 2 := by
  let CX : ℝ := aConstant B + 2 * yConstant K ^ 2
  let CY : ℝ := 2 * yConstant K
  have hXs := house_sourceX_le B s
  have hXt := house_sourceX_le B t
  have hYs := house_sourceY_le B s
  have hYt := house_sourceY_le B t
  have hCY : 0 ≤ CY := by
    dsimp [CY]
    exact mul_nonneg (by norm_num) (zero_le_one.trans one_le_yConstant)
  have hCX : 0 ≤ CX := by
    dsimp [CX]
    exact add_nonneg (zero_le_one.trans (one_le_aConstant B))
      (mul_nonneg (by norm_num) (sq_nonneg _))
  have hYdiff :
      NumberField.house ((sourceY t : K) - (sourceY s : K)) ≤ 2 * CY * m := by
    calc
      _ ≤ NumberField.house (sourceY t : K) +
          NumberField.house (sourceY s : K) := house_sub_le _ _
      _ ≤ CY * m + CY * m := by
        dsimp [CY]
        exact add_le_add hYt hYs
      _ = 2 * CY * m := by ring
  change NumberField.house
    ((sourceX B s : K) - (sourceX B t : K) +
      (sourceY s : K) * ((sourceY t : K) - (sourceY s : K))) ≤ _
  calc
    _ ≤ NumberField.house ((sourceX B s : K) - (sourceX B t : K)) +
        NumberField.house ((sourceY s : K) *
          ((sourceY t : K) - (sourceY s : K))) :=
      NumberField.house_add_le _ _
    _ ≤ (NumberField.house (sourceX B s : K) +
          NumberField.house (sourceX B t : K)) +
        NumberField.house (sourceY s : K) *
          NumberField.house ((sourceY t : K) - (sourceY s : K)) := by
      exact add_le_add (house_sub_le _ _) (NumberField.house_mul_le _ _)
    _ ≤ (CX * m ^ 2 + CX * m ^ 2) + (CY * m) * (2 * CY * m) := by
      apply add_le_add
      · exact add_le_add hXs hXt
      · exact mul_le_mul hYs hYdiff (NumberField.house_nonneg _) (by positivity)
    _ = (2 * aConstant B + 12 * yConstant K ^ 2) * m ^ 2 := by
      dsimp [CX, CY]
      ring

def complexify (σ : K →+* ℝ) : K →+* ℂ :=
  Complex.ofRealHom.comp σ

lemma abs_embedding_le_house (σ : K →+* ℝ) (z : K) :
    |σ z| ≤ NumberField.house z := by
  have h := NumberField.norm_embedding_le_house z (complexify σ)
  simpa [complexify, Real.norm_eq_abs] using h

lemma one_le_abs_norm_of_integer {z : 𝓞 K} (hz : z ≠ 0) :
    (1 : ℝ) ≤ |Algebra.norm ℚ (z : K)| := by
  rw [← Algebra.coe_norm_int, ← Int.cast_one, ← Int.cast_abs, Rat.cast_intCast,
    Int.cast_le]
  exact Int.one_le_abs (Algebra.norm_ne_zero_iff.mpr hz)

lemma sourceD_norm_product_lower (σ : K →+* ℝ) (B : TraceBasisData K)
    {m : ℕ} {s t : ArithmeticSource B m} (hst : s ≠ t) :
    1 ≤ |σ (sourceD B s t : K)| *
      (((2 * aConstant B + 12 * yConstant K ^ 2) * m ^ 2) ^
        (Module.finrank ℚ K - 1)) := by
  let D : 𝓞 K := sourceD B s t
  let H : ℝ := (2 * aConstant B + 12 * yConstant K ^ 2) * m ^ 2
  have hD : D ≠ 0 := sourceD_ne_zero B hst
  have hnorm : (1 : ℝ) ≤ ‖Algebra.norm ℚ (D : K)‖ := by
    have ha := one_le_abs_norm_of_integer (K := K) hD
    rw [← Rat.norm_cast_real, Real.norm_eq_abs]
    simpa only [Rat.cast_abs] using ha
  have hhouse : NumberField.house (D : K) ≤ H := by
    exact house_sourceD_le B s t
  have hH : 0 ≤ H := by
    dsimp [H]
    apply mul_nonneg
    · exact add_nonneg
        (mul_nonneg (by norm_num) (zero_le_one.trans (one_le_aConstant B)))
        (mul_nonneg (by norm_num) (sq_nonneg _))
    · exact sq_nonneg _
  have hnormUpper :=
    NumberField.norm_norm_le_norm_mul_house_pow (D : K) (complexify σ)
  calc
    1 ≤ ‖Algebra.norm ℚ (D : K)‖ := hnorm
    _ ≤ ‖complexify σ (D : K)‖ *
        NumberField.house (D : K) ^ (Module.finrank ℚ K - 1) := hnormUpper
    _ ≤ ‖complexify σ (D : K)‖ * H ^ (Module.finrank ℚ K - 1) := by
      apply mul_le_mul_of_nonneg_left
      · exact pow_le_pow_left₀ (NumberField.house_nonneg _) hhouse _
      · exact norm_nonneg _
    _ = |σ (sourceD B s t : K)| *
        (((2 * aConstant B + 12 * yConstant K ^ 2) * m ^ 2) ^
          (Module.finrank ℚ K - 1)) := by
      simp [D, H, complexify, Real.norm_eq_abs]

lemma inner_point (a b c d : ℝ) :
    ⟪point a b, point c d⟫_ℝ = a * c + b * d := by
  simp [point, PiLp.inner_apply, Fin.sum_univ_two]
  ring

lemma norm_point_le (a b : ℝ) :
    ‖point a b‖ ≤ |a| + |b| := by
  have hsplit : point a b = point a 0 + point 0 b := by
    ext i
    fin_cases i <;> simp
  rw [hsplit]
  calc
    _ ≤ ‖point a 0‖ + ‖point 0 b‖ := norm_add_le _ _
    _ = |a| + |b| := by
      simp [point, EuclideanSpace.norm_eq, Fin.sum_univ_two, Real.norm_eq_abs,
        Real.sqrt_sq_eq_abs]

def InUnitSquare (p : Point) : Prop :=
  0 ≤ p 0 ∧ p 0 ≤ 1 ∧ 0 ≤ p 1 ∧ p 1 ≤ 1

lemma scaled_mem_Icc {x R : ℝ} (hR : 0 < R) (hx : |x| ≤ R) :
    0 ≤ (x + R) / (2 * R) ∧ (x + R) / (2 * R) ≤ 1 := by
  constructor
  · apply div_nonneg
    · linarith [neg_abs_le x]
    · positivity
  · rw [div_le_one (by positivity)]
    linarith [le_abs_self x]

@[simp] lemma point_add (a b c d : ℝ) :
    point a b + point c d = point (a + c) (b + d) := by
  ext i
  fin_cases i <;> simp

@[simp] lemma point_sub (a b c d : ℝ) :
    point a b - point c d = point (a - c) (b - d) := by
  ext i
  fin_cases i <;> simp

@[simp] lemma point_smul (r a b : ℝ) :
    r • point a b = point (r * a) (r * b) := by
  ext i
  fin_cases i <;> simp

def yScale (m : ℕ) : ℝ :=
  2 * yConstant K * (m + 1)

def xScale (B : TraceBasisData K) (m : ℕ) : ℝ :=
  (aConstant B + 2 * yConstant K ^ 2) * (m + 1) ^ 2

lemma yScale_pos (m : ℕ) : 0 < yScale (K := K) m := by
  unfold yScale
  exact mul_pos (mul_pos (by norm_num) (yConstant_pos (K := K))) (by positivity)

lemma xScale_pos (B : TraceBasisData K) (m : ℕ) : 0 < xScale B m := by
  unfold xScale
  apply mul_pos
  · exact add_pos_of_pos_of_nonneg (aConstant_pos B)
      (mul_nonneg (by norm_num) (sq_nonneg _))
  · positivity

def scaledPoint (σ : K →+* ℝ) (B : TraceBasisData K) {m : ℕ}
    (s : ArithmeticSource B m) : Point :=
  point
    ((σ (sourceY s : K) + yScale (K := K) m) / (2 * yScale (K := K) m))
    ((σ (sourceX B s : K) + xScale B m) / (2 * xScale B m))

def scaledDirection (σ : K →+* ℝ) (B : TraceBasisData K) {m : ℕ}
    (s : ArithmeticSource B m) : Point :=
  point (xScale B m) (yScale (K := K) m * σ (sourceY s : K))

def scaledNormal (σ : K →+* ℝ) (B : TraceBasisData K) {m : ℕ}
    (s : ArithmeticSource B m) : Point :=
  point (-(yScale (K := K) m * σ (sourceY s : K))) (xScale B m)

def scaledLine (σ : K →+* ℝ) (B : TraceBasisData K) {m : ℕ}
    (s : ArithmeticSource B m) : RealLine where
  base := scaledPoint σ B s
  direction := scaledDirection σ B s
  direction_ne_zero := by
    intro h
    have h0 := congrArg (fun p : Point ↦ p 0) h
    simp [scaledDirection] at h0
    exact (xScale_pos B m).ne' h0

lemma scaledPoint_mem_unitSquare (σ : K →+* ℝ) (B : TraceBasisData K)
    {m : ℕ} (s : ArithmeticSource B m) :
    InUnitSquare (scaledPoint σ B s) := by
  have hy0 : |σ (sourceY s : K)| ≤ yScale (K := K) m := by
    calc
      _ ≤ NumberField.house (sourceY s : K) := abs_embedding_le_house σ _
      _ ≤ 2 * yConstant K * m := house_sourceY_le B s
      _ ≤ 2 * yConstant K * (m + 1) := by
        apply mul_le_mul_of_nonneg_left
        · exact_mod_cast Nat.le_succ m
        · exact mul_nonneg (by norm_num)
            (zero_le_one.trans (one_le_yConstant (K := K)))
      _ = _ := rfl
  have hx0 : |σ (sourceX B s : K)| ≤ xScale B m := by
    calc
      _ ≤ NumberField.house (sourceX B s : K) := abs_embedding_le_house σ _
      _ ≤ (aConstant B + 2 * yConstant K ^ 2) * m ^ 2 :=
        house_sourceX_le B s
      _ ≤ (aConstant B + 2 * yConstant K ^ 2) * (m + 1) ^ 2 := by
        apply mul_le_mul_of_nonneg_left
        · exact pow_le_pow_left₀ (Nat.cast_nonneg _)
            (by exact_mod_cast Nat.le_succ m) 2
        · exact add_nonneg (zero_le_one.trans (one_le_aConstant B))
            (mul_nonneg (by norm_num) (sq_nonneg _))
      _ = _ := rfl
  have hy := scaled_mem_Icc (yScale_pos (K := K) m) hy0
  have hx := scaled_mem_Icc (xScale_pos B m) hx0
  exact ⟨hy.1, hy.2, hx.1, hx.2⟩

lemma scaled_orthogonal (σ : K →+* ℝ) (B : TraceBasisData K)
    {m : ℕ} (s : ArithmeticSource B m) :
    ⟪scaledDirection σ B s, scaledNormal σ B s⟫_ℝ = 0 := by
  rw [scaledDirection, scaledNormal, inner_point]
  ring

lemma scaledNormal_ne_zero (σ : K →+* ℝ) (B : TraceBasisData K)
    {m : ℕ} (s : ArithmeticSource B m) :
    scaledNormal σ B s ≠ 0 := by
  intro h
  have h1 := congrArg (fun p : Point ↦ p 1) h
  simp [scaledNormal] at h1
  exact (xScale_pos B m).ne' h1

lemma scaled_inner_eq (σ : K →+* ℝ) (B : TraceBasisData K)
    {m : ℕ} (s t : ArithmeticSource B m) :
    ⟪scaledPoint σ B t - scaledPoint σ B s, scaledNormal σ B s⟫_ℝ =
      -(σ (sourceD B s t : K)) / 2 := by
  simp only [scaledPoint, scaledNormal]
  rw [point_sub, inner_point]
  field_simp [(yScale_pos (K := K) m).ne', (xScale_pos B m).ne']
  simp only [sourceD, map_add, map_sub, map_mul]
  ring

lemma scaledNormal_norm_le (σ : K →+* ℝ) (B : TraceBasisData K)
    {m : ℕ} (s : ArithmeticSource B m) :
    ‖scaledNormal σ B s‖ ≤
      (aConstant B + 6 * yConstant K ^ 2) * (m + 1) ^ 2 := by
  calc
    _ ≤ |-(yScale (K := K) m * σ (sourceY s : K))| + |xScale B m| :=
      norm_point_le _ _
    _ = yScale (K := K) m * |σ (sourceY s : K)| + xScale B m := by
      rw [abs_neg, abs_mul, abs_of_pos (yScale_pos (K := K) m),
        abs_of_pos (xScale_pos B m)]
    _ ≤ yScale (K := K) m * yScale (K := K) m + xScale B m := by
      have hyabs : |σ (sourceY s : K)| ≤ yScale (K := K) m := by
        calc
            _ ≤ NumberField.house (sourceY s : K) := abs_embedding_le_house σ _
            _ ≤ 2 * yConstant K * m := house_sourceY_le B s
            _ ≤ yScale (K := K) m := by
              unfold yScale
              apply mul_le_mul_of_nonneg_left
              · exact_mod_cast Nat.le_succ m
              · exact mul_nonneg (by norm_num)
                  (zero_le_one.trans (one_le_yConstant (K := K)))
      exact add_le_add
        (mul_le_mul_of_nonneg_left hyabs (yScale_pos (K := K) m).le) le_rfl
    _ = (aConstant B + 6 * yConstant K ^ 2) * (m + 1) ^ 2 := by
      simp [yScale, xScale]
      ring

lemma scaled_offDiag_distance (σ : K →+* ℝ) (B : TraceBasisData K)
    {m : ℕ} (hm : 0 < m) {s t : ArithmeticSource B m} (hst : s ≠ t) :
    (2 * ((aConstant B + 6 * yConstant K ^ 2) * (m + 1) ^ 2) *
      (((2 * aConstant B + 12 * yConstant K ^ 2) * m ^ 2) ^
        (Module.finrank ℚ K - 1)))⁻¹ ≤
      pointLineDist (scaledPoint σ B t) (scaledLine σ B s) := by
  let A : ℝ := |σ (sourceD B s t : K)|
  let N : ℝ := ‖scaledNormal σ B s‖
  let G : ℝ := (aConstant B + 6 * yConstant K ^ 2) * (m + 1) ^ 2
  let H : ℝ := (2 * aConstant B + 12 * yConstant K ^ 2) * m ^ 2
  let P : ℝ := H ^ (Module.finrank ℚ K - 1)
  have hA : 0 ≤ A := abs_nonneg _
  have hN : 0 < N := norm_pos_iff.mpr (scaledNormal_ne_zero σ B s)
  have hG : 0 < G := by
    dsimp [G]
    apply mul_pos
    · exact add_pos_of_pos_of_nonneg (aConstant_pos B)
        (mul_nonneg (by norm_num) (sq_nonneg _))
    · positivity
  have hH : 0 < H := by
    dsimp [H]
    apply mul_pos
    · exact add_pos_of_pos_of_nonneg
        (mul_pos (by norm_num) (aConstant_pos B))
        (mul_nonneg (by norm_num) (sq_nonneg _))
    · positivity
  have hP : 0 < P := pow_pos hH _
  have hNG : N ≤ G := scaledNormal_norm_le σ B s
  have hprod : 1 ≤ A * P := sourceD_norm_product_lower σ B hst
  have hPinvA : 1 / P ≤ A := by
    apply (div_le_iff₀ hP).2
    simpa [A, P, H, mul_comm] using hprod
  have hgeom :
      A / (2 * N) ≤ pointLineDist (scaledPoint σ B t) (scaledLine σ B s) := by
    have h := pointLineDist_ge_inner_div_norm
      (scaledPoint σ B t) (scaledLine σ B s) (scaledNormal σ B s)
      (scaledNormal_ne_zero σ B s) (scaled_orthogonal σ B s)
    change
      |⟪scaledPoint σ B t - scaledPoint σ B s, scaledNormal σ B s⟫_ℝ| /
        ‖scaledNormal σ B s‖ ≤
          pointLineDist (scaledPoint σ B t) (scaledLine σ B s) at h
    rw [scaled_inner_eq] at h
    simpa [A, N, abs_div, div_div] using h
  calc
    (2 * G * P)⁻¹ = (1 / P) / (2 * G) := by
      field_simp [hG.ne', hP.ne']
    _ ≤ A / (2 * G) := by
      exact div_le_div_of_nonneg_right hPinvA (by positivity)
    _ ≤ A / (2 * N) := by
      exact div_le_div_of_nonneg_left hA (by positivity) (by linarith)
    _ ≤ pointLineDist (scaledPoint σ B t) (scaledLine σ B s) := hgeom

structure PLConfiguration (n : ℕ) where
  points : Fin n → Point
  lines : Fin n → RealLine
  points_mem : ∀ i, InUnitSquare (points i)
  incident : ∀ i, points i ∈ (lines i).carrier

def PLConfiguration.Separated {n : ℕ} (C : PLConfiguration n) (δ : ℝ) : Prop :=
  ∀ i j, i ≠ j → δ ≤ pointLineDist (C.points i) (C.lines j)

lemma PLConfiguration.points_injective_of_separated {n : ℕ}
    (C : PLConfiguration n) {δ : ℝ} (hδ : 0 < δ) (h : C.Separated δ) :
    Function.Injective C.points := by
  intro i j hij
  by_contra hne
  have hj : C.points i ∈ (C.lines j).carrier := by
    simpa [hij] using C.incident j
  have hz := pointLineDist_eq_zero_of_mem hj
  have hsep := h i j hne
  linarith

lemma PLConfiguration.lines_injective_of_separated {n : ℕ}
    (C : PLConfiguration n) {δ : ℝ} (hδ : 0 < δ) (h : C.Separated δ) :
    Function.Injective C.lines := by
  intro i j hij
  by_contra hne
  have hi := C.incident i
  rw [hij] at hi
  have hz := pointLineDist_eq_zero_of_mem hi
  have hsep := h i j hne
  linarith

lemma card_arithmeticSource_lower (B : TraceBasisData K) (m : ℕ)
    (hd : 0 < Module.finrank ℚ K) :
    m ^ (3 * Module.finrank ℚ K - 2) ≤
      Fintype.card (ArithmeticSource B m) := by
  let d := Module.finrank ℚ K
  rw [card_arithmeticSource]
  calc
    m ^ (3 * d - 2) = (m ^ 2) ^ (d - 1) * m ^ d := by
      rw [← pow_mul, ← pow_add]
      congr 1
      omega
    _ ≤ (m ^ 2 + 1) ^ (d - 1) * (m + 1) ^ d := by
      gcongr <;> omega

def sourceEmbedding (B : TraceBasisData K) (m n : ℕ)
    (hcard : n ≤ Fintype.card (ArithmeticSource B m)) :
    Fin n ↪ ArithmeticSource B m :=
  Classical.choice <| Function.Embedding.nonempty_of_card_le <| by
    simpa using hcard

def selectedConfiguration (σ : K →+* ℝ) (B : TraceBasisData K)
    (m n : ℕ) (hcard : n ≤ Fintype.card (ArithmeticSource B m)) :
    PLConfiguration n where
  points i := scaledPoint σ B (sourceEmbedding B m n hcard i)
  lines i := scaledLine σ B (sourceEmbedding B m n hcard i)
  points_mem i := scaledPoint_mem_unitSquare σ B _
  incident i := (scaledLine σ B _).base_mem

lemma selectedConfiguration_separated (σ : K →+* ℝ) (B : TraceBasisData K)
    {m n : ℕ} (hm : 0 < m) (hcard : n ≤ Fintype.card (ArithmeticSource B m)) :
    (selectedConfiguration σ B m n hcard).Separated
      (2 * ((aConstant B + 6 * yConstant K ^ 2) * (m + 1) ^ 2) *
        (((2 * aConstant B + 12 * yConstant K ^ 2) * m ^ 2) ^
          (Module.finrank ℚ K - 1)))⁻¹ := by
  intro i j hij
  apply scaled_offDiag_distance σ B hm
  exact fun h ↦ hij ((sourceEmbedding B m n hcard).injective h.symm)

def constructionConstant (B : TraceBasisData K) : ℝ :=
  8 * (aConstant B + 6 * yConstant K ^ 2) *
    (2 * aConstant B + 12 * yConstant K ^ 2) ^
      (Module.finrank ℚ K - 1)

lemma constructionConstant_pos (B : TraceBasisData K) :
    0 < constructionConstant B := by
  unfold constructionConstant
  apply mul_pos
  · exact mul_pos (by norm_num) <| add_pos_of_pos_of_nonneg
      (aConstant_pos B) (mul_nonneg (by norm_num) (sq_nonneg _))
  · exact pow_pos (add_pos_of_pos_of_nonneg
      (mul_pos (by norm_num) (aConstant_pos B))
      (mul_nonneg (by norm_num) (sq_nonneg _))) _

lemma construction_denominator_le (B : TraceBasisData K) {m : ℕ}
    (hm : 0 < m) (hd : 0 < Module.finrank ℚ K) :
    2 * ((aConstant B + 6 * yConstant K ^ 2) * (m + 1) ^ 2) *
        (((2 * aConstant B + 12 * yConstant K ^ 2) * m ^ 2) ^
          (Module.finrank ℚ K - 1)) ≤
      constructionConstant B * (m : ℝ) ^ (2 * Module.finrank ℚ K) := by
  let d := Module.finrank ℚ K
  let G := aConstant B + 6 * yConstant K ^ 2
  let H := 2 * aConstant B + 12 * yConstant K ^ 2
  have hG : 0 ≤ G := by
    dsimp [G]
    exact add_nonneg (zero_le_one.trans (one_le_aConstant B))
      (mul_nonneg (by norm_num) (sq_nonneg _))
  have hH : 0 ≤ H := by
    dsimp [H]
    exact add_nonneg
      (mul_nonneg (by norm_num) (zero_le_one.trans (one_le_aConstant B)))
      (mul_nonneg (by norm_num) (sq_nonneg _))
  have hm1 : ((m + 1 : ℕ) : ℝ) ≤ 2 * m := by
    have hmR : (1 : ℝ) ≤ m := by exact_mod_cast hm
    norm_num
    linarith
  have hm1' : (m : ℝ) + 1 ≤ 2 * (m : ℝ) := by
    simpa only [Nat.cast_add, Nat.cast_one] using hm1
  calc
    2 * (G * (m + 1) ^ 2) * (H * m ^ 2) ^ (d - 1) ≤
        2 * (G * (2 * m) ^ 2) * (H * m ^ 2) ^ (d - 1) := by
      gcongr
    _ = constructionConstant B * (m : ℝ) ^ (2 * d) := by
      have hexp : 2 + 2 * (d - 1) = 2 * d := by omega
      have hmpow : ((m : ℝ) ^ 2) ^ (d - 1) = m ^ (2 * (d - 1)) := by
        rw [← pow_mul]
      have hcombine :
          (m : ℝ) ^ 2 * ((m : ℝ) ^ 2) ^ (d - 1) = m ^ (2 * d) := by
        rw [hmpow, ← pow_add, hexp]
      calc
        _ = 8 * G * H ^ (d - 1) *
            ((m : ℝ) ^ 2 * ((m : ℝ) ^ 2) ^ (d - 1)) := by
          rw [mul_pow]
          ring
        _ = 8 * G * H ^ (d - 1) * (m : ℝ) ^ (2 * d) := by rw [hcombine]
        _ = _ := by simp [constructionConstant, G, H, d]

lemma selectedConfiguration_simple_separated (σ : K →+* ℝ)
    (B : TraceBasisData K) {m n : ℕ} (hm : 0 < m)
    (hd : 0 < Module.finrank ℚ K)
    (hcard : n ≤ Fintype.card (ArithmeticSource B m)) :
    (selectedConfiguration σ B m n hcard).Separated
      (constructionConstant B * (m : ℝ) ^ (2 * Module.finrank ℚ K))⁻¹ := by
  have hraw := selectedConfiguration_separated σ B hm hcard
  intro i j hij
  apply le_trans ?_ (hraw i j hij)
  have hmR : (0 : ℝ) < m := by exact_mod_cast hm
  have hG : 0 < aConstant B + 6 * yConstant K ^ 2 :=
    add_pos_of_pos_of_nonneg (aConstant_pos B)
      (mul_nonneg (by norm_num) (sq_nonneg _))
  have hH : 0 < 2 * aConstant B + 12 * yConstant K ^ 2 :=
    add_pos_of_pos_of_nonneg
      (mul_pos (by norm_num) (aConstant_pos B))
      (mul_nonneg (by norm_num) (sq_nonneg _))
  have hsimple :
      0 < constructionConstant B * (m : ℝ) ^ (2 * Module.finrank ℚ K) :=
    mul_pos (constructionConstant_pos B) (pow_pos hmR _)
  have hrawpos :
      0 < 2 * ((aConstant B + 6 * yConstant K ^ 2) * (m + 1) ^ 2) *
        (((2 * aConstant B + 12 * yConstant K ^ 2) * m ^ 2) ^
          (Module.finrank ℚ K - 1)) := by
    apply mul_pos
    · exact mul_pos (by norm_num) <| mul_pos hG (pow_pos (by positivity) _)
    · exact pow_pos (mul_pos hH (pow_pos hmR _)) _
  exact (inv_le_inv₀ hsimple hrawpos).2
    (construction_denominator_le B hm hd)

theorem eventually_configuration_of_fixed_field (σ : K →+* ℝ)
    (B : TraceBasisData K) (α : ℝ)
    (hd : 1 < Module.finrank ℚ K)
    (hα : (2 * Module.finrank ℚ K : ℝ) /
        (3 * Module.finrank ℚ K - 2 : ℕ) < α) :
    ∃ n₀ : ℕ, ∀ n ≥ n₀, ∃ C : PLConfiguration n,
      C.Separated ((n : ℝ) ^ (-α)) := by
  let d := Module.finrank ℚ K
  let e := 3 * d - 2
  let θ : ℝ := (2 * d : ℕ) / (e : ℕ)
  let γ := α - θ
  let C₂ := constructionConstant B * (2 : ℝ) ^ (2 * d)
  have he : 0 < e := by
    dsimp [e, d]
    omega
  have hθ : θ < α := by
    simpa [θ, e, d] using hα
  have hγ : 0 < γ := sub_pos.mpr hθ
  have hC₂ : 0 < C₂ :=
    mul_pos (constructionConstant_pos B) (pow_pos (by norm_num) _)
  have htend :
      Filter.Tendsto (fun n : ℕ => (n : ℝ) ^ γ)
        Filter.atTop Filter.atTop :=
    (tendsto_rpow_atTop hγ).comp tendsto_natCast_atTop_atTop
  have hev : ∀ᶠ n : ℕ in Filter.atTop, C₂ ≤ (n : ℝ) ^ γ :=
    Filter.tendsto_atTop.mp htend C₂
  obtain ⟨n₁, hn₁⟩ := Filter.eventually_atTop.mp hev
  refine ⟨max n₁ 1, ?_⟩
  intro n hn
  have hn₁' : n₁ ≤ n := (le_max_left _ _).trans hn
  have hn1 : 1 ≤ n := (le_max_right _ _).trans hn
  have hnR : (0 : ℝ) < n := by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hn1)
  let x : ℝ := (n : ℝ) ^ ((e : ℝ)⁻¹)
  let m : ℕ := ⌈x⌉₊
  have heR : (0 : ℝ) < e := by exact_mod_cast he
  have hx : 0 < x := Real.rpow_pos_of_pos hnR _
  have hm : 0 < m := (Nat.ceil_pos).2 hx
  have hx_le_m : x ≤ (m : ℝ) := by
    exact Nat.le_ceil x
  have hx_one : 1 ≤ x := by
    dsimp [x]
    exact Real.one_le_rpow (by exact_mod_cast hn1) (inv_nonneg.mpr heR.le)
  have hm_lt : (m : ℝ) < x + 1 := Nat.ceil_lt_add_one hx.le
  have hm_le_two_x : (m : ℝ) ≤ 2 * x := by
    linarith
  have hx_pow : x ^ e = (n : ℝ) := by
    dsimp [x]
    exact Real.rpow_inv_natCast_pow hnR.le (Nat.ne_of_gt he)
  have hn_le_mpow : n ≤ m ^ e := by
    have hp : x ^ e ≤ (m : ℝ) ^ e :=
      pow_le_pow_left₀ hx.le hx_le_m e
    have hp' : (n : ℝ) ≤ ((m ^ e : ℕ) : ℝ) := by
      simpa only [hx_pow, Nat.cast_pow] using hp
    exact_mod_cast hp'
  have hcard : n ≤ Fintype.card (ArithmeticSource B m) :=
    hn_le_mpow.trans <| card_arithmeticSource_lower B m (by omega : 0 < d)
  let C := selectedConfiguration σ B m n hcard
  refine ⟨C, ?_⟩
  have hsep :
      C.Separated (constructionConstant B * (m : ℝ) ^ (2 * d))⁻¹ := by
    exact selectedConfiguration_simple_separated σ B hm (by omega : 0 < d) hcard
  have hx_theta : x ^ (2 * d) = (n : ℝ) ^ θ := by
    rw [← Real.rpow_natCast]
    dsimp [x, θ]
    rw [← Real.rpow_mul hnR.le]
    congr 1
    field_simp
  have hmpow :
      (m : ℝ) ^ (2 * d) ≤ (2 : ℝ) ^ (2 * d) * (n : ℝ) ^ θ := by
    calc
      (m : ℝ) ^ (2 * d) ≤ (2 * x) ^ (2 * d) :=
        pow_le_pow_left₀ (by positivity) hm_le_two_x _
      _ = (2 : ℝ) ^ (2 * d) * x ^ (2 * d) := by rw [mul_pow]
      _ = _ := by rw [hx_theta]
  have hden :
      constructionConstant B * (m : ℝ) ^ (2 * d) ≤
        (n : ℝ) ^ α := by
    calc
      constructionConstant B * (m : ℝ) ^ (2 * d) ≤
          C₂ * (n : ℝ) ^ θ := by
        dsimp [C₂]
        nlinarith [constructionConstant_pos B, hmpow,
          Real.rpow_pos_of_pos hnR θ]
      _ ≤ (n : ℝ) ^ γ * (n : ℝ) ^ θ := by
        exact mul_le_mul_of_nonneg_right (hn₁ n hn₁')
          (Real.rpow_nonneg hnR.le θ)
      _ = (n : ℝ) ^ α := by
        rw [← Real.rpow_add hnR]
        congr 1
        dsimp [γ]
        ring
  intro i j hij
  have hposden :
      0 < constructionConstant B * (m : ℝ) ^ (2 * d) :=
    mul_pos (constructionConstant_pos B) (pow_pos (by exact_mod_cast hm) _)
  have hposn : 0 < (n : ℝ) ^ α := Real.rpow_pos_of_pos hnR α
  rw [Real.rpow_neg hnR.le]
  exact le_trans ((inv_le_inv₀ hposn hposden).2 hden) (hsep i j hij)

end

lemma realCyclotomicField_finrank (k : ℕ) :
    let L := CyclotomicField (2 ^ (k + 2)) ℚ
    let K := maximalRealSubfield L
    Module.finrank ℚ K = 2 ^ k := by
  dsimp only
  let L := CyclotomicField (2 ^ (k + 2)) ℚ
  letI : NeZero (2 ^ (k + 2)) := ⟨pow_ne_zero _ (by norm_num)⟩
  letI : NeZero ((2 ^ (k + 2) : ℕ) : ℚ) := ⟨by positivity⟩
  letI : IsCyclotomicExtension {2 ^ (k + 2)} ℚ L := by
    dsimp [L]
    exact CyclotomicField.isCyclotomicExtension (2 ^ (k + 2)) ℚ
  letI : NumberField.IsCMField L :=
    IsCyclotomicExtension.Rat.isCMField L (S := {2 ^ (k + 2)})
      ⟨2 ^ (k + 2), by simp, by
        have hfour : 4 ≤ 2 ^ (k + 2) := by
          calc
            4 = 2 ^ 2 := by norm_num
            _ ≤ 2 ^ (k + 2) := Nat.pow_le_pow_right (by omega) (by omega)
        omega⟩
  let K := maximalRealSubfield L
  have htower := Module.finrank_mul_finrank ℚ K L
  rw [Algebra.IsQuadraticExtension.finrank_eq_two K L] at htower
  have hL : Module.finrank ℚ L = (2 ^ (k + 2)).totient :=
    IsCyclotomicExtension.Rat.finrank (2 ^ (k + 2)) L
  rw [hL, Nat.totient_prime_pow Nat.prime_two
    (by positivity : 0 < k + 2)] at htower
  norm_num at htower
  simp only [pow_succ] at htower
  change Module.finrank ℚ K = 2 ^ k
  omega

lemma exponent_lt_of_large_degree {ε : ℝ} (hε : 0 < ε) {d : ℕ}
    (hd : 1 < d) (hlarge : 4 / ε + 6 < 9 * (d : ℝ)) :
    (2 * d : ℝ) / (3 * d - 2 : ℕ) < (2 : ℝ) / 3 + ε := by
  have h3d : 2 ≤ 3 * d := by omega
  have hcast : ((3 * d - 2 : ℕ) : ℝ) = 3 * (d : ℝ) - 2 := by
    rw [Nat.cast_sub h3d]
    norm_num
  rw [hcast]
  have hden : 0 < 3 * (d : ℝ) - 2 := by
    exact_mod_cast (by omega : 0 < 3 * d - 2)
  rw [div_lt_iff₀ hden]
  have hfour : 4 < (9 * (d : ℝ) - 6) * ε := by
    apply (div_lt_iff₀ hε).mp
    linarith
  nlinarith

lemma exists_cyclotomic_degree_for_exponent (ε : ℝ) (hε : 0 < ε) :
    ∃ k : ℕ, 1 < 2 ^ k ∧
      (2 : ℝ) * ((2 ^ k : ℕ) : ℝ) / (3 * (2 ^ k) - 2 : ℕ) <
        (2 : ℝ) / 3 + ε := by
  obtain ⟨q, hq⟩ := exists_nat_gt ((4 / ε + 6) / 9)
  have hdpow : 1 < 2 ^ (q + 2) := by
    calc
      1 < 2 ^ 1 := by norm_num
      _ ≤ 2 ^ (q + 2) := Nat.pow_le_pow_right (by omega) (by omega)
  refine ⟨q + 2, hdpow, ?_⟩
  apply exponent_lt_of_large_degree hε (d := 2 ^ (q + 2)) hdpow
  have hqd : (q : ℝ) < (2 ^ (q + 2) : ℕ) := by
    exact_mod_cast (lt_trans (Nat.lt_pow_self (by omega : 1 < 2))
      (Nat.pow_lt_pow_right (by omega : 1 < 2) (by omega : q < q + 2)))
  have hq' : 4 / ε + 6 < 9 * (q : ℝ) := by linarith
  nlinarith

/-- The central result: for every loss `ε > 0`, all sufficiently large
cardinalities have `n` incident point-line pairs in the unit square whose
off-diagonal point-to-line distances are at least `n ^ (-(2/3 + ε))`. -/
theorem sharp_exponent_for_minimal_distance (ε : ℝ) (hε : 0 < ε) :
    ∃ n₀ : ℕ, ∀ n ≥ n₀, ∃ C : PLConfiguration n,
      C.Separated ((n : ℝ) ^ (-((2 : ℝ) / 3 + ε))) := by
  obtain ⟨k, hkdeg, hkexp⟩ := exists_cyclotomic_degree_for_exponent ε hε
  let L := CyclotomicField (2 ^ (k + 2)) ℚ
  let K := maximalRealSubfield L
  letI : NumberField K := NumberField.of_subfield K
  letI : NumberField.IsTotallyReal K :=
    NumberField.isTotallyReal_maximalRealSubfield
  have hdeg : Module.finrank ℚ K = 2 ^ k := by
    simpa [L, K] using realCyclotomicField_finrank k
  let φ : K →ₐ[ℚ] ℂ :=
    (Classical.choice (inferInstance : Nonempty (K →+* ℂ))).toRatAlgHom
  let σ : K →+* ℝ := realEmbedding φ
  let B : TraceBasisData K := traceBasisData (by rw [hdeg]; omega)
  apply eventually_configuration_of_fixed_field σ B ((2 : ℝ) / 3 + ε)
  · simpa [hdeg] using hkdeg
  · simpa [hdeg] using hkexp

end SharpDistance