import Omega.Constants
import Mathlib.MeasureTheory.Integral.CircleIntegral
import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
import Mathlib.Data.Complex.FiniteDimensional

/-! The plane is ℂ with its Euclidean norm, regarded as a real vector space.
Coordinates are in the declared normal placement: center 0, seed at +1.
Arc length below is the integral of speed of this smooth parametrization. -/
namespace Omega
noncomputable section
open Set Complex Real

def mark (a z : ℝ) : ℂ := (a*c:ℝ) + (a*z:ℝ)*I
def heights : Fin 6 → ℝ := ![-(phi^2+s),-(1+s),-s,s,1+s,phi^2+s]
def marks (a : ℝ) (i : Fin 6) : ℂ := mark a (heights i)
def majorArc (a : ℝ) : Set ℂ := circleMap 0 a '' Icc delta (2*Real.pi-delta)
def oppositeSemicircle (a : ℝ) : Set ℂ := circleMap 0 a '' Icc (Real.pi/2) (3*Real.pi/2)
def extensionPlus (a : ℝ) : Set ℂ := mark a '' Icc s (phi^2+s)
def extensionMinus (a : ℝ) : Set ℂ := mark a '' Icc (-(phi^2+s)) (-s)
def outline (a : ℝ) : Set ℂ := majorArc a ∪ extensionPlus a ∪ extensionMinus a

def arcLength (a u v : ℝ) : ℝ := ∫ t in u..v, ‖deriv (circleMap 0 a) t‖

theorem arc_length (a u v : ℝ) (ha : 0 < a) : arcLength a u v=(v-u)*a := by
  simp [arcLength, norm_mul, norm_circleMap_zero, abs_of_pos ha,
    intervalIntegral.integral_const, smul_eq_mul]

theorem semicircle_retained (a : ℝ) : oppositeSemicircle a ⊆ majorArc a := by
  unfold oppositeSemicircle majorArc
  apply Set.image_mono
  intro t ht
  constructor <;> linarith [delta_lt_half_pi,ht.1,ht.2]

theorem semicircle_in_outline (a : ℝ) : oppositeSemicircle a ⊆ outline a := by
  intro z hz
  exact Or.inl (Or.inl (semicircle_retained a hz))

theorem major_arc_no_retracing (a : ℝ) (ha : 0 < a) :
    Set.InjOn (circleMap 0 a) (Icc delta (2*Real.pi-delta)) := by
  intro t ht u hu h
  apply eq_of_circleMap_eq (ne_of_gt ha) _ h
  rw [abs_lt]
  constructor <;> linarith [ht.1,ht.2,hu.1,hu.2,delta_pos]

theorem upper_seed_endpoint (a : ℝ) : circleMap 0 a delta=mark a s := by
  simp [circleMap,Complex.exp_mul_I,mark,s,c,mul_add,mul_assoc]

theorem lower_seed_endpoint (a : ℝ) : circleMap 0 a (2*Real.pi-delta)=mark a (-s) := by
  rw [show 2*Real.pi-delta=(-delta)+2*Real.pi by ring, periodic_circleMap 0 a]
  simp only [circleMap,zero_add,Complex.exp_mul_I]
  simp [mark,s,c,mul_add,mul_assoc]

theorem mark_re (a z : ℝ) : (mark a z).re=a*c := by simp [mark]
theorem mark_im (a z : ℝ) : (mark a z).im=a*z := by simp [mark]

theorem bilateral_reflection (a z : ℝ) : star (mark a z)=mark a (-z) := by
  apply Complex.ext <;> simp [mark]

theorem mark_distance (a z w : ℝ) (ha : 0 < a) :
    dist (mark a z) (mark a w)=a*|z-w| := by
  rw [dist_eq_norm]
  have he : mark a z-mark a w=((a*(z-w):ℝ):ℂ)*I := by
    simp only [mark,ofReal_mul,ofReal_sub]
    ring
  rw [he,norm_mul,Complex.norm_real,Complex.norm_I,mul_one,Real.norm_eq_abs,
    abs_mul,abs_of_pos ha]

theorem inner_extension_length (a : ℝ) (ha : 0 < a) :
    dist (mark a (1+s)) (mark a s)=a := by
  rw [mark_distance a _ _ ha]
  ring_nf
  simp

theorem outer_extension_length (a : ℝ) (ha : 0 < a) :
    dist (mark a (phi^2+s)) (mark a (1+s))=a*phi := by
  rw [mark_distance a _ _ ha]
  have h : phi^2+s-(1+s)=phi := by rw [phi_sq]; ring
  rw [h,abs_of_pos phi_pos]

theorem negative_outer_extension_length (a : ℝ) (ha : 0 < a) :
    dist (mark a (-(phi^2+s))) (mark a (-(1+s)))=a*phi := by
  rw [mark_distance a _ _ ha]
  have h : -(phi^2+s)- -(1+s)= -phi := by rw [phi_sq]; ring
  rw [h,abs_neg,abs_of_pos phi_pos]

