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

NGemetry.lean — N-Dimensional Geometry Extension

Extends SpatialEvo from 3D to n-dimensional geometry for VLSI design
and general spatial reasoning applications.

Key contributions:
1. Generic PointND structure for n-dimensional points
2. Generic VectorND structure for n-dimensional vectors
3. N-dimensional spatial algorithms (distance, ordering, orientation)
4. N-dimensional camera pose and scene representation
5. Verification examples and theorems

Per AGENTS.md §1.4: Uses Q16_16 fixed-point for hardware-native computation.
Per AGENTS.md §2: PascalCase types, camelCase functions.
Per AGENTS.md §4: All defs must have eval witnesses or theorems.
-/

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Vector.Basic
import Mathlib.Data.List.Basic
import Mathlib.Tactic

set_option linter.unusedSimpArgs false

namespace Semantics.NGemetry

-- ════════════════════════════════════════════════════════════
-- §0  Fixed-Point Precision (Q16.16 for n-dimensional computations)
-- ════════════════════════════════════════════════════════════

/-- Q16.16 fixed-point for n-dimensional geometry. -/
structure Q1616 where
  raw : Int
  deriving Repr, DecidableEq, Inhabited, BEq

namespace Q1616

def zero    : Q1616 := ⟨0⟩
def one     : Q1616 := ⟨65536⟩        -- 0x00010000 = 1.0

def ofNat (n : Nat) : Q1616 := ⟨n * 65536⟩

def add (a b : Q1616) : Q1616 := ⟨a.raw + b.raw⟩
def sub (a b : Q1616) : Q1616 := ⟨a.raw - b.raw⟩
def mul (a b : Q1616) : Q1616 := ⟨(a.raw * b.raw) / 65536⟩
def div (a b : Q1616) : Q1616 := ⟨(a.raw * 65536) / b.raw⟩

instance : Add Q1616 := ⟨add⟩
instance : Sub Q1616 := ⟨sub⟩
instance : Mul Q1616 := ⟨mul⟩
instance : Div Q1616 := ⟨div⟩
instance : Neg Q1616 := ⟨fun a => ⟨-a.raw⟩⟩

instance : LE Q1616 := ⟨fun a b => a.raw ≤ b.raw⟩
instance : LT Q1616 := ⟨fun a b => a.raw < b.raw⟩

/-- Absolute value. -/
def abs (a : Q1616) : Q1616 := if a.raw < 0 then ⟨-a.raw⟩ else a

/-- Minimum of two values. -/
def min (a b : Q1616) : Q1616 := if a ≤ b then a else b

/-- Maximum of two values. -/
def max (a b : Q1616) : Q1616 := if a ≥ b then a else b

-- Key algebraic lemmas

@[ext]
theorem ext {a b : Q1616} (h : a.raw = b.raw) : a = b := congrArg Q1616.mk h

@[simp] theorem zero_raw : Q1616.zero.raw = 0 := rfl
@[simp] theorem add_zero (a : Q1616) : Q1616.add a Q1616.zero = a := by
  ext; simp [add, zero]
@[simp] theorem mul_zero (a : Q1616) : Q1616.mul a Q1616.zero = Q1616.zero := by
  ext; simp [mul, zero]
@[simp] theorem zero_mul (a : Q1616) : Q1616.mul Q1616.zero a = Q1616.zero := by
  ext; simp [mul, zero]
@[simp] theorem sub_self (a : Q1616) : Q1616.sub a a = Q1616.zero := by
  ext; simp [sub, zero]

theorem mul_comm (a b : Q1616) : Q1616.mul a b = Q1616.mul b a := by
  ext; simp [mul, Int.mul_comm]

-- (a-b)² = (b-a)²  because -(a-b) = b-a and (-x)² = x² in Int division
theorem sq_sub_eq_sq_sub_symm (a b : Q1616) :
    Q1616.mul (Q1616.sub a b) (Q1616.sub a b) =
    Q1616.mul (Q1616.sub b a) (Q1616.sub b a) := by
  ext; simp [mul, sub]; ring

end Q1616

-- ════════════════════════════════════════════════════════════
-- §1  N-Dimensional Point and Vector Structures
-- ════════════════════════════════════════════════════════════

/-- N-dimensional point in space. -/
structure PointND (n : Nat) where
  coordinates : Array Q1616
  dimension : Nat := n
  hDim : dimension = n
  deriving Repr

