import Mathlib

/-!
# Problem 2: Algebraic certificate for `OM = ON`

This file formalises the polynomial core of the coordinate proof in Lean 4.
The theorem `polynomial_certificate` is completely proved by `ring`.
The theorem `algebraic_finish` proves the distance equality from the cleared
angle equations and the two circumcentre equations.

A fully synthetic encoding of Euclidean angles and the interior-point
hypotheses is intentionally separated from this algebraic certificate.
-/

set_option autoImplicit false

namespace Problem2

/-- Polynomial arising from the two angle conditions. -/
def F (a c s t : ℝ) : ℝ :=
  c * ((1 + 2 * a^2) * t^2 + a^2) +
  s * (a * (t^2 + 1) - (a^2 + 1) * t)

def Hq (a q ρ c s : ℝ) : ℝ :=
  ρ * (a + q)^2 - F a c s q

def Hp (a p ρ c s : ℝ) : ℝ :=
  ρ * F a c s p - (a + p)^2

def H0 (c s : ℝ) : ℝ :=
  c^2 + s^2 - 1

def Delta (p q c s : ℝ) : ℝ :=
  s * (1 - p*q) - c * (p + q)

def Den (a p q c s : ℝ) : ℝ :=
  (a + p) * (a + q) * Delta p q c s

def CenterRHS (a p q ρ c s : ℝ) : ℝ :=
  2*a *
    (ρ * (1 + p^2) * (a + q) * (ρ * (s - q*c) + q) -
     (1 + q^2) * (a + p) * (s + p * (ρ - c)))

def T (a p q ρ c s : ℝ) : ℝ :=
  CenterRHS a p q ρ c s -
  (ρ^2 - 1) * Den a p q c s

def Up (a p ρ c s : ℝ) : ℝ :=
  a + p + ρ * (-2*a*c*p^2 - a*c + a*p*s + c*p + p^2*s)

def Vq (a q ρ c s : ℝ) : ℝ :=
  ρ * (a + q) - 2*a*c*q^2 - a*c + a*q*s + c*q + q^2*s

def W (a p q : ℝ) : ℝ :=
  2*a^2*p*q - a^2 - a*p - a*q + p*q

/-- The exact polynomial certificate used in the written solution. -/
theorem polynomial_certificate
    (a p q ρ c s : ℝ) :
    T a p q ρ c s =
      Up a p ρ c s * Hq a q ρ c s +
      Vq a q ρ c s * Hp a p ρ c s -
      ρ * (p - q) * W a p q * H0 c s := by
  unfold T CenterRHS Den Delta Up Vq W Hq Hp H0 F
  ring

/--
Algebraic completion of the proof.

`hcenter` is the cleared-denominator form obtained by solving the two linear
circumcentre equations. `hHq` and `hHp` are the two cleared angle equations.
-/
theorem algebraic_finish
    (a p q ρ c s u v : ℝ)
    (hHq : Hq a q ρ c s = 0)
    (hHp : Hp a p ρ c s = 0)
    (hunit : c^2 + s^2 = 1)
    (hcenter :
      4 * ((ρ - c) * u - s*v) * Den a p q c s =
        CenterRHS a p q ρ c s)
    (hden : Den a p q c s ≠ 0) :
    (u - ρ/2)^2 + v^2 =
      (u - c/2)^2 + (v - s/2)^2 := by
  have hH0 : H0 c s = 0 := by
    unfold H0
    linarith
  have hT : T a p q ρ c s = 0 := by
    calc
      T a p q ρ c s =
          Up a p ρ c s * Hq a q ρ c s +
          Vq a q ρ c s * Hp a p ρ c s -
          ρ * (p - q) * W a p q * H0 c s :=
        polynomial_certificate a p q ρ c s
      _ = 0 := by rw [hHq, hHp, hH0]; ring
  have hmul :
      (4 * ((ρ - c) * u - s*v) - (ρ^2 - 1)) *
          Den a p q c s = 0 := by
    unfold T at hT
    nlinarith [hcenter, hT]
  have hlinear :
      4 * ((ρ - c) * u - s*v) = ρ^2 - 1 := by
    have hz :
        4 * ((ρ - c) * u - s*v) - (ρ^2 - 1) = 0 :=
      (mul_eq_zero.mp hmul).resolve_right hden
    linarith
  nlinarith [hlinear, hunit]

/-!
## Geometry bridge

For the coordinate choices in `problem2_solution_en.md`, the three geometric
angle hypotheses yield `Hq = 0`, `Hp = 0`, and the cleared circumcentre
equation `hcenter`.  Encoding directed Euclidean angles is independent of the
polynomial certificate above and can be added without changing
`polynomial_certificate` or `algebraic_finish`.
-/

end Problem2
