`molecularQuantumStateClasses_25`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.QuantumMolecularDesignDepthC4
domain: Physics
line: 29 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.QuantumMolecularDesignDepthC4 on GitHub at line 29.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  26def molecularQuantumStateClasses : ℕ :=
  27  Fintype.card MolecularEnergyLevel * Fintype.card QuantumGateType
  28
  29theorem molecularQuantumStateClasses_25 :
  30    molecularQuantumStateClasses = 25 := by
  31  unfold molecularQuantumStateClasses
  32  rw [molecularEnergyCount, quantumGateTypeCount]
  33
  34theorem molecularQuantumStateClasses_le_2pow5 :
  35    molecularQuantumStateClasses ≤ 2 ^ 5 := by
  36  rw [molecularQuantumStateClasses_25]
  37  norm_num
  38
  39theorem twoPowerFour_lt_stateClasses :
  40    2 ^ 4 < molecularQuantumStateClasses := by
  41  rw [molecularQuantumStateClasses_25]
  42  norm_num
  43
  44structure QuantumMolecularDepthCert where
  45  state_classes_25 : molecularQuantumStateClasses = 25
  46  addressable_by_five_bits : molecularQuantumStateClasses ≤ 2 ^ 5
  47  not_addressable_by_four_bits : 2 ^ 4 < molecularQuantumStateClasses
  48
  49def quantumMolecularDepthCert : QuantumMolecularDepthCert where
  50  state_classes_25 := molecularQuantumStateClasses_25
  51  addressable_by_five_bits := molecularQuantumStateClasses_le_2pow5
  52  not_addressable_by_four_bits := twoPowerFour_lt_stateClasses
  53
  54end QuantumMolecularDesignDepthC4
  55end Physics
  56end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.