stateCount

formal source

  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)
  57  gate_surj : Function.Surjective (fun s : QuantumMolecularState => s.2)
  58
  59def quantumMolecularBoundCert : QuantumMolecularBoundCert where
  60  state_count := stateCount
  61  five_layer := fiveLayerBound
  62  log_five := log25_eq_5
  63  energy_surj := energy_surj
  64  gate_surj := gate_surj
  65