/-
Copyright (c) 2026 SilverSight Contributors. All rights reserved.
Released under Apache 2.0 license.

Generic n-dimensional Fisher-Rao geometric rigidity.
Unlike FisherRigidity.lean (which fixes n=8), this version is
parameterized by simplex dimension (n : Nat).

The parabola conjugate pair (s₁·s₂ = -1) is dimension-independent.
Only the inner product, Sidon labels, and strand selection depend on n.
-/

import SilverSight.FixedPoint

namespace SilverSight.PIST.FisherRigidityN

open SilverSight.FixedPoint.Q16_16

-- ── Dimension-independent conjugate pair ──────────────────────────────

def Q16_SCALE : Int := 65536

structure ConjugatePair where
  slope_large : Q16_16
  slope_small : Q16_16
  deriving Repr

def conjugateProduct : Q16_16 := ofRawInt (-Q16_SCALE)

def parabolaConjugatePair (m : Q16_16) : ConjugatePair :=
  let sqrt_term := sqrt (add (mul m m) (ofRawInt Q16_SCALE))
  let s1 := add m sqrt_term
  let s2 := div conjugateProduct s1
  { slope_large := s1, slope_small := s2 }

-- ── Fisher-Rao inner product (generic n) ───────────────────────────────

def fisherInner (n : Nat) (p X Y : Fin n → Q16_16) : Q16_16 :=
  let rec sumFin (i : Nat) (acc : Q16_16) : Q16_16 :=
    if h : i < n then
      sumFin (i + 1) (add acc (div (mul (X ⟨i, h⟩) (Y ⟨i, h⟩)) (p ⟨i, h⟩)))
    else acc
  sumFin 0 zero

-- ── Orthogonality (dimension-independent) ──────────────────────────────

def isOrthogonal (s1 s2 : Q16_16) : Bool :=
  mul s1 s2 == ofRawInt (-Q16_SCALE)

def isOrthogonalWithin (s1 s2 : Q16_16) (tol : Nat) : Bool :=
  let prod_raw := (mul s1 s2).val
  let target_raw := -Q16_SCALE
  decide (Int.natAbs (prod_raw - target_raw) ≤ tol)

-- ── Spectral gap ───────────────────────────────────────────────────────

def eigensolidSpectralGapRaw : Int := 9984

def thresholdOneSeventh : Q16_16 := ofRatio 1 7

lemma spectralGapIntCompare : eigensolidSpectralGapRaw * 7 > Q16_SCALE := by
  unfold eigensolidSpectralGapRaw Q16_SCALE
  norm_num

-- ── Sidon labels (generic n: powers of 2) ──────────────────────────────

def sidonLabels (n : Nat) : Fin n → Q16_16 :=
  fun i => ofRawInt (1 <<< i.val)

-- ── Conjugate strand selection (generic n) ──────────────────────────────

def conjugateStrandSelection (n : Nat) (cp : ConjugatePair) : Fin n → Bool :=
  fun i =>
    let halfScale := ofRawInt 32768
    let usesLargeSlope := cp.slope_large > halfScale
    if usesLargeSlope then i.val % 2 = 0 else i.val % 2 = 1

-- ── n=8 specialization ─────────────────────────────────────────────────

def fisherInner8 : (Fin 8 → Q16_16) → (Fin 8 → Q16_16) → (Fin 8 → Q16_16) → Q16_16 :=
  fisherInner 8

def sidonLabels8 : Fin 8 → Q16_16 := sidonLabels 8

def conjugateStrandSelection8 (cp : ConjugatePair) : Fin 8 → Bool :=
  conjugateStrandSelection 8 cp

lemma m1SelectsEvenStrands : conjugateStrandSelection 8 (parabolaConjugatePair (ofRawInt Q16_SCALE)) ⟨0, by decide⟩ = true := by
  unfold conjugateStrandSelection parabolaConjugatePair conjugateProduct Q16_SCALE ofRawInt
  decide

lemma m1_orthogonal_within_4 :
    let cp := parabolaConjugatePair (ofRawInt Q16_SCALE)
    isOrthogonalWithin cp.slope_large cp.slope_small 4 = true := by
  unfold parabolaConjugatePair isOrthogonalWithin conjugateProduct Q16_SCALE ofRawInt
  decide

end SilverSight.PIST.FisherRigidityN
