/-
BindingSite.BindingSiteTypes — Core type definitions for the binding site pipeline.

All compute-path fields use Q16_16 (no Float, no Real).
The §5 math sections in BindingSiteEntropy.lean may use Real for theorems.

Design note on entropy encoding:
  B-factors (temperature factors in PDB files) proxy positional uncertainty.
  We map B-factor ∈ [0,100] → entropy ∈ [0,1] using the linear approximation
  entropy = bFactor / 100, represented as Q16_16 raw integer bFactor*65536/100.
  A more accurate ln(1+B)/ln(101) formula requires a multi-range Q16_16.ln;
  the linear map is provably monotone and sufficient as a classification proxy.
-/
import SilverSight.FixedPoint

namespace BindingSite

open SilverSight.FixedPoint

-- ═══════════════════════════════════════════════════════════════════════════
-- §1  Hachimoji state space (8 states, isomorphic to {A,T,G,C,Z,P,B,S})
-- ═══════════════════════════════════════════════════════════════════════════

/-- Eight-state binding site classification.
    Each state corresponds to a distinct entropy/geometry regime. -/
inductive BindingSiteState where
  | Phi    -- Φ: helix/sheet — low entropy, ordered
  | Lambda -- Λ: loop — medium entropy
  | Rho    -- Ρ: random coil — moderate disorder
  | Kappa  -- Κ: kink/turn — sharp geometry
  | Omega  -- Ω: unmodelable (AF3 uncertainty > ground truth)
  | Sigma  -- Σ: surface-exposed, solvated
  | Pi     -- Π: potential binding site (druggable pocket)
  | Zeta   -- Ζ: metal-coordinating (zinc finger etc.)
  deriving BEq, DecidableEq, Repr, Inhabited

-- ═══════════════════════════════════════════════════════════════════════════
-- §2  Amino acid token (20 canonical + Unknown)
-- ═══════════════════════════════════════════════════════════════════════════

inductive AminoAcidToken where
  | Ala | Arg | Asn | Asp | Cys
  | Gln | Glu | Gly | His | Ile
  | Leu | Lys | Met | Phe | Pro
  | Ser | Thr | Trp | Tyr | Val
  | Unknown
  deriving BEq, DecidableEq, Repr, Inhabited

/-- Map a PDB three-letter residue name to an AminoAcidToken.
    The `mod` parameter carries PTM codes (e.g., "phospho"); currently unused. -/
def residueToToken (resName : String) (_mod : String) : AminoAcidToken :=
  match resName.toUpper with
  | "ALA" => .Ala | "ARG" => .Arg | "ASN" => .Asn | "ASP" => .Asp | "CYS" => .Cys
  | "GLN" => .Gln | "GLU" => .Glu | "GLY" => .Gly | "HIS" => .His | "ILE" => .Ile
  | "LEU" => .Leu | "LYS" => .Lys | "MET" => .Met | "PHE" => .Phe | "PRO" => .Pro
  | "SER" => .Ser | "THR" => .Thr | "TRP" => .Trp | "TYR" => .Tyr | "VAL" => .Val
  | _ => .Unknown

-- ═══════════════════════════════════════════════════════════════════════════
-- §3  Entropy → Hachimoji state classifier (Q16_16 thresholds)
-- ═══════════════════════════════════════════════════════════════════════════

-- Threshold raw values for entropy ∈ [0,1] scaled by 65536:
--   0.2 × 65536 = 13107   0.4 × 65536 = 26214
--   0.6 × 65536 = 39321   0.8 × 65536 = 52428
private def thresh_phi   : Int := 13107   -- below → Phi
private def thresh_lam   : Int := 26214   -- below → Lambda (or Phi if not loop)
private def thresh_pi    : Int := 52428   -- below → Pi; at/above → Omega

/-- Map a Q16_16 normalized entropy value to a BindingSiteState.
    Five bands over [0, 1]:
      [0, 0.2)    → Phi (ordered)
      [0.2, 0.4)  → Lambda if loop context, else Phi
      [0.4, 0.6)  → Lambda
      [0.6, 0.8)  → Pi (potential binding site)
      [0.8, 1.0]  → Omega (unmodelable)
    Metal-binding context overrides to Zeta. -/
