/-!
Iconological Semantics (Schlenker & Lamberton 2024), geometric part:
formalization of (84)-(85), (90), and a reconstructed "elegant" version
(fn. 45 and fn. 64), with equivalence theorems.

Self-contained, Lean core only (no Mathlib).  Reals are replaced by `Rat`
(all proofs are ring identities, so nothing depends on this choice).
Vectors are triples, 3x3 matrices are stored by columns (so that the
orientation triple <u,v,w> of the paper is literally the matrix [u v w]).

Sections
  1. linear algebra on Rat^3
  2. the ORIGINAL definitions (84), (85), (90)
  3. the ELEGANT version: similarity transformations
  4. equivalence theorems (static, dynamic, loci)
  5. properties easy in the elegant version
  6. worked examples (86)-(89), (91), (129), signer/addressee frames
  7. issues: counterexamples
-/

namespace IconologicalGeometry

/-! ## 1. Linear algebra -/

@[ext] structure V3 where
  x : Rat
  y : Rat
  z : Rat
  deriving DecidableEq, Repr

namespace V3
def zero : V3 := ⟨0, 0, 0⟩
def add (a b : V3) : V3 := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩
def sub (a b : V3) : V3 := ⟨a.x - b.x, a.y - b.y, a.z - b.z⟩
def neg (a : V3) : V3 := ⟨-a.x, -a.y, -a.z⟩
def smul (k : Rat) (a : V3) : V3 := ⟨k * a.x, k * a.y, k * a.z⟩
def dot (a b : V3) : Rat := a.x * b.x + a.y * b.y + a.z * b.z
def cross (a b : V3) : V3 :=
  ⟨a.y * b.z - a.z * b.y, a.z * b.x - a.x * b.z, a.x * b.y - a.y * b.x⟩
/-- squared Euclidean norm -/
def nsq (a : V3) : Rat := a.dot a
end V3

instance : Add V3 := ⟨V3.add⟩
instance : Sub V3 := ⟨V3.sub⟩
instance : Neg V3 := ⟨V3.neg⟩
instance : HSMul Rat V3 V3 := ⟨V3.smul⟩
instance : Zero V3 := ⟨V3.zero⟩

/-- 3x3 matrix stored by columns. -/
@[ext] structure M3 where
  c1 : V3
  c2 : V3
  c3 : V3
  deriving DecidableEq, Repr

namespace M3
def one : M3 := ⟨⟨1, 0, 0⟩, ⟨0, 1, 0⟩, ⟨0, 0, 1⟩⟩
def mulV (A : M3) (v : V3) : V3 := v.x • A.c1 + v.y • A.c2 + v.z • A.c3
def mul (A B : M3) : M3 := ⟨A.mulV B.c1, A.mulV B.c2, A.mulV B.c3⟩
def T (A : M3) : M3 :=
  ⟨⟨A.c1.x, A.c2.x, A.c3.x⟩, ⟨A.c1.y, A.c2.y, A.c3.y⟩, ⟨A.c1.z, A.c2.z, A.c3.z⟩⟩
def det (A : M3) : Rat := A.c1.dot (A.c2.cross A.c3)
def diag (a b c : Rat) : M3 := ⟨⟨a, 0, 0⟩, ⟨0, b, 0⟩, ⟨0, 0, c⟩⟩
end M3

/-- A rotation matrix: orthogonal (both ways) with determinant 1. -/
def IsRot (A : M3) : Prop := A.T.mul A = M3.one ∧ A.mul A.T = M3.one ∧ A.det = 1

instance (A : M3) : Decidable (IsRot A) := by unfold IsRot; infer_instance

/-- The paper's wording: a right-handed triple of orthogonal unit vectors. -/
def RightHandedOrthonormal (u v w : V3) : Prop :=
  u.dot u = 1 ∧ v.dot v = 1 ∧ w.dot w = 1 ∧
  u.dot v = 0 ∧ u.dot w = 0 ∧ v.dot w = 0 ∧ u.cross v = w

section lemmas
open V3 M3

@[simp] theorem V3.add_x (a b : V3) : (a + b).x = a.x + b.x := rfl
@[simp] theorem V3.add_y (a b : V3) : (a + b).y = a.y + b.y := rfl
@[simp] theorem V3.add_z (a b : V3) : (a + b).z = a.z + b.z := rfl
@[simp] theorem V3.sub_x (a b : V3) : (a - b).x = a.x - b.x := rfl
@[simp] theorem V3.sub_y (a b : V3) : (a - b).y = a.y - b.y := rfl
@[simp] theorem V3.sub_z (a b : V3) : (a - b).z = a.z - b.z := rfl
@[simp] theorem V3.smul_x (k : Rat) (a : V3) : (k • a).x = k * a.x := rfl
@[simp] theorem V3.smul_y (k : Rat) (a : V3) : (k • a).y = k * a.y := rfl
@[simp] theorem V3.smul_z (k : Rat) (a : V3) : (k • a).z = k * a.z := rfl
@[simp] theorem V3.zero_x : (0 : V3).x = 0 := rfl
@[simp] theorem V3.zero_y : (0 : V3).y = 0 := rfl
@[simp] theorem V3.zero_z : (0 : V3).z = 0 := rfl
@[simp] theorem V3.neg_x (a : V3) : (-a).x = -a.x := rfl
@[simp] theorem V3.neg_y (a : V3) : (-a).y = -a.y := rfl
@[simp] theorem V3.neg_z (a : V3) : (-a).z = -a.z := rfl

