theorem
proved
twoPowerFour_lt_stateClasses
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QuantumMolecularDesignDepthC4 on GitHub at line 39.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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