instance (n : Nat) : Inhabited (PointND n) where
  default := { coordinates := Array.replicate n Q1616.zero, hDim := rfl }

namespace PointND

/-- Create point from array of coordinates. -/
def fromArray (coords : Array Q1616) (n : Nat) : PointND n :=
  { coordinates := coords, dimension := n, hDim := rfl }

/-- Get coordinate at index i. Uses safe Array.getD (no size invariant in struct). -/
def getCoord (p : PointND n) (i : Nat) (_ : i < n) : Q1616 :=
  p.coordinates.getD i Q1616.zero

/-- Safe coordinate access with default zero. -/
@[inline] def getCoordD (p : PointND n) (i : Nat) : Q1616 :=
  p.coordinates.getD i Q1616.zero

/-- Euclidean distance between two n-dimensional points (squared sum, no sqrt). -/
def euclideanDistance (p1 p2 : PointND n) : Q1616 :=
  let dim := p1.dimension
  (List.range dim).foldl (fun acc i =>
    let diff := Q1616.sub (p1.getCoordD i) (p2.getCoordD i)
    Q1616.add acc (Q1616.mul diff diff)
  ) Q1616.zero

/-- Manhattan distance between two n-dimensional points. -/
def manhattanDistance (p1 p2 : PointND n) : Q1616 :=
  let dim := p1.dimension
  (List.range dim).foldl (fun acc i =>
    Q1616.add acc (Q1616.abs (Q1616.sub (p1.getCoordD i) (p2.getCoordD i)))
  ) Q1616.zero

/-- Origin point in n-dimensional space. -/
def origin (n : Nat) : PointND n :=
  fromArray (Array.replicate n Q1616.zero) n

-- origin's dimension field equals n
@[simp] theorem origin_dimension (n : Nat) : (origin n).dimension = n := rfl

-- getCoordD on origin always returns zero.
@[simp] theorem origin_getCoordD (n : Nat) (i : Nat) :
    (origin n).getCoordD i = Q1616.zero := by
  simp only [getCoordD, origin, fromArray]
  by_cases hi : i < n
  · have hsize : i < (Array.replicate n Q1616.zero).size := Array.size_replicate ▸ hi
    simp [Array.getD, hsize, Array.getElem_replicate]
  · have hsize : ¬ i < (Array.replicate n Q1616.zero).size := by
      simpa [Array.size_replicate] using hi
    simp [Array.getD, hsize]

end PointND

/-- N-dimensional vector in space. -/
structure VectorND (n : Nat) where
  components : Array Q1616
  dimension : Nat := n
  hDim : dimension = n
  deriving Repr

instance (n : Nat) : Inhabited (VectorND n) where
  default := { components := Array.replicate n Q1616.zero, dimension := n, hDim := rfl }

namespace VectorND

/-- Create vector from array of components. -/
def fromArray (comps : Array Q1616) (n : Nat) : VectorND n :=
  { components := comps, dimension := n, hDim := rfl }

/-- Get component at index i. Uses safe Array.getD (no size invariant in struct). -/
def getComp (v : VectorND n) (i : Nat) (_ : i < n) : Q1616 :=
  v.components.getD i Q1616.zero

/-- Safe component access with default zero. -/
@[inline] def getCompD (v : VectorND n) (i : Nat) : Q1616 :=
  v.components.getD i Q1616.zero

/-- Vector addition. -/
def add (v1 v2 : VectorND n) : VectorND n :=
  let dim := v1.dimension
  let newComps := (List.range dim).toArray.map (fun i =>
    Q1616.add (v1.getCompD i) (v2.getCompD i)
  )
  fromArray newComps n

/-- Vector subtraction. -/
def sub (v1 v2 : VectorND n) : VectorND n :=
  let dim := v1.dimension
  let newComps := (List.range dim).toArray.map (fun i =>
    Q1616.sub (v1.getCompD i) (v2.getCompD i)
  )
  fromArray newComps n

/-- Dot product of two n-dimensional vectors. -/
def dot (v1 v2 : VectorND n) : Q1616 :=
  let dim := v1.dimension
  (List.range dim).foldl (fun acc i =>
    Q1616.add acc (Q1616.mul (v1.getCompD i) (v2.getCompD i))
  ) Q1616.zero

