The field generated by distances to two anchors

-- Extracted dependency interfaces and their necessary proofs.
import Mathlib
import Mathlib.Algebra.CharP.IntermediateField
import Mathlib.FieldTheory.Galois.Basic
import Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
import Mathlib.FieldTheory.Minpoly.Field

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


noncomputable section

open Polynomial

namespace Esgk

variable {F K : Type*} [Field F] [Field K] [Algebra F K] [CharZero F]


def twoAnchorDistanceField (x y : K) (r : F) : IntermediateField F K :=
  IntermediateField.adjoin F
    { (x + algebraMap F K r) ^ 2 + y ^ 2,
      (x - algebraMap F K r) ^ 2 + y ^ 2 }


theorem firstCoordinate_mem_twoAnchorDistanceField
    (x y : K) {r : F} (hr : r ≠ 0) :
    x ∈ twoAnchorDistanceField x y r := by
  let dLeft : K := (x + algebraMap F K r) ^ 2 + y ^ 2
  let dRight : K := (x - algebraMap F K r) ^ 2 + y ^ 2
  let L : IntermediateField F K := twoAnchorDistanceField x y r
  have hdLeft : dLeft ∈ L := by
    exact IntermediateField.subset_adjoin F {dLeft, dRight}
      (Set.mem_insert dLeft {dRight})
  have hdRight : dRight ∈ L := by
    exact IntermediateField.subset_adjoin F {dLeft, dRight}
      (Set.mem_insert_of_mem dLeft (Set.mem_singleton dRight))
  have hden : algebraMap F K (4 * r) ≠ 0 := by
    simpa using (mul_ne_zero (by norm_num : (4 : F) ≠ 0) hr)
  have hquot : (dLeft - dRight) / algebraMap F K (4 * r) ∈ L := by
    exact L.div_mem (L.sub_mem hdLeft hdRight) (L.algebraMap_mem (4 * r))
  have heq : (dLeft - dRight) / algebraMap F K (4 * r) = x := by
    rw [div_eq_iff hden]
    dsimp [dLeft, dRight]
    simp only [map_mul, map_ofNat]
    ring
  rwa [heq] at hquot


theorem secondCoordinate_sq_mem_twoAnchorDistanceField
    (x y : K) {r : F} (hr : r ≠ 0) :
    y ^ 2 ∈ twoAnchorDistanceField x y r := by
  let L : IntermediateField F K := twoAnchorDistanceField x y r
  have hx : x ∈ L := firstCoordinate_mem_twoAnchorDistanceField x y hr
  let dLeft : K := (x + algebraMap F K r) ^ 2 + y ^ 2
  have hdLeft : dLeft ∈ L := by
    exact IntermediateField.subset_adjoin F
      {dLeft, (x - algebraMap F K r) ^ 2 + y ^ 2} (Set.mem_insert _ _)
  have hbaseMem : x + algebraMap F K r ∈ L :=
    L.add_mem hx (L.algebraMap_mem r)
  have hbase : (x + algebraMap F K r) ^ 2 ∈ L := by
    simpa [pow_two] using L.mul_mem hbaseMem hbaseMem
  have hdiff : dLeft - (x + algebraMap F K r) ^ 2 ∈ L :=
    L.sub_mem hdLeft hbase
  have heq : dLeft - (x + algebraMap F K r) ^ 2 = y ^ 2 := by
    dsimp [dLeft]
    ring
  rwa [heq] at hdiff


theorem secondCoordinate_isIntegral_twoAnchorDistanceField
    (x y : K) {r : F} (hr : r ≠ 0) :
    IsIntegral (twoAnchorDistanceField x y r) y := by
  let L : IntermediateField F K := twoAnchorDistanceField x y r
  have hx : x ∈ L := firstCoordinate_mem_twoAnchorDistanceField x y hr
  let xL : L := ⟨x, hx⟩
  let dLeft : K := (x + algebraMap F K r) ^ 2 + y ^ 2
  have hdLeft : dLeft ∈ L := by
    exact IntermediateField.subset_adjoin F
      {dLeft, (x - algebraMap F K r) ^ 2 + y ^ 2} (Set.mem_insert _ _)
  let dLeftL : L := ⟨dLeft, hdLeft⟩
  let z : L := dLeftL - (xL + algebraMap F L r) ^ 2
  let p : L[X] := X ^ 2 - C z
  refine ⟨p, monic_X_pow_sub_C z (by norm_num), ?_⟩
  simp [p, z, dLeftL, xL, dLeft]


