logo

Show the Proof

In [1]:
import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof
Out[1]:
 step typerequirementsstatement
0instantiation1, 2, 3, 4, 5, 6, 7,  ⊢  
  : , : , : , : , : , :
1theorem  ⊢  
 proveit.physics.quantum.algebra.scalar_mult_absorption
2instantiation8, 9, 10  ⊢  
  : , :
3reference94  ⊢  
4reference42  ⊢  
5reference22  ⊢  
6reference43  ⊢  
7instantiation11, 12, 13,  ⊢  
  : , : , :
8theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
9instantiation97, 68, 14  ⊢  
  : , : , :
10instantiation30, 15, 16  ⊢  
  : , : , :
11theorem  ⊢  
 proveit.logic.equality.sub_left_side_into
12instantiation17, 50, 51, 18, 19,  ⊢  
  : , : , : , :
13instantiation20, 21, 22  ⊢  
  : , : , :
14instantiation97, 73, 23  ⊢  
  : , : , :
15instantiation55, 33, 24  ⊢  
  : , :
16instantiation25, 26, 27  ⊢  
  : , : , :
17theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_ket_in_QmultCodomain
18instantiation49, 50, 51, 28  ⊢  
  : , : , :
19instantiation29, 96, 82  ⊢  
  : , :
20axiom  ⊢  
 proveit.physics.quantum.algebra.multi_qmult_def
21theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
22instantiation58  ⊢  
  : , :
23theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.e_is_real_pos
24instantiation30, 31, 32  ⊢  
  : , : , :
25axiom  ⊢  
 proveit.logic.equality.equals_transitivity
26instantiation41, 99, 34, 42, 36, 43, 33, 56, 57, 45  ⊢  
  : , : , : , : , : , :
27instantiation41, 42, 94, 34, 43, 35, 36, 46, 47, 56, 57, 45  ⊢  
  : , : , : , : , : , :
28instantiation37, 50, 51, 38, 39  ⊢  
  : , : , : , : , :
29theorem  ⊢  
 proveit.physics.quantum.algebra.num_ket_in_register_space
30theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
31instantiation55, 40, 45  ⊢  
  : , :
32instantiation41, 42, 94, 99, 43, 44, 56, 57, 45  ⊢  
  : , : , : , : , : , :
33instantiation55, 46, 47  ⊢  
  : , :
34theorem  ⊢  
 proveit.numbers.numerals.decimals.nat3
35instantiation58  ⊢  
  : , :
36instantiation48  ⊢  
  : , : , :
37theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_op_is_op
38instantiation49, 50, 51, 52  ⊢  
  : , : , :
39instantiation53, 76, 54  ⊢  
  : , : , :
40instantiation55, 56, 57  ⊢  
  : , :
41theorem  ⊢  
 proveit.numbers.multiplication.disassociation
42axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
43theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
44instantiation58  ⊢  
  : , :
45instantiation97, 68, 59  ⊢  
  : , : , :
46instantiation97, 68, 60  ⊢  
  : , : , :
47instantiation97, 68, 61  ⊢  
  : , : , :
48theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
49theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_op_is_linmap
50instantiation62, 76  ⊢  
  :
51theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_set_is_hilbert_space
52instantiation63, 96, 64  ⊢  
  : , :
53theorem  ⊢  
 proveit.physics.quantum.algebra.qmult_matrix_is_linmap
54instantiation65, 66, 67  ⊢  
  : , : , :
55theorem  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
56theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.i_is_complex
57instantiation97, 68, 69  ⊢  
  : , : , :
58theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
59instantiation97, 71, 70  ⊢  
  : , : , :
60instantiation97, 71, 72  ⊢  
  : , : , :
61instantiation97, 73, 74  ⊢  
  : , : , :
62theorem  ⊢  
 proveit.linear_algebra.inner_products.complex_vec_set_is_hilbert_space
63theorem  ⊢  
 proveit.physics.quantum.algebra.num_bra_is_lin_map
64assumption  ⊢  
65theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
66instantiation75, 76  ⊢  
  :
67instantiation77, 96  ⊢  
  :
68theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
69theorem  ⊢  
 proveit.physics.quantum.QPE._phase_is_real
70instantiation97, 79, 78  ⊢  
  : , : , :
71theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
72instantiation97, 79, 90  ⊢  
  : , : , :
73theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
74theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pi_is_real_pos
75theorem  ⊢  
 proveit.linear_algebra.matrices.unitaries_are_matrices
76instantiation80, 94, 91  ⊢  
  : , :
77theorem  ⊢  
 proveit.physics.quantum.QFT.invFT_is_unitary
78instantiation97, 81, 82  ⊢  
  : , : , :
79theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
80theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
81instantiation83, 84, 85  ⊢  
  : , :
82assumption  ⊢  
83theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
84theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
85instantiation86, 87, 88  ⊢  
  : , :
86theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
87instantiation89, 90, 91  ⊢  
  : , :
88instantiation92, 93  ⊢  
  :
89theorem  ⊢  
 proveit.numbers.exponentiation.exp_int_closure
90instantiation97, 98, 94  ⊢  
  : , : , :
91instantiation97, 95, 96  ⊢  
  : , : , :
92theorem  ⊢  
 proveit.numbers.negation.int_closure
93instantiation97, 98, 99  ⊢  
  : , : , :
94theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
95theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
96axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
97theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
98theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
99theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1