/-
Copyright (c) 2026 SilverSight Contributors. All rights reserved.
Released under Apache 2.0 license.
-/
import Mathlib.Data.Nat.Basic

/-! # Cost Transparency and Model Selection Framework

All costs are in millicents (integer Nat) to avoid typeclass issues.
-/

namespace SilverSight.CollectiveIntelligence

/-- Millicents: 1/1000 of a cent. Integer arithmetic, no floats. -/
def Millicents := Nat

/-- Explicit cost parameters in millicents. -/
structure CostParams where
  inputCostPer1k : Nat
  outputCostPer1k : Nat
  fixedOverhead : Nat
  deriving Repr

/-- Explicit cost calculation: C = c_in * |I|/1000 + c_out * |O|/1000 + c_fixed. -/
def explicitCost (p : CostParams) (inToks outToks : Nat) : Nat :=
  (p.inputCostPer1k * inToks / 1000) +
  (p.outputCostPer1k * outToks / 1000) +
  p.fixedOverhead

/-- Model with cost and dual quaternion χ as Nat ratio. -/
structure Model where
  name : String
  cost : CostParams
  chiNum : Nat
  chiDen : Nat
  deriving Repr

/-- Coordination cost in millicents. $0.01 = 1000 mc, $0.10 max = 10000 mc. -/
def coordinationCostMC (n : Nat) : Nat :=
  if n ≤ 1 then 0
  else if n = 2 then 1000
  else min (2000*(n-1)) 10000

/-- Coordination cost never exceeds $0.10 (10000 millicents). -/
theorem coordinationCost_bounded (n : Nat) : coordinationCostMC n ≤ 10000 := by
  unfold coordinationCostMC
  by_cases h1 : n ≤ 1
  · simp [h1]
  · by_cases h2 : n = 2
    · simp [h1, h2]
    · simp [h1, h2]
      apply Nat.min_le_right

end SilverSight.CollectiveIntelligence
