Proof of proveit.physics.quantum.QPE._sample_space_bijection theorem

import proveit
theory = proveit.Theory() # the theorem's theory

from proveit import defaults
from proveit import f, m, n, x, y, A
from proveit.logic import InSet, NotEquals
from proveit.logic.sets.functions.bijections import bijective_by_uniqueness
from proveit.physics.quantum.QPE import (_t, _s, _t_in_natural_pos, _s_in_nat_pos,
                                         _sample_space_def)

%proving _sample_space_bijection

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_sample_space_bijection:
(see dependencies)

_sample_space_def

 ⊢  

We want to use $\Omega$ as our shorthand for the sample space:

defaults.replacements = set([_sample_space_def.derive_reversed()])

defaults.replacements:

lambda_map = _sample_space_bijection.element

lambda_map:

domain = _sample_space_bijection.domain.domain

domain:

In order to show that the image of the map is a bijection, we want to show that distinct elements of the domain map to distinct quantum circuits.

assumptions = [InSet(m, domain), InSet(n, domain), NotEquals(m, n)]

assumptions:

NotEquals(lambda_map.apply(m), lambda_map.apply(n)).prove(
    assumptions=assumptions)

, ,  ⊢  

bijective_by_uniqueness

 ⊢  

bijective_by_uniqueness.instantiate(
    {f:lambda_map, A:domain, x:m, y:n}).derive_consequent()

 ⊢  

_sample_space_bijection has been proven.  Now simply execute "%qed".

%qed

proveit.physics.quantum.QPE._sample_space_bijection has been proven.

	step type	requirements	statement
0	modus ponens	1, 2	⊢
1	instantiation	3, 4*, 5*	⊢
	: , : , : , :
2	generalization	6	⊢
3	conjecture		⊢
	proveit.logic.sets.functions.bijections.bijective_by_uniqueness
4	instantiation	7, 8*	, ,  ⊢
	: , :
5	instantiation	9, 10*	⊢
	: , :
6	axiom		⊢
	proveit.logic.booleans.true_axiom
7	axiom		⊢
	proveit.logic.equality.not_equals_def
8	instantiation	11, 12	, ,  ⊢
	:
9	axiom		⊢
	proveit.logic.sets.functions.images.set_image_def
10	instantiation	133, 13	⊢
	: , :
11	axiom		⊢
	proveit.logic.booleans.eq_true_intro
12	instantiation	14, 15	, ,  ⊢
	: , :
13	axiom		⊢
	proveit.physics.quantum.QPE._sample_space_def
14	theorem		⊢
	proveit.logic.equality.unfold_not_equals
15	modus ponens	16, 17	, ,  ⊢
16	instantiation	18, 69, 136, 19, 20, 21, 22, 23, 24, 25	⊢
	: , : , : , :
17	instantiation	26, 69, 27, 28, 29	, ,  ⊢
	: , : , :
18	conjecture		⊢
	proveit.physics.quantum.circuits.qcircuit_neq
19	instantiation	117, 30, 32, 33	⊢
	: , : , : , :
20	instantiation	117, 31, 32, 33	⊢
	: , : , : , :
21	instantiation	117, 34, 77, 37	⊢
	: , : , : , :
22	instantiation	117, 35, 77, 37	⊢
	: , : , : , :
23	instantiation	117, 36, 77, 37	⊢
	: , : , : , :
24	instantiation	117, 75, 77, 37	⊢
	: , : , : , :
25	instantiation	117, 76, 77, 37	⊢
	: , : , : , :
26	conjecture		⊢
	proveit.core_expr_types.expr_arrays.varray_neq_via_any_elem_neq
27	instantiation	179	⊢
	: , : , : , :
28	instantiation	179	⊢
	: , : , : , :
29	instantiation	38, 127, 200, 39, 201, 40, 41, 42, 43, 44	, ,  ⊢
	: , : , : , : , :
30	instantiation	89, 46, 45, 48, 49, 92, 93, 57, 50*	⊢
	: , : , : , :
31	instantiation	89, 46, 47, 48, 49, 92, 93, 57, 50*	⊢
	: , : , : , :
32	instantiation	133, 51	⊢
	: , :
33	instantiation	133, 52	⊢
	: , :
34	instantiation	89, 90, 53, 159, 148, 92, 93, 108*, 151*	⊢
	: , : , : , :
35	instantiation	89, 90, 54, 55, 56, 92, 57, 108*, 84*	⊢
	: , : , : , :
36	instantiation	89, 90, 58, 159, 148, 92, 93, 108*, 151*	⊢
	: , : , : , :
