/-
Suggested additional results for the geometry of projection (Schlenker & Lamberton 2024, 7.2-7.3).
Builds on `IconologicalGeometry.lean` (imported).  Lean core only.

  A1  a viewpoint is determined by two projected classifiers
  A2  when two classifiers can share one viewpoint (intrinsic criterion)
  A3  dynamic projection: object speed = (s(pi)/t(pi)) x classifier speed
-/
import IconologicalGeometry

namespace IconologicalGeometry
open V3 M3

/-! ## A1. Identifiability of the viewpoint -/

theorem sq_nonneg' (a : Rat) : 0 ≤ a * a := by
  rcases (Rat.le_total : 0 ≤ a ∨ a ≤ 0) with h | h
  · exact Rat.mul_nonneg h h
  · have h' : 0 ≤ -a := by grind
    have := Rat.mul_nonneg h' h'; grind

theorem nsq_eq_zero {a : V3} (h : a.nsq = 0) : a = 0 := by
  simp [V3.nsq, V3.dot] at h
  have h1 := sq_nonneg' a.x
  have h2 := sq_nonneg' a.y
  have h3 := sq_nonneg' a.z
  have hx : a.x * a.x = 0 := by grind
  have hy : a.y * a.y = 0 := by grind
  have hz : a.z * a.z = 0 := by grind
  have hx : a.x = 0 := by rcases Rat.mul_eq_zero.1 hx with h | h <;> exact h
  have hy : a.y = 0 := by rcases Rat.mul_eq_zero.1 hy with h | h <;> exact h
  have hz : a.z = 0 := by rcases Rat.mul_eq_zero.1 hz with h | h <;> exact h
  ext <;> simp <;> assumption

theorem sq_pos_eq {a b : Rat} (ha : 0 < a) (hb : 0 < b) (h : a * a = b * b) : a = b := by
  have h0 : (a - b) * (a + b) = 0 := by grind
  rcases Rat.mul_eq_zero.1 h0 with h | h
  · grind
  · grind

