import CoreFormalism.BraidStateN
import CoreFormalism.FixedPoint

open SilverSight.BraidStateN
open SilverSight.FixedPoint
open SilverSight.FixedPoint.Q16_16

namespace SilverSight.HopfFibration

structure Quaternion where
  a : Q16_16
  b : Q16_16
  c : Q16_16
  d : Q16_16
  deriving Repr

namespace Quaternion

def conj (q : Quaternion) : Quaternion :=
  { a := q.a, b := Q16_16.neg q.b, c := Q16_16.neg q.c, d := Q16_16.neg q.d }

def sumSq (q : Quaternion) : Q16_16 :=
  let sq (x : Q16_16) : Q16_16 := Q16_16.mul x x
  Q16_16.add (Q16_16.add (sq q.a) (sq q.b)) (Q16_16.add (sq q.c) (sq q.d))

def isUnit (q : Quaternion) : Prop :=
  (Quaternion.sumSq q).val = Q16_16.one.val

def ofChiralLabel (label : ChiralLabel) : Quaternion :=
  match label with
  | ChiralLabel.achiral_stable          => { a := Q16_16.one,  b := 0, c := 0, d := 0 }
  | ChiralLabel.left_handed_mass_bias   => { a := 0,           b := Q16_16.one, c := 0, d := 0 }
  | ChiralLabel.right_handed_vector_bias => { a := 0,          b := 0, c := Q16_16.one, d := 0 }
  | ChiralLabel.chiral_scarred          => { a := 0,           b := 0, c := 0, d := Q16_16.one }

theorem ofChiralLabel_isUnit (label : ChiralLabel) : isUnit (ofChiralLabel label) := by
  unfold isUnit ofChiralLabel sumSq
  cases label <;> native_decide

end Quaternion

structure PointS7 where
  q1 : Quaternion
  q2 : Quaternion
  deriving Repr

def braidToS7 (s : BraidStateN 8) : PointS7 :=
  let a0 := (s.strands ⟨0, by decide⟩).residue
  let a1 := (s.strands ⟨2, by decide⟩).residue
  let a2 := (s.strands ⟨4, by decide⟩).residue
  let a3 := (s.strands ⟨6, by decide⟩).residue
  { q1 := { a := a0, b := a1, c := 0, d := 0 }
  , q2 := { a := a2, b := a3, c := 0, d := 0 }
  }

end SilverSight.HopfFibration