/-- Vector magnitude (Euclidean norm squared — no sqrt for Q16.16). -/
def magnitude (v : VectorND n) : Q1616 :=
  dot v v

/-- Normalize vector to unit length. -/
def normalize (v : VectorND n) : VectorND n :=
  let mag := magnitude v
  let dim := v.dimension
  if mag = Q1616.zero then
    v  -- Return zero vector unchanged
  else
    let newComps := (List.range dim).toArray.map (fun i =>
      Q1616.div (v.getCompD i) mag
    )
    fromArray newComps n

/-- Zero vector in n-dimensional space. -/
def zero (n : Nat) : VectorND n :=
  fromArray (Array.replicate n Q1616.zero) n

-- getCompD on zero vector always returns Q1616.zero
@[simp] theorem zero_getCompD (n : Nat) (i : Nat) :
    (zero n).getCompD i = Q1616.zero := by
  simp only [getCompD, zero, fromArray]
  by_cases hi : i < n
  · have hsize : i < (Array.replicate n Q1616.zero).size := Array.size_replicate ▸ hi
    simp [Array.getD, hsize, Array.getElem_replicate]
  · have hsize : ¬ i < (Array.replicate n Q1616.zero).size := by
      simpa [Array.size_replicate] using hi
    simp [Array.getD, hsize]

end VectorND

-- ════════════════════════════════════════════════════════════
-- §2  N-Dimensional Camera and Scene Structures
-- ════════════════════════════════════════════════════════════

/-- N-dimensional camera pose (position + orientation). -/
structure CameraPoseND (n : Nat) where
  position : PointND n
  rotation : VectorND n  -- Simplified: n-dimensional rotation parameters
  frameIndex : Nat
  deriving Repr

instance (n : Nat) : Inhabited (CameraPoseND n) where
  default := { position := default, rotation := default, frameIndex := 0 }

/-- N-dimensional point cloud with density metric. -/
structure PointCloudND (n : Nat) where
  points : Array (PointND n)
  density : Q1616  -- Points per unit volume
  dimension : Nat := n
  deriving Repr, Inhabited

/-- N-dimensional bounding hyperbox. -/
structure BoundingHyperbox (n : Nat) where
  min : PointND n
  max : PointND n
  deriving Repr

instance (n : Nat) : Inhabited (BoundingHyperbox n) where
  default := { min := default, max := default }

/-- N-dimensional scene containing geometric assets. -/
structure SceneND (n : Nat) where
  name : String
  pointCloud : PointCloudND n
  cameraPoses : Array (CameraPoseND n)
  objects : Array (BoundingHyperbox n)
  deriving Repr, Inhabited

-- ════════════════════════════════════════════════════════════
-- §3  N-Dimensional Spatial Algorithms
-- ════════════════════════════════════════════════════════════

/-- Compute camera orientation vector between two n-dimensional poses.
    Returns a VectorND representing coordinate-wise displacement from pose1 to pose2. -/
def computeCameraOrientationND (n : Nat) (pose1 pose2 : CameraPoseND n) : VectorND n :=
  let newComps := (List.range n).toArray.map (fun i =>
    Q1616.sub (pose2.position.getCoordD i) (pose1.position.getCoordD i)
  )
  VectorND.fromArray newComps n

/-- Compute depth ordering for n-dimensional objects.
    Requires n > 0 to access the 0th coordinate safely.
    NOTE: The original had `by sorry` for `0 < n`; now made explicit via `hn`. -/
def computeDepthOrderingND (n : Nat) (hn : 0 < n) (camera : PointND n)
    (objects : Array (BoundingHyperbox n)) : Array Nat :=
  let distances := objects.mapIdx (fun i obj =>
    let center := PointND.fromArray
      (Array.replicate n (Q1616.div
        (Q1616.add (obj.min.getCoord 0 hn) (obj.max.getCoord 0 hn))
        Q1616.one)) n
    let dist := PointND.euclideanDistance camera center
    (i, dist)
  )
  distances.map (fun p => p.1)

/-- Compute object distance in n-dimensional space.
    Requires n > 0 to access the 0th coordinate safely.
    NOTE: The original had `by sorry` for `0 < n`; now made explicit via `hn`. -/
