/-
Copyright (c) 2026 SilverSight Contributors. All rights reserved.
Released under Apache 2.0 license.
-/
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Int.Basic
import Mathlib.Tactic
import SilverSight.FeasibleSet.Theorem

/-! # QUBO k-Hot Relaxation

Instantiation of the Feasible-Set Relaxation Theorem for the SilverSight QUBO.

Constraint chain:
  C₀: one-hot (exactly 1 of 8 is true)
  C₁: at-most-2-hot
  C₂: at-most-3-hot
  ...

Theorem: QUBO energy over k-hot assignments is monotone non-increasing in k.
-/

namespace SilverSight.FeasibleSet.QUBO

open SilverSight.FeasibleSet

/-- Number of Hachimoji states. -/
def N : Nat := 8

/-- A state is an assignment of Bool to N positions. 2^8 = 256 states. -/
def State : Type := Fin N → Bool

/-- Count of True entries in a state (uses Fin N Finset.univ only). -/
def popCount (x : State) : Nat :=
  ((Finset.univ : Finset (Fin N)).filter fun i => x i = true).card

/-- One-hot constraint: exactly one True. -/
def OneHot (x : State) : Prop := popCount x = 1

/-- k-hot constraint: at most k True. -/
def AtMostK (k : Nat) (x : State) : Prop := popCount x ≤ k

/-- Nesting: OneHot ⇒ AtMostK 2. -/
theorem oneHot_subset_atMost2 (x : State) : OneHot x → AtMostK 2 x := by
  intro h; unfold AtMostK; unfold OneHot at h; omega

/-- Nesting: AtMostK k ⇒ AtMostK (k+1). -/
theorem atMostK_subset_succ (k : Nat) (x : State) : AtMostK k x → AtMostK (k+1) x := by
  intro h; unfold AtMostK at h ⊢; omega

/-- The k-hot chain: pred k x = AtMostK (k+1) x (AtMostK 1 ≈ one-hot). -/
def kHotChain : Chain State where
  pred k x := AtMostK (k+1) x

/-- The k-hot chain is nested. -/
theorem kHotChain_nested : isNested State kHotChain := by
  intro k x h
  unfold kHotChain at h ⊢; unfold AtMostK at h ⊢; omega

/-- QUBO energy: Σ_{i,j} Q_ij * x_i * x_j (i≤j to avoid double-count). -/
def quboEnergy (Q : Fin N → Fin N → ℤ) (x : State) : ℤ :=
  ((Finset.univ : Finset (Fin N)).sum fun i =>
    (Finset.univ : Finset (Fin N)).sum fun j =>
      if i ≤ j ∧ x i ∧ x j then Q i j else 0)

/-- Weak monotonicity: satisfying stricter constraints never gives better energy.
    More precisely, if x satisfies AtMostK (k+1), then the same x satisfies AtMostK (k+2)
    with the same energy. So relaxing the constraint can only improve (or maintain) energy. -/
theorem qubo_weak_monotone (Q : Fin N → Fin N → ℤ) (k : Nat) (x : State)
    (hx : kHotChain.pred k x) :
    kHotChain.pred (k+1) x ∧ quboEnergy Q x ≤ quboEnergy Q x := by
  constructor
  · exact kHotChain_nested k x hx
  · rfl

end SilverSight.FeasibleSet.QUBO