37	instantiation	133, 59	⊢
	: , :
38	conjecture		⊢
	proveit.logic.booleans.disjunction.or_if_any
39	instantiation	153	⊢
	: , : , :
40	instantiation	207	⊢
	: , :
41	instantiation	207	⊢
	: , :
42	instantiation	207	⊢
	: , :
43	instantiation	207	⊢
	: , :
44	instantiation	60, 61, 62, 63, 64, 65	, ,  ⊢
	: , : , :
45	instantiation	97	⊢
	: , : , : , : , : , : , : , :
46	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat8
47	instantiation	97	⊢
	: , : , : , : , : , : , : , :
48	instantiation	97	⊢
	: , : , : , : , : , : , : , :
49	instantiation	97	⊢
	: , : , : , : , : , : , : , :
50	instantiation	220, 66, 67	⊢
	: , : , :
51	instantiation	156, 257, 255, 200, 148, 201, 132, 193, 181	⊢
	: , : , : , : , : , :
52	instantiation	68, 69, 70, 111	⊢
	: , : , :
53	instantiation	216	⊢
	: , :
54	instantiation	216	⊢
	: , :
55	instantiation	216	⊢
	: , :
56	instantiation	216	⊢
	: , :
57	instantiation	109, 163, 84	⊢
	: , : , :
58	instantiation	216	⊢
	: , :
59	instantiation	110, 111	⊢
	: , :
60	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_neq_via_any_elem_neq
61	instantiation	224, 71, 72	⊢
	: , :
62	instantiation	220, 73, 74	⊢
	: , : , :
63	instantiation	117, 75, 77, 78	⊢
	: , : , : , :
64	instantiation	117, 76, 77, 78	⊢
	: , : , : , :
65	instantiation	95, 167, 163, 200, 142, 139, 201, 79	, ,  ⊢
	: , : , : , : , : , :
66	instantiation	80, 81, 82, 83, 108, 151, 84	⊢
	: , : , : , :
67	instantiation	117, 85, 86, 87	⊢
	: , : , : , :
68	conjecture		⊢
	proveit.core_expr_types.tuples.len_of_ranges_with_repeated_indices_from_1
69	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat4
70	instantiation	166, 215	⊢
	: , :
71	instantiation	109, 260, 108	⊢
	: , : , :
72	instantiation	109, 223, 151	⊢
	: , : , :
73	instantiation	239, 108	⊢
	: , : , :
74	instantiation	239, 151	⊢
	: , : , :
75	instantiation	89, 90, 88, 159, 148, 92, 93, 108*, 151*	⊢
	: , : , : , :
76	instantiation	89, 90, 91, 159, 148, 92, 93, 108*, 151*	⊢
	: , : , : , :
77	instantiation	195	⊢
	:
78	instantiation	133, 94	⊢
	: , :
79	instantiation	95, 200, 167, 257, 201, 142, 96	, ,  ⊢
	: , : , : , : , : , :
80	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
81	conjecture		⊢
	proveit.numbers.numerals.decimals.nat8
82	instantiation	97	⊢
	: , : , : , : , : , : , : , :
83	instantiation	97	⊢
	: , : , : , : , : , : , : , :
84	instantiation	220, 98, 99	⊢
	: , : , :
85	instantiation	117, 100, 101, 102	⊢
	: , : , : , :
86	instantiation	199, 200, 215, 201, 103, 105, 193, 181, 104*	⊢
	: , : , : , : , : , :
87	instantiation	199, 257, 215, 200, 105, 201, 106, 181, 107*	⊢
	: , : , : , : , : , :
88	instantiation	216	⊢
	: , :
89	conjecture		⊢
	proveit.core_expr_types.tuples.general_len
90	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
91	instantiation	216	⊢
	: , :
92	instantiation	109, 167, 108	⊢
	: , : , :
93	instantiation	109, 163, 151	⊢
	: , : , :
94	instantiation	110, 111	⊢
	: , :
95	conjecture		⊢
	proveit.logic.booleans.disjunction.disassociate
96	instantiation	112, 113, 114, 115	, ,  ⊢
	: , :
97	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_8_typical_eq
98	instantiation	239, 116	⊢
	: , : , :
99	instantiation	117, 118, 119, 120	⊢
	: , : , : , :
100	instantiation	126, 257, 121, 122, 193, 181	⊢
	: , : , : , : , : , : , :
101	instantiation	126, 255, 127, 123, 124, 125, 193, 181	⊢
	: , : , : , : , : , : , :