/-- Two classifiers with distinct centers, the first with a valid pose, projected to the same
two objects under viewpoints π and π' (same r*): π and π' agree on r(π) and s(π). -/
theorem viewpoint_determined (lex₁ lex₂ : Prop) (π π' : Viewpoint) (rstar : Frame)
    (cl₁ cl₂ d₁ d₂ : Pose) (hv : cl₁.Valid) (hne : cl₁.c ≠ cl₂.c)
    (h₁ : projStatic lex₁ π rstar cl₁ d₁) (h₂ : projStatic lex₂ π rstar cl₂ d₂)
    (h₁' : projStatic lex₁ π' rstar cl₁ d₁) (h₂' : projStatic lex₂ π' rstar cl₂ d₂) :
    π.s = π'.s ∧ π.frame.o = π'.frame.o ∧ π.frame.R = π'.frame.R := by
  rw [projStatic_iff] at h₁ h₂ h₁' h₂'
  have e1 := shared_viewpoint_distance _ cl₁ cl₂ d₁ d₂ h₁.2 h₂.2
  have e2 := shared_viewpoint_distance _ cl₁ cl₂ d₁ d₂ h₁'.2 h₂'.2
  have hn : (cl₁.c - cl₂.c).nsq ≠ 0 := by
    intro h
    apply hne
    have := nsq_eq_zero h
    have hx := congrArg V3.x this
    have hy := congrArg V3.y this
    have hz := congrArg V3.z this
    simp at hx hy hz
    ext <;> grind
  have hnp : 0 < (cl₁.c - cl₂.c).nsq := by
    have : 0 ≤ (cl₁.c - cl₂.c).nsq := by
      simp [V3.nsq, V3.dot]
      have := sq_nonneg' (cl₁.c.x - cl₂.c.x)
      have := sq_nonneg' (cl₁.c.y - cl₂.c.y)
      have := sq_nonneg' (cl₁.c.z - cl₂.c.z)
      grind
    grind
  have hs2 : (π.toSim rstar).s * (π.toSim rstar).s = (π'.toSim rstar).s * (π'.toSim rstar).s := by
    have : ((π.toSim rstar).s * (π.toSim rstar).s) * (cl₁.c - cl₂.c).nsq
         = ((π'.toSim rstar).s * (π'.toSim rstar).s) * (cl₁.c - cl₂.c).nsq := by
      rw [← e1, ← e2]
    grind
  have hs : (π.toSim rstar).s = (π'.toSim rstar).s := sq_pos_eq (π.toSim rstar).hs (π'.toSim rstar).hs hs2
  have hg : π.toSim rstar = π'.toSim rstar := sim_unique cl₁ hv _ _ hs (h₁.2.trans h₁'.2.symm)
  have f := toSim_toViewpoint_frame π rstar
  have f' := toSim_toViewpoint_frame π' rstar
  refine ⟨hs, ?_, ?_⟩
  · rw [← f.1, ← f'.1]; simp only [Sim.toViewpoint]; rw [hg]
  · rw [← f.2, ← f'.2]; simp only [Sim.toViewpoint]; rw [hg]

/-! ## A2. When can two classifiers share a viewpoint? -/

/-- displacement from P to Q, read in P's own body axes -/
def bodyDisp (P Q : Pose) : V3 := P.O.T.mulV (Q.c - P.c)

theorem act_c_sub (g : Sim) (P Q : Pose) :
    (g.act Q).c - (g.act P).c = g.s • g.Q.mulV (Q.c - P.c) := by
  ext <;> simp [Sim.act, Sim.apply] <;> grind

theorem shared_viewpoint_iff (cl₁ cl₂ d₁ d₂ : Pose)
    (h₁ : cl₁.Valid) (k₁ : d₁.Valid) (s : Rat) (hs : 0 < s) :
    (∃ g : Sim, g.s = s ∧ g.act cl₁ = d₁ ∧ g.act cl₂ = d₂) ↔
      d₁.O.T.mul d₂.O = cl₁.O.T.mul cl₂.O ∧ bodyDisp d₁ d₂ = s • bodyDisp cl₁ cl₂ := by
  constructor
  · rintro ⟨g, rfl, e1, e2⟩
    refine ⟨shared_viewpoint_relative_orientation g cl₁ cl₂ d₁ d₂ e1 e2, ?_⟩
    have hc := act_c_sub g cl₁ cl₂
    rw [e1, e2] at hc
    have ho : d₁.O = g.Q.mul cl₁.O := by rw [← e1]; rfl
    unfold bodyDisp
    rw [hc, ho, M3.T_mul, M3.mulV_smul, ← M3.mul_mulV, M3.mul_assoc, g.hQ.1, M3.mul_one]
  · rintro ⟨ho, hd⟩
    let Q := d₁.O.mul cl₁.O.T
    have hQ : IsRot Q := k₁.mul h₁.T
    let g : Sim := ⟨s, hs, Q, hQ, d₁.c - s • Q.mulV cl₁.c⟩
    have g1 : g.act cl₁ = d₁ := by
      refine Pose.ext ?_ ?_
      · ext <;> simp [g, Sim.act, Sim.apply] <;> grind
      · show Q.mul cl₁.O = d₁.O
        show (d₁.O.mul cl₁.O.T).mul cl₁.O = d₁.O
        rw [M3.mul_assoc, h₁.1, M3.mul_one]
    refine ⟨g, rfl, g1, ?_⟩
    have hc := act_c_sub g cl₁ cl₂
    rw [g1] at hc
    refine Pose.ext ?_ ?_
    · -- centers
      have hΔ : d₂.c - d₁.c = s • Q.mulV (cl₂.c - cl₁.c) := by
        have : d₁.O.mulV (d₁.O.T.mulV (d₂.c - d₁.c)) = d₂.c - d₁.c := by
          rw [← M3.mul_mulV, k₁.2.1, M3.one_mulV]
        rw [← this]
        unfold bodyDisp at hd
        rw [hd, M3.mulV_smul]
        show _ = s • (d₁.O.mul cl₁.O.T).mulV _
        rw [M3.mul_mulV]
      have := hΔ
      have hx := congrArg V3.x hc
      have hy := congrArg V3.y hc
      have hz := congrArg V3.z hc
      have hx' := congrArg V3.x this
      have hy' := congrArg V3.y this
      have hz' := congrArg V3.z this
      simp at hx hy hz hx' hy' hz'
      ext <;> grind
    · show Q.mul cl₂.O = d₂.O
      show (d₁.O.mul cl₁.O.T).mul cl₂.O = d₂.O
      rw [M3.mul_assoc]
      have : cl₁.O.T.mul cl₂.O = d₁.O.T.mul d₂.O := ho.symm
      rw [this, ← M3.mul_assoc, k₁.2.1, M3.one_mul]

/-! ## A3. Dynamic projection scales speeds by s(π)/t(π) -/

theorem dyn_speed_ratio (lex : Rat → Prop) (π : Viewpoint) (rstar : Frame) (dur : Rat)
    (cl obj : Rat → Pose) (t : Rat) (h : projDyn lex π rstar dur cl obj t)
    (a b : Rat) (ha : 0 ≤ a) (ha' : a ≤ dur) (hb : 0 ≤ b) (hb' : b ≤ dur) (hab : a ≠ b) :
    ((obj (t + π.ts * a)).c - (obj (t + π.ts * b)).c).nsq
        / ((t + π.ts * a) - (t + π.ts * b)) ^ 2
      = (π.s / π.ts) ^ 2 * (((cl a).c - (cl b).c).nsq / (a - b) ^ 2) := by
  have hA := ((projStatic_iff _ π rstar _ _).1 (h.2 a ha ha')).2
  have hB := ((projStatic_iff _ π rstar _ _).1 (h.2 b hb hb')).2
  have e := shared_viewpoint_distance _ _ _ _ _ hA hB
  simp only [Viewpoint.toSim] at e
  rw [e]
  have hts : π.ts ≠ 0 := Rat.ne_of_gt π.hts
  have hab' : a - b ≠ 0 := fun h0 => hab (by grind)
  have : (t + π.ts * a) - (t + π.ts * b) = π.ts * (a - b) := by grind
  rw [this]
  generalize ((cl a).c - (cl b).c).nsq = N
  generalize a - b = x at *
  grind

end IconologicalGeometry