theorem total_extension_length (a : ℝ) (ha : 0 < a) :
    dist (mark a (phi^2+s)) (mark a s)=a*phi^2 := by
  rw [mark_distance a _ _ ha]
  simp only [add_sub_cancel_right,abs_of_nonneg (sq_nonneg phi)]

theorem chord_length (a : ℝ) (ha : 0 < a) :
    dist (mark a s) (mark a (-s))=2*a*s := by
  rw [mark_distance a _ _ ha,sub_neg_eq_add,abs_of_pos (add_pos s_pos s_pos)]
  ring

theorem outer_segment_retained (a : ℝ) :
    mark a '' Icc (1+s) (phi^2+s) ⊆ outline a := by
  intro z hz
  rcases hz with ⟨t,ht,rfl⟩
  apply Or.inl ∘ Or.inr
  exact ⟨t,⟨by linarith [ht.1],ht.2⟩,rfl⟩

/-- The readout explicitly selects the outer straight segment and the opposite
semicircle. It is not a claim about uniqueness among all possible observables. -/
def G (a : ℝ) : ℝ := (dist (mark a (-(phi^2+s))) (mark a (-(1+s)))+
  dist (mark a (phi^2+s)) (mark a (1+s)))/2
def C (a : ℝ) : ℝ := arcLength a (Real.pi/2) (3*Real.pi/2)
def W (a : ℝ) : ℝ := G a+C a

theorem G_eq (a : ℝ) (ha : 0 < a) : G a=a*phi := by
  rw [G,negative_outer_extension_length a ha,outer_extension_length a ha]
  ring
theorem C_eq (a : ℝ) (ha : 0 < a) : C a=a*Real.pi := by
  unfold C
  rw [arc_length a _ _ ha]
  ring
theorem W_eq (a : ℝ) (ha : 0 < a) : W a=a*(phi+Real.pi) := by
  rw [W,G_eq a ha,C_eq a ha]
  ring

theorem geometric_provenance (a : ℝ) (ha : 0 < a) :
    G a/W a=lam ∧ C a/W a=mu := by
  rw [G_eq a ha,C_eq a ha,W_eq a ha]
  constructor <;> field_simp [lam,mu,ne_of_gt ha,ne_of_gt denominator_pos] <;> ring

def outlineLength (a : ℝ) : ℝ := arcLength a delta (2*Real.pi-delta)+
    dist (mark a (phi^2+s)) (mark a s)+
    dist (mark a (-(phi^2+s))) (mark a (-s))

theorem outline_length (a : ℝ) (ha : 0 < a) :
    outlineLength a=a*(2*Real.pi-epsilon)+2*a*phi^2 := by
  unfold outlineLength
  rw [arc_length a _ _ ha,total_extension_length a ha,mark_distance a _ _ ha]
  have he : -(phi^2+s)- -s= -(phi^2) := by ring
  rw [he,abs_neg,abs_of_nonneg (sq_nonneg phi)]
  unfold delta
  ring

theorem reference_not_outline (a : ℝ) (ha : 0 < a) : W a < outlineLength a := by
  rw [W_eq a ha,outline_length a ha,phi_sq]
  have he : epsilon < Real.pi := by unfold epsilon; linarith [pi_pos]
  nlinarith [phi_pos]

/-- The normal placement is unique once its scale and the six labeled
coordinate rules are specified. -/
theorem marked_coordinate_uniqueness (a : ℝ) (p : Fin 6 → ℂ)
    (hre : ∀ i, (p i).re=a*c) (him : ∀ i, (p i).im=a*heights i) : p=marks a := by
  funext i
  apply Complex.ext
  · exact (hre i).trans (mark_re a (heights i)).symm
  · exact (him i).trans (mark_im a (heights i)).symm

theorem heights_strictly_ordered : StrictMono heights := by
  intro i j hij
  fin_cases i <;> fin_cases j <;> norm_num [heights] at hij ⊢ <;>
    nlinarith [phi_pos,s_pos,phi_sq,phi_bounds.1,le_abs_self phi]

theorem sequential_extensions (a : ℝ) :
    mark a s+(a:ℂ)*I=mark a (1+s) ∧
    mark a (1+s)+(a*phi:ℝ)*I=mark a (phi^2+s) ∧
    mark a (-s)-(a:ℂ)*I=mark a (-(1+s)) ∧
    mark a (-(1+s))-(a*phi:ℝ)*I=mark a (-(phi^2+s)) := by
  simp only [mark,phi_sq,ofReal_mul,ofReal_add,ofReal_neg,ofReal_one]
  constructor
  · ring
  constructor
  · ring
  constructor <;> ring

end
end Omega