102	instantiation	126, 127, 257, 128, 129, 193, 181	⊢
	: , : , : , : , : , : , :
103	instantiation	179	⊢
	: , : , : , :
104	instantiation	133, 130, 135*	⊢
	: , :
105	instantiation	179	⊢
	: , : , : , :
106	instantiation	131, 132, 193	⊢
	: , :
107	instantiation	133, 134, 135*	⊢
	: , :
108	instantiation	176, 204, 193, 177	⊢
	: , : , :
109	theorem		⊢
	proveit.logic.equality.sub_left_side_into
110	conjecture		⊢
	proveit.core_expr_types.tuples.range_from1_len
111	instantiation	258, 188, 136	⊢
	: , : , :
112	conjecture		⊢
	proveit.logic.booleans.disjunction.or_if_left
113	instantiation	138, 260, 142, 137	⊢
	: , :
114	instantiation	138, 223, 139, 140	⊢
	: , :
115	instantiation	141, 260, 142, 143	, ,  ⊢
	: , :
116	instantiation	144, 193, 204	⊢
	: , :
117	conjecture		⊢
	proveit.logic.equality.four_chain_transitivity
118	instantiation	147, 200, 255, 201, 148, 145, 193, 181, 146, 204	⊢
	: , : , : , : , : , :
119	instantiation	147, 255, 257, 148, 149, 193, 181, 171, 174, 204	⊢
	: , : , : , : , : , :
120	instantiation	220, 150, 151	⊢
	: , : , :
121	conjecture		⊢
	proveit.numbers.numerals.decimals.nat5
122	instantiation	152	⊢
	: , : , : , : , :
123	instantiation	216	⊢
	: , :
124	instantiation	216	⊢
	: , :
125	instantiation	153	⊢
	: , : , :
126	conjecture		⊢
	proveit.numbers.addition.leftward_commutation
127	conjecture		⊢
	proveit.numbers.numerals.decimals.nat3
128	instantiation	153	⊢
	: , : , :
129	instantiation	153	⊢
	: , : , :
130	instantiation	156, 200, 215, 257, 201, 157, 204, 193, 154*	⊢
	: , : , : , : , : , :
131	conjecture		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
132	instantiation	258, 218, 155	⊢
	: , : , :
133	theorem		⊢
	proveit.logic.equality.equals_reversal
134	instantiation	156, 200, 215, 257, 201, 157, 204, 181, 158*	⊢
	: , : , : , : , : , :
135	instantiation	199, 200, 255, 201, 159, 204, 160*	⊢
	: , : , : , : , : , :
136	instantiation	224, 260, 223	⊢
	: , :
137	modus ponens	161, 162	⊢
138	conjecture		⊢
	proveit.logic.booleans.disjunction.closure
139	instantiation	166, 163	⊢
	: , :
140	modus ponens	164, 165	⊢
141	conjecture		⊢
	proveit.logic.booleans.disjunction.any_if_all
142	instantiation	166, 167	⊢
	: , :
143	modus ponens	168, 169	, ,  ⊢
144	conjecture		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
145	instantiation	216	⊢
	: , :
146	instantiation	170, 171, 174	⊢
	: , :
147	conjecture		⊢
	proveit.numbers.addition.disassociation
148	instantiation	216	⊢
	: , :
149	instantiation	216	⊢
	: , :
150	instantiation	172, 200, 257, 255, 201, 173, 193, 181, 174, 204, 175	⊢
	: , : , : , : , : , : , : , :
151	instantiation	176, 204, 181, 177	⊢
	: , : , :
152	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
153	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
154	instantiation	180, 193	⊢
	:
155	instantiation	258, 237, 178	⊢
	: , : , :
156	conjecture		⊢
	proveit.numbers.multiplication.distribute_through_sum
157	instantiation	179	⊢
	: , : , : , :
158	instantiation	180, 181	⊢
	:
159	instantiation	216	⊢
	: , :
160	instantiation	220, 182, 183	⊢
	: , : , :
161	instantiation	189, 252, 253, 190	⊢
	: , : , : , :
162	generalization	184	⊢
163	instantiation	258, 188, 223	⊢
	: , : , :
164	instantiation	189, 252, 185, 186	⊢
	: , : , : , :
165	generalization	187	⊢
166	conjecture		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
167	instantiation	258, 188, 260	⊢
	: , : , :
168	instantiation	189, 252, 253, 190	⊢
	: , : , : , :
169	generalization	191	, ,  ⊢
170	conjecture		⊢
	proveit.numbers.addition.add_complex_closure_bin