def computeObjectDistanceND (n : Nat) (hn : 0 < n)
    (obj1 obj2 : BoundingHyperbox n) : Q1616 :=
  let center1 := PointND.fromArray
    (Array.replicate n (Q1616.div
      (Q1616.add (obj1.min.getCoord 0 hn) (obj1.max.getCoord 0 hn))
      Q1616.one)) n
  let center2 := PointND.fromArray
    (Array.replicate n (Q1616.div
      (Q1616.add (obj2.min.getCoord 0 hn) (obj2.max.getCoord 0 hn))
      Q1616.one)) n
  PointND.euclideanDistance center1 center2

/-- Check if two n-dimensional bounding hyperboxes intersect. -/
def hyperboxIntersection (_n : Nat) (_box1 _box2 : BoundingHyperbox _n) : Bool :=
  false  -- TODO(lean-port): Implement proper n-dimensional intersection test

-- ════════════════════════════════════════════════════════════
-- §4  Theorems: N-Dimensional Geometry Properties
-- ════════════════════════════════════════════════════════════

/-- Theorem: Origin point has zero distance to itself. -/
theorem originDistanceZero (n : Nat) :
    PointND.euclideanDistance (PointND.origin n) (PointND.origin n) = Q1616.zero := by
  simp only [PointND.euclideanDistance]
  have hdim : (PointND.origin n).dimension = n := rfl
  rw [hdim]
  apply List.foldl_fixed'
  intro i
  simp [Q1616.sub_self, Q1616.mul_zero, Q1616.add_zero]

/-- Theorem: Euclidean distance is symmetric. -/
theorem euclideanDistanceSymmetric (n : Nat) (p1 p2 : PointND n) :
    PointND.euclideanDistance p1 p2 = PointND.euclideanDistance p2 p1 := by
  simp only [PointND.euclideanDistance]
  have h1 : p1.dimension = n := p1.hDim
  have h2 : p2.dimension = n := p2.hDim
  rw [h1, h2]
  have hf : (fun (acc : Q1616) (i : Nat) =>
        Q1616.add acc (Q1616.mul (Q1616.sub (p1.getCoordD i) (p2.getCoordD i))
                                   (Q1616.sub (p1.getCoordD i) (p2.getCoordD i)))) =
      (fun (acc : Q1616) (i : Nat) =>
        Q1616.add acc (Q1616.mul (Q1616.sub (p2.getCoordD i) (p1.getCoordD i))
                                   (Q1616.sub (p2.getCoordD i) (p1.getCoordD i)))) := by
    funext acc i; congr 1; exact Q1616.sq_sub_eq_sq_sub_symm _ _
  rw [hf]

-- ── helpers for manhattanTriangleInequality ─────────────────────────────────

/-- Taking .raw commutes with foldl+Q1616.add. -/
private lemma foldl_add_raw (f : Nat → Q1616) (l : List Nat) (init : Q1616) :
    (l.foldl (fun acc i => Q1616.add acc (f i)) init).raw =
    l.foldl (fun acc i => acc + (f i).raw) init.raw := by
  induction l generalizing init with
  | nil => simp
  | cons h t ih =>
      simp only [List.foldl_cons]
      rw [ih (Q1616.add init (f h))]
      simp [Q1616.add]

/-- (Q1616.abs (Q1616.sub a b)).raw = abs (a.raw - b.raw) as Int. -/
private lemma abs_sub_raw (a b : Q1616) :
    (Q1616.abs (Q1616.sub a b)).raw = abs (a.raw - b.raw) := by
  simp only [Q1616.abs, Q1616.sub]
  split_ifs with h
  · exact (abs_of_neg h).symm
  · exact (abs_of_nonneg (not_lt.mp h)).symm

/-- foldl-sum monotonicity for any coordinatewise bound (no ∈ membership needed). -/
private lemma foldl_le_sum_gen (f g h : Nat → Int) (l : List Nat) (af ag ah : Int)
    (hacc : af ≤ ag + ah)
    (hfgh : ∀ i, f i ≤ g i + h i) :
    l.foldl (fun acc i => acc + f i) af ≤
    l.foldl (fun acc i => acc + g i) ag +
    l.foldl (fun acc i => acc + h i) ah := by
  induction l generalizing af ag ah with
  | nil => simpa
  | cons k t ih =>
      simp only [List.foldl_cons]
      apply ih
      have := hfgh k; omega