def entropyToHachimoji (entropy : Q16_16) (isLoopContext : Bool) (isMetalBinding : Bool)
    : BindingSiteState :=
  if isMetalBinding then .Zeta
  else
    let e := entropy.val
    if e < thresh_phi then .Phi
    else if e < thresh_lam then (if isLoopContext then .Lambda else .Phi)
    else if e < 39321 then .Lambda   -- [0.4, 0.6)
    else if e < thresh_pi then .Pi
    else .Omega

-- ═══════════════════════════════════════════════════════════════════════════
-- §4  Residue and profile structs (all floating-point fields are Q16_16)
-- ═══════════════════════════════════════════════════════════════════════════

/-- A single residue's binding-site classification. -/
structure BindingSiteResidue where
  token       : AminoAcidToken
  entropy     : Q16_16                         -- normalized ∈ [0, 1]
  state       : BindingSiteState
  position    : Q16_16 × Q16_16 × Q16_16      -- Ångström coords
  bindability : Q16_16                         -- score ∈ [0, 100]
  deriving Repr, Inhabited

/-- Aggregate entropy profile for a binding site pocket. -/
structure BindingSiteProfile where
  residues     : List BindingSiteResidue
  totalEntropy : Q16_16                        -- mean entropy over residues
  maxEntropy   : Q16_16
  minEntropy   : Q16_16
  siteState    : BindingSiteState
  druggable    : Bool
  receiptHash  : String
  deriving Repr, Inhabited

-- ═══════════════════════════════════════════════════════════════════════════
-- §5  Receipt struct
-- ═══════════════════════════════════════════════════════════════════════════

/-- Complete pipeline receipt: PDB → entropy profile → classification.
    Note: pvgsParams is NOT stored here because PVGS_DQ_Bridge defines its own
    Q16_16 type (`.raw` field) incompatible with Core Q16_16 (`.val` field).
    The codec computes PVGSParams at call time from the profile. -/
structure BindingSiteReceipt where
  version       : String
  pdbId         : String
  entityId      : Nat
  clusterId     : Nat
  profile       : BindingSiteProfile
  dqEnergy      : Int                          -- from dualQuatEnergy.toInt
  stellarRank   : Nat
  helstromBound : Q16_16                       -- quantum discrimination bound
  sha256        : String
  deriving Repr, Inhabited

-- ═══════════════════════════════════════════════════════════════════════════
-- §6  Entropy computation (B-factor proxy, Q16_16, no Float)
-- ═══════════════════════════════════════════════════════════════════════════

/-- Map an integer B-factor ∈ [0, 100] to a Q16_16 normalized entropy in [0, 1].
    Linear approximation: entropy = clamp(bFactor, 0, 100) / 100.
    Monotone, deterministic, no Float. -/
def bFactorToEntropy (bFactor : Nat) : Q16_16 :=
  let clamped : Int := min (bFactor : Int) 100
  Q16_16.ofRawInt (clamped * 65536 / 100)

/-- Average B-factor over a residue and its neighbors, then map to entropy. -/
def entropyFromBFactor (bFactor : Nat) (neighborBFactors : List Nat) : Q16_16 :=
  let total   := bFactor + neighborBFactors.foldl (· + ·) 0
  let denom   := 1 + neighborBFactors.length
  let avgInt  := total / denom                 -- integer division
  bFactorToEntropy avgInt

-- ═══════════════════════════════════════════════════════════════════════════
-- §7  Profile builder helpers (Q16_16 arithmetic)
-- ═══════════════════════════════════════════════════════════════════════════

/-- Q16_16 mean over a non-empty list.  Returns zero for empty lists. -/
def q16Mean (xs : List Q16_16) : Q16_16 :=
  match xs with
  | [] => Q16_16.zero
  | _  =>
    let sum := xs.foldl Q16_16.add Q16_16.zero
    Q16_16.div sum (Q16_16.ofNat xs.length)

/-- Q16_16 maximum over a non-empty list.  Returns zero for empty lists. -/
def q16Max (xs : List Q16_16) : Q16_16 :=
  xs.foldl (fun acc x => if x.val > acc.val then x else acc) Q16_16.zero

/-- Q16_16 minimum over a list; returns Q16_16.maxVal for empty lists
    (so a subsequent min-over-profile is safe). -/
def q16Min (xs : List Q16_16) : Q16_16 :=
  xs.foldl (fun acc x => if x.val < acc.val then x else acc) Q16_16.maxVal

end BindingSite