@[simp] theorem M3.mulV_x (A : M3) (v : V3) :
    (A.mulV v).x = v.x * A.c1.x + v.y * A.c2.x + v.z * A.c3.x := rfl
@[simp] theorem M3.mulV_y (A : M3) (v : V3) :
    (A.mulV v).y = v.x * A.c1.y + v.y * A.c2.y + v.z * A.c3.y := rfl
@[simp] theorem M3.mulV_z (A : M3) (v : V3) :
    (A.mulV v).z = v.x * A.c1.z + v.y * A.c2.z + v.z * A.c3.z := rfl

theorem M3.mulV_add (A : M3) (a b : V3) : A.mulV (a + b) = A.mulV a + A.mulV b := by
  ext <;> simp <;> grind
theorem M3.mulV_sub (A : M3) (a b : V3) : A.mulV (a - b) = A.mulV a - A.mulV b := by
  ext <;> simp <;> grind
theorem M3.mulV_smul (A : M3) (k : Rat) (a : V3) : A.mulV (k • a) = k • A.mulV a := by
  ext <;> simp <;> grind
theorem M3.mul_mulV (A B : M3) (v : V3) : (A.mul B).mulV v = A.mulV (B.mulV v) := by
  ext <;> simp [M3.mul] <;> grind
theorem M3.one_mulV (v : V3) : M3.one.mulV v = v := by
  ext <;> simp [M3.one] <;> grind
theorem M3.mul_assoc (A B C : M3) : (A.mul B).mul C = A.mul (B.mul C) := by
  ext <;> simp [M3.mul] <;> grind
theorem M3.T_mul (A B : M3) : (A.mul B).T = B.T.mul A.T := by
  ext <;> simp [M3.mul, M3.T] <;> grind
theorem M3.one_mul (A : M3) : M3.one.mul A = A := by
  ext <;> simp [M3.mul, M3.one] <;> grind
theorem M3.mul_one (A : M3) : A.mul M3.one = A := by
  ext <;> simp [M3.mul, M3.one] <;> grind
theorem M3.T_T (A : M3) : A.T.T = A := rfl
theorem M3.T_one : M3.one.T = M3.one := rfl
theorem M3.det_mul (A B : M3) : (A.mul B).det = A.det * B.det := by
  simp [M3.det, M3.mul, V3.dot, V3.cross]; grind

theorem IsRot.mul {A B : M3} (hA : IsRot A) (hB : IsRot B) : IsRot (A.mul B) := by
  obtain ⟨a1, a2, a3⟩ := hA
  obtain ⟨b1, b2, b3⟩ := hB
  refine ⟨?_, ?_, ?_⟩
  · rw [M3.T_mul, M3.mul_assoc, ← M3.mul_assoc A.T, a1, M3.one_mul, b1]
  · rw [M3.T_mul, M3.mul_assoc, ← M3.mul_assoc B, b2, M3.one_mul, a2]
  · rw [M3.det_mul, a3, b3]; grind
theorem IsRot.T {A : M3} (hA : IsRot A) : IsRot A.T :=
  ⟨by rw [M3.T_T]; exact hA.2.1, by rw [M3.T_T]; exact hA.1, by
    have := hA.2.2; simp [M3.det, V3.dot, V3.cross, M3.T] at *; grind⟩
theorem IsRot.one : IsRot M3.one := by
  decide +kernel

/-- Rotations preserve the dot product (hence squared norms). -/
theorem IsRot.dot_pres {A : M3} (hA : IsRot A) (a b : V3) :
    (A.mulV a).dot (A.mulV b) = a.dot b := by
  have h := hA.1
  simp [M3.ext_iff, V3.ext_iff, M3.mul, M3.T, M3.one] at h
  simp [V3.dot]; grind

/-- The paper's "right-handed triple of orthogonal unit vectors" is exactly a rotation matrix. -/
theorem rightHanded_isRot {u v w : V3} (h : RightHandedOrthonormal u v w) :
    IsRot ⟨u, v, w⟩ := by
  obtain ⟨h1, h2, h3, h4, h5, h6, h7⟩ := h
  simp [V3.dot, V3.ext_iff, V3.cross] at h1 h2 h3 h4 h5 h6 h7
  obtain ⟨h7x, h7y, h7z⟩ := h7
  refine ⟨?_, ?_, ?_⟩
  · simp [M3.ext_iff, V3.ext_iff, M3.mul, M3.T, M3.one]; grind
  · simp [M3.ext_iff, V3.ext_iff, M3.mul, M3.T, M3.one]; grind
  · simp [M3.det, V3.dot, V3.cross]; grind

end lemmas

/-! ## 2. The ORIGINAL formalization: (84), (85), (90) -/

/-- A Cartesian right-handed frame of reference, `r = (origin, axes)`; the axes are the
columns of `R`, expressed in some fixed ambient (absolute) coordinates. -/
structure Frame where
  o : V3
  R : M3
  hR : IsRot R

/-- Real-world object or classifier: absolute center and orientation triple `<u,v,w>` (= columns
of `O`).  Deliberately RAW (no orthonormality proof); `Pose.Valid` states what (84a) requires. -/
@[ext] structure Pose where
  c : V3
  O : M3
  deriving DecidableEq, Repr

def Pose.Valid (P : Pose) : Prop := IsRot P.O

instance (u v w : V3) : Decidable (RightHandedOrthonormal u v w) := by
  unfold RightHandedOrthonormal; infer_instance