/-- Coordinatewise Int abs triangle inequality. -/
private lemma int_abs_triangle (a b c : Int) :
    abs (a - c) ≤ abs (a - b) + abs (b - c) := by
  have h1 : a - b ≤ abs (a - b) := le_abs_self _
  have h2 : b - c ≤ abs (b - c) := le_abs_self _
  have h3 : -(a - b) ≤ abs (a - b) := by
    have := le_abs_self (-(a - b)); rwa [abs_neg] at this
  have h4 : -(b - c) ≤ abs (b - c) := by
    have := le_abs_self (-(b - c)); rwa [abs_neg] at this
  apply abs_le.mpr; constructor <;> linarith

/-- Manhattan distance satisfies the triangle inequality.
    Proof: coordinatewise abs(p1-p3) ≤ abs(p1-p2) + abs(p2-p3),
    lifted to fold sums by foldl_le_sum_gen. -/
theorem manhattanTriangleInequality (n : Nat) (p1 p2 p3 : PointND n) :
    let d12 := PointND.manhattanDistance p1 p2
    let d23 := PointND.manhattanDistance p2 p3
    let d13 := PointND.manhattanDistance p1 p3
    d13 ≤ d12 + d23 := by
  show (PointND.manhattanDistance p1 p3).raw ≤
       (PointND.manhattanDistance p1 p2).raw + (PointND.manhattanDistance p2 p3).raw
  simp only [PointND.manhattanDistance]
  rw [foldl_add_raw, foldl_add_raw, foldl_add_raw]
  simp only [abs_sub_raw, Q1616.zero]
  rw [p1.hDim, p2.hDim]
  apply foldl_le_sum_gen
  · simp
  · intro i
    exact int_abs_triangle (p1.getCoordD i).raw (p2.getCoordD i).raw (p3.getCoordD i).raw

/-- Theorem: Dot product is commutative. -/
theorem dotProductCommutative (n : Nat) (v1 v2 : VectorND n) :
    VectorND.dot v1 v2 = VectorND.dot v2 v1 := by
  simp only [VectorND.dot]
  have h1 : v1.dimension = n := v1.hDim
  have h2 : v2.dimension = n := v2.hDim
  rw [h1, h2]
  have hf : (fun (acc : Q1616) (i : Nat) =>
        Q1616.add acc (Q1616.mul (v1.getCompD i) (v2.getCompD i))) =
      (fun (acc : Q1616) (i : Nat) =>
        Q1616.add acc (Q1616.mul (v2.getCompD i) (v1.getCompD i))) := by
    funext acc i; congr 1; exact Q1616.mul_comm _ _
  rw [hf]

/-- Theorem: Zero vector has zero magnitude. -/
theorem zeroVectorMagnitude (n : Nat) :
    VectorND.magnitude (VectorND.zero n) = Q1616.zero := by
  simp only [VectorND.magnitude, VectorND.dot]
  have hdim : (VectorND.zero n).dimension = n := rfl
  rw [hdim]
  apply List.foldl_fixed'
  intro i
  simp [Q1616.mul_zero, Q1616.add_zero]

-- ════════════════════════════════════════════════════════════
-- §5  Verification Examples
-- ════════════════════════════════════════════════════════════

#eval PointND.origin 3  -- Expected: Point with 3 zero coordinates

#eval let p1 := PointND.fromArray (#[Q1616.ofNat 1, Q1616.ofNat 2, Q1616.ofNat 3]) 3
      let p2 := PointND.fromArray (#[Q1616.ofNat 4, Q1616.ofNat 5, Q1616.ofNat 6]) 3
      PointND.euclideanDistance p1 p2  -- Expected: squared distance between points

#eval let v := VectorND.fromArray (#[Q1616.ofNat 1, Q1616.ofNat 0, Q1616.ofNat 0]) 3
      VectorND.magnitude v  -- Expected: magnitude (squared) of vector

#eval let v1 := VectorND.fromArray (#[Q1616.ofNat 1, Q1616.ofNat 2, Q1616.ofNat 3]) 3
      let v2 := VectorND.fromArray (#[Q1616.ofNat 4, Q1616.ofNat 5, Q1616.ofNat 6]) 3
      VectorND.dot v1 v2  -- Expected: dot product

end Semantics.NGemetry