-- MultiSurfacePacker.lean — Lean decision logic for ΔΦΓΛ Lagrangian
--
-- Formalizes the Multi-Surface Packing Lagrangian optimization and coherence gating
-- using pure, definitionally-reducible Q16_16 fixed-point arithmetic.

import SilverSight.FixedPoint
import Mathlib.Tactic

namespace SilverSight.PIST.MultiSurfacePacker

open SilverSight.FixedPoint
open SilverSight.FixedPoint.Q16_16

-- ============================================================
-- §1  COST & LAGRANGIAN STRUCTURES
-- ============================================================

structure DeltaSurfaceCost where
  deltaL1 : Q16_16
  blockCount : Nat
  avgCompressibility : Q16_16
  deriving Repr, Inhabited, DecidableEq

structure SpectralSurfaceCost where
  sampleCount : Q16_16
  coherence : Q16_16
  spectralEnergy : Q16_16
  deriving Repr, Inhabited, DecidableEq

structure ProgramSurfaceCost where
  descriptionLength : Q16_16
  complexity : Q16_16
  codonCount : Nat
  deriving Repr, Inhabited, DecidableEq

structure MultiSurfaceLagrangian where
  deltaCost : Q16_16
  spectralCost : Q16_16
  programCost : Q16_16
  alpha : Q16_16
  beta : Q16_16
  total : Q16_16
  deriving Repr, Inhabited, DecidableEq

/-- Compute the Lagrangian: L = deltaL1 + alpha * sampleCount + beta * descriptionLength. -/
def computeLagrangian (delta : DeltaSurfaceCost) (spectral : SpectralSurfaceCost)
    (program : ProgramSurfaceCost) (alpha beta : Q16_16) : MultiSurfaceLagrangian :=
  let spectralWeighted := mul alpha spectral.sampleCount
  let programWeighted := mul beta program.descriptionLength
  let total := add delta.deltaL1 (add spectralWeighted programWeighted)
  { deltaCost := delta.deltaL1
    spectralCost := spectralWeighted
    programCost := programWeighted
    alpha := alpha
    beta := beta
    total := total }

-- ============================================================
-- §2  COHERENCE OVERLAP & GATING
-- ============================================================

/-- Custom definitionally-reducible index lookup for List. -/
def get? {α : Type} : List α → Nat → Option α
  | [], _ => none
  | x :: _, 0 => some x
  | _ :: xs, n + 1 => get? xs n

/-- Safely get element from list with default value. -/
def getD (l : List Q16_16) (i : Nat) (default : Q16_16) : Q16_16 :=
  match get? l i with
  | some x => x
  | none => default

/-- Custom definitionally-reducible foldl with index for List. -/
def foldlIdx {α β : Type} (f : β → Nat → α → β) (init : β) (l : List α) : β :=
  let rec loop (i : Nat) (acc : β) : List α → β
    | [] => acc
    | x :: xs => loop (i + 1) (f acc i x) xs
  loop 0 init l

/-- Compute coherence overlap squared between two sample series. -/
def coherenceOverlap (samplesA samplesB : List Q16_16) : Q16_16 :=
  if samplesA.isEmpty ∨ samplesB.isEmpty then
    zero
  else
    let m := min samplesA.length samplesB.length
    let commonA := samplesA.take m
    let commonB := samplesB.take m
    if m = 0 then
      zero
    else
      let sumA := commonA.foldl add zero
      let sumB := commonB.foldl add zero
      let meanA := div sumA (ofNat m)
      let meanB := div sumB (ofNat m)
      let dot := foldlIdx (fun acc i a =>
        let aCentered := sub a meanA
        let bCentered := sub (getD commonB i zero) meanB
        add acc (mul aCentered bCentered)) zero commonA
      let normA := commonA.foldl (fun acc a =>
        let aC := sub a meanA
        add acc (mul aC aC)) zero
      let normB := commonB.foldl (fun acc b =>
        let bC := sub b meanB
        add acc (mul bC bC)) zero
      if normA.toInt = 0 ∧ normB.toInt = 0 then
        one
      else
        let denom := mul normA normB
        if denom.toInt = 0 then
          zero
        else
          div (mul dot dot) denom

/-- Coherence gate: accepts if overlapSq >= 1 - epsilon. -/
def coherenceGate (overlapSq : Q16_16) (epsilon : Q16_16) : Bool :=
  let threshold := sub one epsilon
  overlapSq ≥ threshold

-- ============================================================
-- §3  GCCL SWAP GATE & DECISIONS
-- ============================================================

structure GCDecision where
  accept : Bool
  reject : Bool
  hold : Bool
  quarantine : Bool
  deriving Repr, Inhabited, DecidableEq

/-- GCCL swap decision logic. -/
def gcclSwapGate (oldCost newCost reconRisk : Q16_16) : GCDecision :=
  let improvement := if oldCost > newCost then
    sub oldCost newCost
  else
    zero
  let admissible := improvement ≥ reconRisk
  { accept := admissible
    reject := ¬admissible
    hold := ¬admissible
    quarantine := false }

-- ============================================================
-- §4  RECEIPT STRUCTURE
-- ============================================================

structure MultiSurfaceReceipt where
  schema : String := "multi_surface_packing_v1"
  inputSize : Nat
  deltaCost : Q16_16
  spectralCost : Q16_16
  programCost : Q16_16
  totalLagrangian : Q16_16
  coherencePassed : Bool
  gcclPassed : Bool
  decision : String
  compressedSize : Nat
  compressionRatio : Q16_16
  claimBoundary : String := "multi-surface-packing-lean-core"
  deriving Repr, Inhabited, DecidableEq

def finalizeReceipt (receipt : MultiSurfaceReceipt) : MultiSurfaceReceipt :=
  receipt

-- ============================================================
-- §5  THEOREMS
-- ============================================================

theorem coherenceGateAcceptsIdentical :
    coherenceGate one (ofRawInt 3277) = true := by
  decide

theorem coherenceGateRejectsOrthogonal :
    coherenceGate zero (ofRawInt 3277) = false := by
  decide

theorem gcclRejectsExpansion :
    gcclSwapGate (ofNat 100) (ofNat 200) (ofNat 500) =
    { accept := false, reject := true, hold := true, quarantine := false } := by
  decide

-- ============================================================
-- §6  EXAMPLES
-- ============================================================

def exampleDelta : DeltaSurfaceCost := {
  deltaL1 := ofNat 12800
  blockCount := 4
  avgCompressibility := ofNat 32768
}

def exampleSpectral : SpectralSurfaceCost := {
  sampleCount := ofNat 256
  coherence := ofNat 55705
  spectralEnergy := ofNat 65536
}

def exampleProgram : ProgramSurfaceCost := {
  descriptionLength := ofNat 500
  complexity := ofNat 29491
  codonCount := 150
}

end SilverSight.PIST.MultiSurfacePacker