theorem finrank_adjoin_secondCoordinate_le_two
    (x y : K) {r : F} (hr : r ≠ 0) :
    Module.finrank (twoAnchorDistanceField x y r)
      (IntermediateField.adjoin (twoAnchorDistanceField x y r) {y}) ≤ 2 := by
  let L : IntermediateField F K := twoAnchorDistanceField x y r
  have hy : IsIntegral L y := secondCoordinate_isIntegral_twoAnchorDistanceField x y hr
  let xL : L := ⟨x, firstCoordinate_mem_twoAnchorDistanceField x y hr⟩
  let dLeft : K := (x + algebraMap F K r) ^ 2 + y ^ 2
  have hdLeft : dLeft ∈ L := by
    exact IntermediateField.subset_adjoin F
      {dLeft, (x - algebraMap F K r) ^ 2 + y ^ 2} (Set.mem_insert _ _)
  let dLeftL : L := ⟨dLeft, hdLeft⟩
  let z : L := dLeftL - (xL + algebraMap F L r) ^ 2
  let p : L[X] := X ^ 2 - C z
  rw [IntermediateField.adjoin.finrank hy]
  have hp : Polynomial.aeval y p = 0 := by
    simp [p, z, dLeftL, xL, dLeft]
  exact (natDegree_le_of_dvd (minpoly.dvd L y hp)
    (monic_X_pow_sub_C z (by norm_num)).ne_zero).trans_eq natDegree_X_pow_sub_C


theorem adjoin_secondCoordinate_eq_top_of_coordinates_generate
    (x y : K) {r : F} (hr : r ≠ 0)
    (hxy : IntermediateField.adjoin F {x, y} = ⊤) :
    IntermediateField.adjoin (twoAnchorDistanceField x y r) {y} = ⊤ := by
  let L : IntermediateField F K := twoAnchorDistanceField x y r
  apply IntermediateField.restrictScalars_injective F
  rw [IntermediateField.restrictScalars_top]
  apply top_unique
  rw [← hxy, IntermediateField.adjoin_le_iff]
  intro z hz
  rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hz
  rcases hz with (hz | hz)
  · subst z
    let xL : L := ⟨x, firstCoordinate_mem_twoAnchorDistanceField x y hr⟩
    change x ∈ IntermediateField.adjoin L {y}
    simpa [xL] using (IntermediateField.adjoin L {y}).algebraMap_mem xL
  · subst z
    change y ∈ IntermediateField.adjoin L {y}
    exact IntermediateField.subset_adjoin L {y} (Set.mem_singleton y)


theorem finiteDimensional_twoAnchorDistanceField
    (x y : K) {r : F} (hr : r ≠ 0)
    (hxy : IntermediateField.adjoin F {x, y} = ⊤) :
    FiniteDimensional (twoAnchorDistanceField x y r) K := by
  let L : IntermediateField F K := twoAnchorDistanceField x y r
  change FiniteDimensional L K
  have hy : IsIntegral L y := secondCoordinate_isIntegral_twoAnchorDistanceField x y hr
  have htop : IntermediateField.adjoin L {y} = ⊤ :=
    adjoin_secondCoordinate_eq_top_of_coordinates_generate x y hr hxy
  letI : FiniteDimensional L (⊤ : IntermediateField L K) := by
    rw [← htop]
    exact IntermediateField.adjoin.finiteDimensional hy
  exact IntermediateField.topEquiv.toLinearEquiv.finiteDimensional