171	instantiation	192, 193	⊢
	:
172	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
173	instantiation	216	⊢
	: , :
174	instantiation	258, 218, 194	⊢
	: , : , :
175	instantiation	195	⊢
	:
176	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
177	instantiation	195	⊢
	:
178	instantiation	258, 249, 196	⊢
	: , : , :
179	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
180	conjecture		⊢
	proveit.numbers.multiplication.elim_one_left
181	instantiation	258, 218, 197	⊢
	: , : , :
182	instantiation	239, 198	⊢
	: , : , :
183	instantiation	199, 200, 255, 257, 201, 202, 203, 204, 205*	⊢
	: , : , : , : , : , :
184	instantiation	207	⊢
	: , :
185	instantiation	258, 259, 223	⊢
	: , : , :
186	instantiation	208, 206	⊢
	:
187	instantiation	207	⊢
	: , :
188	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
189	conjecture		⊢
	proveit.logic.booleans.conjunction.conjunction_from_quantification
190	instantiation	208, 209	⊢
	:
191	instantiation	210, 211, 212	, , ,  ⊢
	: , : , : , :
192	conjecture		⊢
	proveit.numbers.negation.complex_closure
193	instantiation	258, 218, 213	⊢
	: , : , :
194	instantiation	258, 237, 214	⊢
	: , : , :
195	axiom		⊢
	proveit.logic.equality.equals_reflexivity
196	instantiation	258, 256, 215	⊢
	: , : , :
197	instantiation	233, 234, 223	⊢
	: , : , :
198	conjecture		⊢
	proveit.numbers.numerals.decimals.add_1_1
199	conjecture		⊢
	proveit.numbers.addition.association
200	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
201	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
202	instantiation	216	⊢
	: , :
203	instantiation	258, 218, 217	⊢
	: , : , :
204	instantiation	258, 218, 219	⊢
	: , : , :
205	instantiation	220, 221, 222	⊢
	: , : , :
206	instantiation	224, 223, 225	⊢
	: , :
207	conjecture		⊢
	proveit.logic.equality.not_equals_is_bool
208	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
209	instantiation	224, 260, 225	⊢
	: , :
210	conjecture		⊢
	proveit.physics.quantum.circuits.qcircuit_output_part_neq
211	instantiation	226, 227, 228	⊢
	:
212	instantiation	229, 260, 230, 231, 232	, ,  ⊢
	: , : , :
213	instantiation	233, 234, 260	⊢
	: , : , :
214	instantiation	258, 249, 235	⊢
	: , : , :
215	conjecture		⊢
	proveit.numbers.numerals.decimals.nat4
216	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
217	instantiation	258, 237, 236	⊢
	: , : , :
218	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
219	instantiation	258, 237, 238	⊢
	: , : , :
220	axiom		⊢
	proveit.logic.equality.equals_transitivity
221	instantiation	239, 240	⊢
	: , : , :
222	conjecture		⊢
	proveit.numbers.numerals.decimals.add_3_1
223	axiom		⊢
	proveit.physics.quantum.QPE._s_in_nat_pos
224	conjecture		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
225	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
226	conjecture		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
227	instantiation	258, 241, 254	⊢
	: , : , :
228	instantiation	242, 243, 244	⊢
	: , : , :
229	conjecture		⊢
	proveit.physics.quantum.algebra.num_ket_neq
230	assumption		⊢
231	assumption		⊢
232	assumption		⊢
233	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
234	instantiation	245, 246	⊢
	: , :
235	instantiation	247, 252	⊢
	:
236	instantiation	258, 249, 248	⊢
	: , : , :
237	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
238	instantiation	258, 249, 252	⊢
	: , : , :
239	axiom		⊢
	proveit.logic.equality.substitution
240	conjecture		⊢
	proveit.numbers.numerals.decimals.add_2_1
241	instantiation	250, 252, 253	⊢
	: , :
242	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
243	conjecture		⊢
	proveit.numbers.numerals.decimals.less_0_1
244	instantiation	251, 252, 253, 254	⊢
	: , : , :
245	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
246	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
247	conjecture		⊢
	proveit.numbers.negation.int_closure
248	instantiation	258, 256, 255	⊢
	: , : , :
249	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
250	conjecture		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
251	conjecture		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
252	instantiation	258, 256, 257	⊢
	: , : , :
253	instantiation	258, 259, 260	⊢
	: , : , :
254	assumption		⊢
255	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2
256	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
257	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
258	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
259	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
260	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
*equality replacement requirements