-- Hamiltonian Operator Type and Properties
-- Phase 2: Loop Invariant Formalization
-- Status: Immutable operator definition (no physics—just structure metadata)

module Core.Hamiltonian where

open import Data.Nat using (ℕ)
open import Data.Real using (ℝ)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Core.QuantumState using (Dimension)

-- Hamiltonian operator (time-independent)
record Hamiltonian : Set where
  field
    dim : Dimension          -- dimensionality (2^n for n qubits)
    is_hermitian : Bool      -- should be true (unverified bookkeeping)
    matrix_entries : ℕ       -- number of matrix entries (dim.dim²)

-- Predicate: Hamiltonian is properly dimensioned
isValidHamiltonian : Hamiltonian → Set
isValidHamiltonian h =
  let d = Dimension.dim (Hamiltonian.dim h)
  in Hamiltonian.matrix_entries h ≡ d * d

-- Predicate: Hamiltonian is Hermitian (bookkeeping—not verified)
claimsHermitian : Hamiltonian → Set
claimsHermitian h =
  Hamiltonian.is_hermitian h ≡ true

-- Immutability property: Hamiltonian unchanged during evolution
hamiltonianImmutable : (h h' : Hamiltonian) → Set
hamiltonianImmutable h h' =
  (Hamiltonian.dim h ≡ Hamiltonian.dim h') ∧
  (Hamiltonian.matrix_entries h ≡ Hamiltonian.matrix_entries h')