theorem twoAnchorDistanceField_finrank_le_two
    (x y : K) {r : F} (hr : r ≠ 0)
    (hxy : IntermediateField.adjoin F {x, y} = ⊤) :
    Module.finrank (twoAnchorDistanceField x y r) K ≤ 2 := by
  let L : IntermediateField F K := twoAnchorDistanceField x y r
  change Module.finrank L K ≤ 2
  have htop : IntermediateField.adjoin L {y} = ⊤ :=
    adjoin_secondCoordinate_eq_top_of_coordinates_generate x y hr hxy
  rw [← IntermediateField.finrank_top', ← htop]
  exact finrank_adjoin_secondCoordinate_le_two x y hr

 
theorem twoAnchorDistanceField_finrank_eq_one_or_two
    (x y : K) {r : F} (hr : r ≠ 0)
    (hxy : IntermediateField.adjoin F {x, y} = ⊤) :
    Module.finrank (twoAnchorDistanceField x y r) K = 1 ∨
      Module.finrank (twoAnchorDistanceField x y r) K = 2 := by
  letI : FiniteDimensional (twoAnchorDistanceField x y r) K :=
    finiteDimensional_twoAnchorDistanceField x y hr hxy
  have hpos : 0 < Module.finrank (twoAnchorDistanceField x y r) K := Module.finrank_pos
  have hle := twoAnchorDistanceField_finrank_le_two x y hr hxy
  omega


theorem twoAnchorDistanceField_finrank_eq_two_of_secondCoordinate_not_mem
    (x y : K) {r : F} (hr : r ≠ 0)
    (hxy : IntermediateField.adjoin F {x, y} = ⊤)
    (hy : y ∉ twoAnchorDistanceField x y r) :
    Module.finrank (twoAnchorDistanceField x y r) K = 2 := by
  rcases twoAnchorDistanceField_finrank_eq_one_or_two x y hr hxy with
    hdegreeOne | hdegreeTwo
  · exfalso
    apply hy
    have htop : twoAnchorDistanceField x y r = ⊤ :=
      IntermediateField.finrank_eq_one_iff_eq_top.mp hdegreeOne
    rw [htop]
    trivial
  · exact hdegreeTwo


theorem exists_twoAnchorReflectionAlgEquiv
    (x y : K) {r : F} (hr : r ≠ 0)
    (hxy : IntermediateField.adjoin F {x, y} = ⊤)
    (hy : y ∉ twoAnchorDistanceField x y r) :
    ∃ σ : K ≃ₐ[twoAnchorDistanceField x y r] K,
      σ ≠ 1 ∧ σ x = x ∧ σ y = -y ∧ ∀ z, σ (σ z) = z := by
  let L : IntermediateField F K := twoAnchorDistanceField x y r
  change ∃ σ : K ≃ₐ[L] K, σ ≠ 1 ∧ σ x = x ∧ σ y = -y ∧ ∀ z, σ (σ z) = z
  letI : FiniteDimensional L K :=
    finiteDimensional_twoAnchorDistanceField x y hr hxy
  have hfinrank : Module.finrank L K = 2 :=
    twoAnchorDistanceField_finrank_eq_two_of_secondCoordinate_not_mem x y hr hxy hy
  letI : Algebra.IsIntegral L K := Algebra.IsIntegral.of_finite L K
  letI : Algebra.IsSeparable L K := Algebra.IsSeparable.of_integral L K
  letI : Algebra.IsQuadraticExtension L K := { finrank_eq_two' := hfinrank }
  letI : IsGalois L K := Algebra.IsQuadraticExtension.isGalois L K
  have hnontrivial : ∃ σ : K ≃ₐ[L] K, σ ≠ 1 := by
    have hcard : Nat.card (K ≃ₐ[L] K) = 2 := by
      rw [IsGalois.card_aut_eq_finrank, hfinrank]
    by_contra h
    push Not at h
    have hsubsingleton : Subsingleton (K ≃ₐ[L] K) :=
      ⟨fun σ τ => by rw [h σ, h τ]⟩
    have hone : Nat.card (K ≃ₐ[L] K) = 1 :=
      Nat.card_eq_one_iff_unique.mpr ⟨hsubsingleton, ⟨1⟩⟩
    omega
  obtain ⟨σ, hσ⟩ := hnontrivial
  have hx : x ∈ L := firstCoordinate_mem_twoAnchorDistanceField x y hr
  let xL : L := ⟨x, hx⟩
  have hσx : σ x = x := by
    simpa [xL] using σ.commutes xL
  have hysq : y ^ 2 ∈ L :=
    secondCoordinate_sq_mem_twoAnchorDistanceField x y hr
  let ySqL : L := ⟨y ^ 2, hysq⟩
  have hσsq : (σ y) ^ 2 = y ^ 2 := by
    have h := σ.commutes ySqL
    change σ (y ^ 2) = y ^ 2 at h
    simpa only [map_pow] using h
  have hyIntegral : IsIntegral L y :=
    secondCoordinate_isIntegral_twoAnchorDistanceField x y hr
  have htop : IntermediateField.adjoin L {y} = ⊤ :=
    adjoin_secondCoordinate_eq_top_of_coordinates_generate x y hr hxy
  have hAlgebraTop : Algebra.adjoin L {y} = ⊤ :=
    (IntermediateField.adjoin_eq_top_iff_of_isAlgebraic
      (by
        intro z hz
        rw [Set.mem_singleton_iff] at hz
        subst z
        exact hyIntegral.isAlgebraic)).mp htop
  have hproduct : (σ y - y) * (σ y + y) = 0 := by
    calc
      (σ y - y) * (σ y + y) = (σ y) ^ 2 - y ^ 2 := by ring
      _ = 0 := sub_eq_zero.mpr hσsq
  have hσy : σ y = -y := by
    rcases mul_eq_zero.mp hproduct with hfixed | hnegated
    · exfalso
      apply hσ
      have hfix : σ y = y := sub_eq_zero.mp hfixed
      have hext : (σ : K →ₐ[L] K) = AlgHom.id L K := by
        refine AlgHom.ext_of_adjoin_eq_top hAlgebraTop ?_
        intro z hz
        rw [Set.mem_singleton_iff] at hz
        subst z
        simpa using hfix
      ext z
      have hz := AlgHom.congr_fun hext z
      simpa using hz
    · exact eq_neg_of_add_eq_zero_left hnegated
  refine ⟨σ, hσ, hσx, hσy, ?_⟩
  intro z
  have hcomp :
      (σ : K →ₐ[L] K).comp (σ : K →ₐ[L] K) = AlgHom.id L K := by
    refine AlgHom.ext_of_adjoin_eq_top hAlgebraTop ?_
    intro w hw
    rw [Set.mem_singleton_iff] at hw
    subst w
    simp [hσy]
  have hz := AlgHom.congr_fun hcomp z
  simpa using hz

end Esgk