/-- coordinates of an absolute point relative to a frame -/
def Frame.coord (F : Frame) (p : V3) : V3 := F.R.T.mulV (p - F.o)
/-- absolute point with the given coordinates in the frame -/
def Frame.point (F : Frame) (q : V3) : V3 := F.R.mulV q + F.o

/-- (84a)(i): `center(d, r)`. -/
def center (P : Pose) (F : Frame) : V3 := F.coord P.c
/-- (84a)(ii): `orientation(d, r)`: the triple of coordinates of u, v, w relative to `r`
(as a matrix with these columns). -/
def orientation (P : Pose) (F : Frame) : M3 := F.R.T.mul P.O

/-- (84b): a viewpoint provides a frame, a spatial scaling factor `s(π) > 0`, and a temporal
scaling factor `t(π) > 0` (field `ts`, renamed to avoid the paper's clash with time `t`). -/
structure Viewpoint where
  frame : Frame
  s : Rat
  hs : 0 < s
  ts : Rat
  hts : 0 < ts

/-- (85), for a fixed time and world: `lex` stands for the lexical condition
`word'_{t,w}(d) = 1`; `cl` is the classifier's pose (in signing space), `rstar` is the signer's
frame r*, `d` the object's pose (in the world), `π.frame` is r(π).
(85)(ii)a, b are the 2nd and 3rd conjuncts. -/
def projStatic (lex : Prop) (π : Viewpoint) (rstar : Frame) (cl d : Pose) : Prop :=
  lex ∧ center d π.frame = π.s • center cl rstar ∧ orientation d π.frame = orientation cl rstar

/-- (90), literally: `lex t'` is `word'_{t',w}(d)=1`; `cl d'` the static classifier at
classifier-time `d'`; `obj τ` the object's pose at real time τ; `dur` the duration `d`.
(i) lex at t; (ii) for each d' in [0,dur], proj(d, π, t + t(π)·d', w) = word-cl(d'). -/
def projDyn (lex : Rat → Prop) (π : Viewpoint) (rstar : Frame) (dur : Rat)
    (cl obj : Rat → Pose) (t : Rat) : Prop :=
  lex t ∧ ∀ d', 0 ≤ d' → d' ≤ dur →
    projStatic (lex (t + π.ts * d')) π rstar (cl d') (obj (t + π.ts * d'))

/-! ## 3. The ELEGANT version (reconstruction of fn. 45 / fn. 64) -/

/-- A similarity of space: uniform scaling `s > 0`, rotation `Q`, translation `t`. -/
@[ext] structure Sim where
  s : Rat
  hs : 0 < s
  Q : M3
  hQ : IsRot Q
  t : V3

def Sim.apply (g : Sim) (p : V3) : V3 := g.s • g.Q.mulV p + g.t
/-- action on poses: points are moved, orientation triples are only rotated (no scaling) -/
def Sim.act (g : Sim) (P : Pose) : Pose := ⟨g.apply P.c, g.Q.mul P.O⟩

def Sim.id : Sim := ⟨1, by decide, M3.one, IsRot.one, 0⟩
/-- `g₂.comp g₁` = first g₁ then g₂ -/
def Sim.comp (g₂ g₁ : Sim) : Sim :=
  ⟨g₂.s * g₁.s, Rat.mul_pos g₂.hs g₁.hs, g₂.Q.mul g₁.Q, g₂.hQ.mul g₁.hQ,
   g₂.s • g₂.Q.mulV g₁.t + g₂.t⟩

/-- The elegant projection: the classifier's pose is carried onto the object's pose by the
similarity `g` (which is what a viewpoint contributes). -/
def projSim (lex : Prop) (g : Sim) (cl d : Pose) : Prop := lex ∧ g.act cl = d

/-- The similarity determined by a viewpoint `π` and the signer's frame `r*`: it sends
`r*`-coordinates to `r(π)`-coordinates-scaled, i.e. the composite
  absolute-in-signing-space --(coord in r*)--> scale by s(π) --(point in r(π))--> world. -/
def Viewpoint.toSim (π : Viewpoint) (rstar : Frame) : Sim :=
  ⟨π.s, π.hs, π.frame.R.mul rstar.R.T, π.frame.hR.mul rstar.hR.T,
   π.frame.o - π.s • (π.frame.R.mul rstar.R.T).mulV rstar.o⟩

/-- Conversely, a similarity is a viewpoint (given r* and a temporal scale). -/
def Sim.toViewpoint (g : Sim) (rstar : Frame) (ts : Rat) (hts : 0 < ts) : Viewpoint :=
  ⟨⟨g.t + g.s • g.Q.mulV rstar.o, g.Q.mul rstar.R, g.hQ.mul rstar.hR⟩, g.s, g.hs, ts, hts⟩

/-- Dynamic elegant projection: a single similarity for space, and the affine time map
`d' ↦ t + t(π)·d'`. -/
def projDynSim (lex : Rat → Prop) (g : Sim) (ts : Rat) (dur : Rat)
    (cl obj : Rat → Pose) (t : Rat) : Prop :=
  ∀ d', 0 ≤ d' → d' ≤ dur → lex (t + ts * d') ∧ g.act (cl d') = obj (t + ts * d')

/-! ## 4. Equivalence theorems -/

section equiv
open V3 M3

theorem Frame.point_coord (F : Frame) (p : V3) : F.point (F.coord p) = p := by
  have h := F.hR.2.1
  simp [M3.ext_iff, V3.ext_iff, M3.mul, M3.T, M3.one] at h
  ext <;> simp [Frame.point, Frame.coord, M3.T] <;> grind

theorem Frame.coord_point (F : Frame) (q : V3) : F.coord (F.point q) = q := by
  have h := F.hR.1
  simp [M3.ext_iff, V3.ext_iff, M3.mul, M3.T, M3.one] at h
  ext <;> simp [Frame.point, Frame.coord, M3.T] <;> grind

theorem toSim_apply (π : Viewpoint) (r : Frame) (p : V3) :
    (π.toSim r).apply p = π.frame.point (π.s • r.coord p) := by
  ext <;> simp [Viewpoint.toSim, Sim.apply, Frame.point, Frame.coord, M3.mul, M3.T] <;> grind

theorem toSim_orient (π : Viewpoint) (r : Frame) (O : M3) :
    (π.toSim r).Q.mul O = π.frame.R.mul (r.R.T.mul O) := M3.mul_assoc _ _ _

theorem frame_cancel (F : Frame) (O : M3) : F.R.mul (F.R.T.mul O) = O := by
  rw [← M3.mul_assoc, F.hR.2.1, M3.one_mul]
theorem frame_cancel' (F : Frame) (O : M3) : F.R.T.mul (F.R.mul O) = O := by
  rw [← M3.mul_assoc, F.hR.1, M3.one_mul]

/-- **Static equivalence** (main theorem).  The original (85) holds for viewpoint π iff the
elegant version holds for the similarity `π.toSim r*`.  No validity of the poses is needed. -/
theorem projStatic_iff (lex : Prop) (π : Viewpoint) (rstar : Frame) (cl d : Pose) :
    projStatic lex π rstar cl d ↔ projSim lex (π.toSim rstar) cl d := by
  unfold projStatic projSim center orientation
  constructor
  · rintro ⟨hl, hc, ho⟩
    refine ⟨hl, ?_⟩
    have hc' : d.c = π.frame.point (π.s • rstar.coord cl.c) := by
      rw [← hc, Frame.point_coord]
    have ho' : d.O = π.frame.R.mul (rstar.R.T.mul cl.O) := by
      rw [← ho, frame_cancel]
    refine Pose.ext ?_ ?_
    · show (π.toSim rstar).apply cl.c = d.c
      rw [toSim_apply]; exact hc'.symm
    · show (π.toSim rstar).Q.mul cl.O = d.O
      rw [toSim_orient]; exact ho'.symm
  · rintro ⟨hl, h⟩
    refine ⟨hl, ?_, ?_⟩
    · have := congrArg Pose.c h
      simp only [Sim.act, toSim_apply] at this
      rw [← this, Frame.coord_point]
    · have := congrArg Pose.O h
      simp only [Sim.act, toSim_orient] at this
      rw [← this, frame_cancel']

/-- Every similarity arises from a viewpoint: viewpoints (frame + scale) ≅ similarities. -/
theorem toViewpoint_toSim (g : Sim) (rstar : Frame) (ts : Rat) (hts : 0 < ts) :
    (g.toViewpoint rstar ts hts).toSim rstar = g := by
  have h := rstar.hR.2.1
  have hs : (g.Q.mul rstar.R).mul rstar.R.T = g.Q := by
    rw [M3.mul_assoc, h, M3.mul_one]
  obtain ⟨s, hs0, Q, hQ, t⟩ := g
  simp only [Viewpoint.toSim, Sim.toViewpoint] at *
  simp only [hs]
  congr 1
  ext <;> simp <;> grind

theorem toSim_toViewpoint_frame (π : Viewpoint) (rstar : Frame) :
    ((π.toSim rstar).toViewpoint rstar π.ts π.hts).frame.o = π.frame.o ∧
    ((π.toSim rstar).toViewpoint rstar π.ts π.hts).frame.R = π.frame.R := by
  have h := rstar.hR.1
  have h2 := rstar.hR.2.1
  constructor
  · simp only [Viewpoint.toSim, Sim.toViewpoint]
    ext <;> simp <;> grind
  · simp only [Viewpoint.toSim, Sim.toViewpoint]
    rw [M3.mul_assoc, h, M3.mul_one]

/-- **Dynamic equivalence**: (90) iff the elegant dynamic version, plus the lexical condition
at t. -/
theorem projDyn_iff (lex : Rat → Prop) (π : Viewpoint) (rstar : Frame) (dur : Rat)
    (cl obj : Rat → Pose) (t : Rat) :
    projDyn lex π rstar dur cl obj t ↔
      lex t ∧ projDynSim lex (π.toSim rstar) π.ts dur cl obj t := by
  unfold projDyn projDynSim
  constructor
  · rintro ⟨h0, h⟩
    refine ⟨h0, fun d' a b => ?_⟩
    have := (projStatic_iff _ π rstar _ _).1 (h d' a b)
    exact this
  · rintro ⟨h0, h⟩
    refine ⟨h0, fun d' a b => ?_⟩
    exact (projStatic_iff _ π rstar _ _).2 (h d' a b)

/-- In (90), condition (i) is subsumed by (ii) as soon as the duration is nonnegative
(take d' = 0): the lexical condition at t is redundant in (90) as well. -/
theorem projDyn_i_redundant (lex : Rat → Prop) (π : Viewpoint) (rstar : Frame) (dur : Rat)
    (hd : 0 ≤ dur) (cl obj : Rat → Pose) (t : Rat) :
    projDyn lex π rstar dur cl obj t ↔
      ∀ d', 0 ≤ d' → d' ≤ dur →
        projStatic (lex (t + π.ts * d')) π rstar (cl d') (obj (t + π.ts * d')) := by
  unfold projDyn
  constructor
  · exact fun h => h.2
  · intro h
    refine ⟨?_, h⟩
    have := (h 0 (Rat.le_refl) hd).1
    rwa [Rat.mul_zero, Rat.add_zero] at this

/-- Redundancy claim of p. 35 and fn. 49 (two-valued reading): the lexical conjunct of (53)
is implied by the projective condition (85), because (85)(i) already contains it. -/
theorem lexical_condition_redundant (lex : Prop) (π : Viewpoint) (rstar : Frame)
    (cl d : Pose) :
    (lex ∧ projStatic lex π rstar cl d) ↔ projStatic lex π rstar cl d :=
  ⟨fun h => h.2, fun h => ⟨h.1, h⟩⟩

/-! ### Iconic loci, Appendix I-E: (127)-(128) -/

/-- (127) with (128)(ii)b: the orientation condition is trivialized. -/
def projLocus (lex : Prop) (π : Viewpoint) (rstar : Frame) (cl d : Pose) : Prop :=
  lex ∧ center d π.frame = π.s • center cl rstar

/-- "Trivialized" (128)(ii)b is the same as "the locus has *some* orientation for which the
full (127) holds" (ambiguity: 'one can pick any orientation one wishes'), provided the
object's orientation is a genuine rotation. -/
theorem projLocus_iff_exists_orientation (lex : Prop) (π : Viewpoint) (rstar : Frame)
    (cl d : Pose) (hd : d.Valid) :
    projLocus lex π rstar cl d ↔
      ∃ O', IsRot O' ∧ projStatic lex π rstar ⟨cl.c, O'⟩ d := by
  constructor
  · rintro ⟨hl, hc⟩
    refine ⟨rstar.R.mul (π.frame.R.T.mul d.O), rstar.hR.mul (π.frame.hR.T.mul hd), hl, hc, ?_⟩
    simp only [orientation]
    rw [frame_cancel']
  · rintro ⟨O', _, hl, hc, _⟩
    exact ⟨hl, hc⟩

end equiv


/-! ## 5. Properties that the elegant version makes easy -/

section props
open V3 M3

/-- Composition of transformations is composition of actions. -/
theorem Sim.act_comp (g₂ g₁ : Sim) (P : Pose) :
    (g₂.comp g₁).act P = g₂.act (g₁.act P) := by
  refine Pose.ext ?_ ?_
  · ext <;> simp [Sim.comp, Sim.act, Sim.apply, M3.mul] <;> grind
  · exact M3.mul_assoc _ _ _

theorem Sim.act_id (P : Pose) : Sim.id.act P = P := by
  refine Pose.ext ?_ ?_
  · ext <;> simp [Sim.id, Sim.act, Sim.apply, M3.one] <;> grind
  · exact M3.one_mul _

/-- Inverse similarity. -/
def Sim.inv (g : Sim) : Sim :=
  ⟨g.s⁻¹, Rat.inv_pos.2 g.hs, g.Q.T, g.hQ.T, -(g.s⁻¹ • g.Q.T.mulV g.t)⟩

theorem Sim.inv_act (g : Sim) (P : Pose) : g.inv.act (g.act P) = P := by
  have h := g.hQ.1
  have hs : g.s ≠ 0 := Rat.ne_of_gt g.hs
  simp [M3.ext_iff, V3.ext_iff, M3.mul, M3.T, M3.one] at h
  refine Pose.ext ?_ ?_
  · ext <;> simp [Sim.inv, Sim.act, Sim.apply, M3.T] <;> grind
  · show g.Q.T.mul (g.Q.mul P.O) = P.O
    rw [← M3.mul_assoc, g.hQ.1, M3.one_mul]

theorem Sim.act_inv (g : Sim) (P : Pose) : g.act (g.inv.act P) = P := by
  have h := g.hQ.2.1
  have hs : g.s ≠ 0 := Rat.ne_of_gt g.hs
  simp [M3.ext_iff, V3.ext_iff, M3.mul, M3.T, M3.one] at h
  refine Pose.ext ?_ ?_
  · ext <;> simp [Sim.inv, Sim.act, Sim.apply, M3.T] <;> grind
  · show g.Q.mul (g.Q.T.mul P.O) = P.O
    rw [← M3.mul_assoc, g.hQ.2.1, M3.one_mul]

/-- Projection is symmetric: the object is the image of the classifier iff the classifier is
the image of the object under the inverse transformation. -/
theorem projSim_symm (lex : Prop) (g : Sim) (cl d : Pose) :
    projSim lex g cl d ↔ lex ∧ g.inv.act d = cl := by
  unfold projSim
  constructor
  · rintro ⟨h, rfl⟩; exact ⟨h, Sim.inv_act _ _⟩
  · rintro ⟨h, hd⟩; refine ⟨h, ?_⟩; rw [← hd]; exact Sim.act_inv _ _

/-- fn. 64 read with an unconstrained existential is VACUOUS: for any two valid poses and any
scale there is a similarity with that scale mapping one to the other.  The transformation
has to be tied to the viewpoint (shared by all classifiers of a scene), as in `projSim`. -/
theorem exists_sim_of_valid (cl d : Pose) (hcl : cl.Valid) (hd : d.Valid)
    (s : Rat) (hs : 0 < s) : ∃ g : Sim, g.s = s ∧ g.act cl = d := by
  have hQ : IsRot (d.O.mul cl.O.T) := hd.mul hcl.T
  refine ⟨⟨s, hs, d.O.mul cl.O.T, hQ, d.c - s • (d.O.mul cl.O.T).mulV cl.c⟩, rfl, ?_⟩
  refine Pose.ext ?_ ?_
  · ext <;> simp [Sim.act, Sim.apply] <;> grind
  · show (d.O.mul cl.O.T).mul cl.O = d.O
    rw [M3.mul_assoc, hcl.1, M3.mul_one]

/-- Given the scale, the transformation is unique (for a valid classifier pose). -/
theorem sim_unique (cl : Pose) (hcl : cl.Valid) (g g' : Sim) (hs : g.s = g'.s)
    (h : g.act cl = g'.act cl) : g = g' := by
  have hO := congrArg Pose.O h
  have hc := congrArg Pose.c h
  simp only [Sim.act] at hO hc
  have hQ : g.Q = g'.Q := by
    have := congrArg (fun M => M.mul cl.O.T) hO
    simp only [M3.mul_assoc, hcl.2.1, M3.mul_one] at this
    exact this
  obtain ⟨s, hs0, Q, hQ0, t⟩ := g
  obtain ⟨s', hs0', Q', hQ0', t'⟩ := g'
  simp only at hs hQ
  subst hs; subst hQ
  simp only [Sim.apply] at hc
  have : t = t' := by
    have hx := congrArg V3.x hc
    have hy := congrArg V3.y hc
    have hz := congrArg V3.z hc
    simp at hx hy hz
    ext <;> grind
  subst this; rfl

/-- If two classifiers are projected by the SAME viewpoint, distances are scaled by s(π):
the same-π requirement is a real geometric constraint. -/
theorem shared_viewpoint_distance (g : Sim) (cl₁ cl₂ d₁ d₂ : Pose)
    (h₁ : g.act cl₁ = d₁) (h₂ : g.act cl₂ = d₂) :
    (d₁.c - d₂.c).nsq = g.s * g.s * (cl₁.c - cl₂.c).nsq := by
  subst h₁ h₂
  have : (g.act cl₁).c - (g.act cl₂).c = g.s • g.Q.mulV (cl₁.c - cl₂.c) := by
    ext <;> simp [Sim.act, Sim.apply] <;> grind
  rw [this]
  simp only [V3.nsq]
  have h := g.hQ.dot_pres (cl₁.c - cl₂.c) (cl₁.c - cl₂.c)
  simp [V3.dot] at h ⊢
  grind

/-- ... and the relative orientation of two depicted objects is preserved exactly. -/
theorem shared_viewpoint_relative_orientation (g : Sim) (cl₁ cl₂ d₁ d₂ : Pose)
    (h₁ : g.act cl₁ = d₁) (h₂ : g.act cl₂ = d₂) :
    d₁.O.T.mul d₂.O = cl₁.O.T.mul cl₂.O := by
  subst h₁ h₂
  simp only [Sim.act, M3.T_mul]
  rw [M3.mul_assoc, ← M3.mul_assoc g.Q.T, g.hQ.1, M3.one_mul]

/-! ### Change of frame: signer vs addressee -/

/-- Rotate a frame's axes (keeping its origin): `R ↦ R·P`. -/
def Frame.rot (F : Frame) (P : M3) (hP : IsRot P) : Frame := ⟨F.o, F.R.mul P, F.hR.mul hP⟩

def Viewpoint.rot (π : Viewpoint) (P : M3) (hP : IsRot P) : Viewpoint :=
  { π with frame := π.frame.rot P hP }

theorem toSim_rot (π : Viewpoint) (r : Frame) (P : M3) (hP : IsRot P) :
    (π.rot P hP).toSim (r.rot P hP) = π.toSim r := by
  have hQ : (π.frame.R.mul P).mul (r.R.mul P).T = π.frame.R.mul r.R.T := by
    rw [M3.T_mul, M3.mul_assoc, ← M3.mul_assoc P, hP.2.1, M3.one_mul]
  apply Sim.ext
  · rfl
  · exact hQ
  · simp only [Viewpoint.toSim, Viewpoint.rot, Frame.rot, hQ]

/-- Changing the coordinate axes of BOTH the signer's frame r* and the viewpoint frame r(π) by
the same rotation `P` does not change what projects to what. -/
theorem projStatic_rot (lex : Prop) (π : Viewpoint) (r : Frame) (P : M3) (hP : IsRot P)
    (cl d : Pose) :
    projStatic lex (π.rot P hP) (r.rot P hP) cl d ↔ projStatic lex π r cl d := by
  rw [projStatic_iff, projStatic_iff, toSim_rot]

/-- Same for dynamic projection. -/
theorem projDyn_rot (lex : Rat → Prop) (π : Viewpoint) (r : Frame) (P : M3) (hP : IsRot P)
    (dur : Rat) (cl obj : Rat → Pose) (t : Rat) :
    projDyn lex (π.rot P hP) (r.rot P hP) dur cl obj t ↔ projDyn lex π r dur cl obj t := by
  rw [projDyn_iff, projDyn_iff, toSim_rot]; rfl

/-- The signer's frame r*: origin at the center of signing space, x right, y front, z up
(chest at (0,-1,0)). -/
def signerFrame : Frame := ⟨0, M3.one, IsRot.one⟩

/-- 180 degrees about z. -/
def rotZ180 : M3 := M3.diag (-1) (-1) 1
theorem rotZ180_isRot : IsRot rotZ180 := by decide +kernel

/-- Directions of the addressee (standing at (0,1,0), facing the signer, i.e. facing -y), in
r*-coordinates.  right/front/up are the addressee's own; left and back are their negatives. -/
def addrRight : V3 := ⟨-1, 0, 0⟩
def addrFront : V3 := ⟨0, -1, 0⟩
def addrUp : V3 := ⟨0, 0, 1⟩

/-- The paper's addressee coordinate system (x toward the addressee's LEFT, y toward their
BACK, z up) is the very same coordinate system as the signer's r*: identical axes. -/
theorem addressee_paper_frame_eq_signer :
    (⟨-addrRight, -addrFront, addrUp⟩ : M3) = signerFrame.R := by decide +kernel

/-- The addressee's own natural (right, front, up) frame is r* rotated by 180 degrees about z. -/
theorem addressee_natural_frame :
    (⟨addrRight, addrFront, addrUp⟩ : M3) = signerFrame.R.mul rotZ180 := by decide +kernel

/-- Hence: doing the whole construction with addressee-natural axes for both frames (r* and
r(π)) is equivalent to the signer version (the paper's remark, p. 31-32 and fn. 47). -/
theorem signer_addressee_equivalence (lex : Prop) (π : Viewpoint) (cl d : Pose) :
    projStatic lex (π.rot rotZ180 rotZ180_isRot) (signerFrame.rot rotZ180 rotZ180_isRot) cl d
      ↔ projStatic lex π signerFrame cl d :=
  projStatic_rot _ _ _ _ _ _ _

end props

/-! ## 6. Worked examples -/

section examples
open V3 M3

instance : DecidablePred Pose.Valid := fun P => inferInstanceAs (Decidable (IsRot P.O))

def idFrame : Frame := ⟨0, M3.one, IsRot.one⟩

/-- (88): orientation triples. -/
def oOb : M3 := ⟨⟨0, 1, 0⟩, ⟨-1, 0, 0⟩, ⟨0, 0, 1⟩⟩
def oDL : M3 := ⟨⟨0, -1, 0⟩, ⟨1, 0, 0⟩, ⟨0, 0, 1⟩⟩

/-- (86)/(88): Obama at (50,0,0), Dalai Lama at (0,0,0), coordinates in r(π). -/
def obama : Pose := ⟨⟨50, 0, 0⟩, oOb⟩
def dalai : Pose := ⟨⟨0, 0, 0⟩, oDL⟩
/-- (89): the classifiers in the signer's frame r*: same orientations, Obama's at (1,0,0). -/
def clObama : Pose := ⟨⟨1, 0, 0⟩, oOb⟩
def clDalai : Pose := ⟨⟨0, 0, 0⟩, oDL⟩

theorem oOb_rightHanded : RightHandedOrthonormal ⟨0, 1, 0⟩ ⟨-1, 0, 0⟩ ⟨0, 0, 1⟩ := by
  decide +kernel
theorem oDL_rightHanded : RightHandedOrthonormal ⟨0, -1, 0⟩ ⟨1, 0, 0⟩ ⟨0, 0, 1⟩ := by
  decide +kernel
theorem obama_valid : obama.Valid := by decide +kernel
theorem dalai_valid : dalai.Valid := by decide +kernel

def vp (s ts : Rat) (hs : 0 < s) (hts : 0 < ts) : Viewpoint := ⟨idFrame, s, hs, ts, hts⟩
def vp50 : Viewpoint := vp 50 1 (by decide) (by decide)
def vp150 : Viewpoint := vp (1/50) 1 (by decide +kernel) (by decide)

/-- (85) as WRITTEN (center(d,r(π)) = s(π)·center(WORD,r*)) works with s = 50, not 1/50 -/
theorem example_obama_s50 : projStatic True vp50 idFrame clObama obama := by
  refine ⟨trivial, ?_, ?_⟩ <;> decide +kernel
theorem example_dalai_s50 : projStatic True vp50 idFrame clDalai dalai := by
  refine ⟨trivial, ?_, ?_⟩ <;> decide +kernel

/-- ... and FAILS with the paper's stated scaling factor 1/50: the example is inconsistent with
the direction of scaling in (85)(ii)a. -/
theorem example_obama_paper_scale_fails : ¬ projStatic True vp150 idFrame clObama obama := by
  intro h; have := h.2.1; revert this; decide +kernel

/-- With the scaling applied object -> classifier (as the prose of (89) does), 1/50 is right. -/
theorem example_obama_prose_direction :
    center clObama idFrame = (1/50 : Rat) • center obama idFrame := by decide +kernel

/-- The elegant reading: the similarity is a uniform scaling by 50 about the origin. -/
theorem example_obama_sim : projSim True (vp50.toSim idFrame) clObama obama :=
  (projStatic_iff _ _ _ _ _).1 example_obama_s50

/-- Swapping the two orientations breaks projection even when positions match. -/
theorem example_orientation_matters :
    ¬ projStatic True vp50 idFrame clObama ⟨obama.c, oDL⟩ := by
  intro h; have := h.2.2; revert this; decide +kernel

/-- Signer/addressee: doing the same in the addressee-natural frames gives the same verdict
(corollary of the general theorem). -/
theorem example_addressee_frames :
    projStatic True (vp50.rot rotZ180 rotZ180_isRot) (idFrame.rot rotZ180 rotZ180_isRot)
      clObama obama :=
  (projStatic_rot _ _ _ _ _ _ _).2 example_obama_s50

/-- But changing only the signer's axes (leaving r(π)) changes the verdict: the classifier at
x=1 is now at x=-1 in the new coordinates. -/
theorem example_one_sided_change_fails :
    ¬ projStatic True vp50 (idFrame.rot rotZ180 rotZ180_isRot) clObama obama := by
  intro h; have := h.2.1; revert this; decide +kernel

/-- A non-trivial pair of frames: r(π) translated and r* rotated; the transformation `toSim`
is computed by the theorem, and the classifier is placed accordingly. -/
def rstar₂ : Frame := idFrame.rot rotZ180 rotZ180_isRot
def vp₂ : Viewpoint :=
  ⟨⟨⟨10, 0, 0⟩, M3.one, IsRot.one⟩, 50, by decide, 1, by decide⟩
/-- The classifier at absolute (1,0,0) has r*₂-coordinates (-1,0,0); scaled by 50 and placed in the
frame with origin (10,0,0), it lands at absolute (-40,0,0), rotated by 180 degrees about z. -/
example : (vp₂.toSim rstar₂).act clObama = ⟨⟨-40, 0, 0⟩, rotZ180.mul oOb⟩ := by decide +kernel

/-! ### Dynamic example (91) and time scaling -/

/-- classifier moves toward the other one for 1 second: x = 1 - d'/2 -/
def clMove (d' : Rat) : Pose := ⟨⟨1 - d' / 2, 0, 0⟩, oOb⟩
/-- object: x = 50 - 5τ (real time τ, evaluation time t = 0) -/
def obMove (τ : Rat) : Pose := ⟨⟨50 - 5 * τ, 0, 0⟩, oOb⟩

def vpDyn : Viewpoint := vp 50 5 (by decide) (by decide)

theorem example_dynamic : projDyn (fun _ => True) vpDyn idFrame 1 clMove obMove 0 := by
  refine ⟨trivial, fun d' _ _ => ⟨trivial, ?_, ?_⟩⟩
  · ext <;> simp [center, Frame.coord, vpDyn, vp, idFrame, clMove, obMove,
      M3.T, M3.one] <;> grind
  · rfl

/-- With a temporal scale of 1 instead of 5, (91) fails (at d' = 1). -/
theorem example_dynamic_wrong_time_scale :
    ¬ projDyn (fun _ => True) (vp 50 1 (by decide) (by decide)) idFrame 1 clMove obMove 0 := by
  intro ⟨_, h⟩
  have := (h 1 (by decide) (by decide)).2.1
  revert this; decide +kernel

/-- the flight example: 8 h shown in 2 s gives t(π) = 14400. -/
example : ((8 * 60 * 60 : Rat) / 2) = 14400 := by decide +kernel

/-! ### Iconic locus example (129) -/

/-- r(s(π)): origin at chest height 1.2 m. -/
def vpLocus : Viewpoint :=
  ⟨⟨⟨0, 0, 6/5⟩, M3.one, IsRot.one⟩, 3, by decide, 1, by decide⟩
def locusA : Pose := ⟨⟨0, 0, 3/10⟩, M3.one⟩
def headS : Pose := ⟨⟨0, 0, 21/10⟩, M3.one⟩
/-- the head of s(A) at 2.10 m qualifies; orientation is irrelevant (trivialized). -/
theorem example_locus : projLocus True vpLocus idFrame locusA headS := by
  refine ⟨trivial, ?_⟩; decide +kernel

end examples

/-! ## 7. Issues: counterexamples -/

section issues
open V3 M3

/-- fn. 64 with an existential but a LEFT-HANDED object orientation: no similarity (rotation +
scaling + translation) maps the classifier onto it.  Handedness is therefore essential:
(84a)(ii)'s "right-handed" is not decoration. -/
theorem no_sim_to_mirror_pose :
    ¬ ∃ g : Sim, g.act ⟨0, M3.one⟩ = ⟨0, M3.diag 1 1 (-1)⟩ := by
  rintro ⟨g, h⟩
  have := congrArg Pose.O h
  simp only [Sim.act, M3.mul_one] at this
  have hd := g.hQ.2.2
  rw [this] at hd; revert hd; decide +kernel

/-- Likewise a non-unit "orientation triple" (orthogonal but not normalized). -/
theorem no_sim_to_nonunit_pose :
    ¬ ∃ g : Sim, g.act ⟨0, M3.one⟩ = ⟨0, M3.diag 2 2 2⟩ := by
  rintro ⟨g, h⟩
  have := congrArg Pose.O h
  simp only [Sim.act, M3.mul_one] at this
  have hd := g.hQ.2.2
  rw [this] at hd; revert hd; decide +kernel

/-- So without the orthonormality constraint, the existential ("there is a transformation")
reading of fn. 64 is not automatically satisfiable, while with it (`exists_sim_of_valid`) it is
always satisfiable: in both cases a viewpoint-independent existential is the wrong notion. -/
theorem mirror_pose_not_valid : ¬ (⟨0, M3.diag 1 1 (-1)⟩ : Pose).Valid := by decide +kernel

end issues

end IconologicalGeometry