def
definition
quantumComputingDepthCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QuantumComputingDepthFromRS on GitHub at line 40.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
37 pauli_8 : pauliGroupSize = 2 ^ 3
38 universal_D : universalGates = 3
39
40def quantumComputingDepthCert : QuantumComputingDepthCert where
41 five_gates := quantumGateTypeCount
42 pauli_8 := pauliGroupSize_2cubed
43 universal_D := universalGates_eq_D
44
45end IndisputableMonolith.Physics.QuantumComputingDepthFromRS