QuantumGateType

formal source

  23  | electronic | vibrational | rotational | translational | spin
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26inductive QuantumGateType where
  27  | pauli | clifford | tGate | cnot | toffoli
  28  deriving DecidableEq, Repr, BEq, Fintype
  29
  30theorem energyCount : Fintype.card MolecularEnergyLevel = 5 := by decide
  31theorem gateCount : Fintype.card QuantumGateType = 5 := by decide
  32
  33abbrev QuantumMolecularState : Type := MolecularEnergyLevel × QuantumGateType
  34
  35theorem stateCount : Fintype.card QuantumMolecularState = 25 := by
  36  simp only [QuantumMolecularState, Fintype.card_prod, energyCount, gateCount]
  37
  38/-- 2⁵ = 32 ≥ 25. So ceil(log₂ 25) ≤ 5. -/
  39theorem fiveLayerBound : (2 : ℕ) ^ 5 ≥ 25 := by decide
  40
  41/-- ceil(log₂ 25) = 5. -/
  42theorem log25_eq_5 : Nat.log2 25 + 1 = 5 := by decide
  43
  44theorem energy_surj :
  45    Function.Surjective (fun s : QuantumMolecularState => s.1) := by
  46  intro x; exact ⟨(x, QuantumGateType.pauli), rfl⟩
  47
  48theorem gate_surj :
  49    Function.Surjective (fun s : QuantumMolecularState => s.2) := by
  50  intro x; exact ⟨(MolecularEnergyLevel.electronic, x), rfl⟩
  51
  52structure QuantumMolecularBoundCert where
  53  state_count : Fintype.card QuantumMolecularState = 25
  54  five_layer : (2 : ℕ) ^ 5 ≥ 25
  55  log_five : Nat.log2 25 + 1 = 5
  56  energy_surj : Function.Surjective (fun s : QuantumMolecularState => s.1)