def
definition
molecularQuantumStateClasses
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QuantumMolecularDesignDepthC4 on GitHub at line 26.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
23open MolecularPhysicsFromRS
24open QuantumComputingDepthFromRS
25
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