Mathematics · proofs · software

Quantum and Circuits · Lean source

Audit.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

circuits_fresh_20261026/fresh_source/Audit.lean248 lines

Original source pathverification/circuits_fresh_20261026/fresh_source/Audit.lean

Skip source text

1 import CircuitObstructions
2 set_option pp.universes false
3 set_option pp.proofs false
4 #check CircuitObstructions.restores_append
5 #print axioms CircuitObstructions.restores_append
6 #check CircuitObstructions.canonical_target_not
7 #print axioms CircuitObstructions.canonical_target_not
8 #check CircuitObstructions.canonical_input_to_target
9 #print axioms CircuitObstructions.canonical_input_to_target
10 #check CircuitObstructions.affine_restored_exists
11 #print axioms CircuitObstructions.affine_restored_exists
12 #check CircuitObstructions.betaStar_exists
13 #print axioms CircuitObstructions.betaStar_exists
14 #check CircuitObstructions.betaStar_spec
15 #print axioms CircuitObstructions.betaStar_spec
16 #check CircuitObstructions.betaStar_le_of_bound
17 #print axioms CircuitObstructions.betaStar_le_of_bound
18 #check CircuitObstructions.betaStar_le_inputs
19 #print axioms CircuitObstructions.betaStar_le_inputs
20 #check CircuitObstructions.beta_le_betaStar
21 #print axioms CircuitObstructions.beta_le_betaStar
22 #check CircuitObstructions.betaStar_le_half_toffoliCount
23 #print axioms CircuitObstructions.betaStar_le_half_toffoliCount
24 #check CircuitObstructions.betaStar_restoration_bound
25 #print axioms CircuitObstructions.betaStar_restoration_bound
26 #check CircuitObstructions.toffoliCount_ge_two_betaStar_sub_three
27 #print axioms CircuitObstructions.toffoliCount_ge_two_betaStar_sub_three
28 #check CircuitObstructions.canonical_restored_output_degree
29 #print axioms CircuitObstructions.canonical_restored_output_degree
30 #check CircuitObstructions.restored_degree_and_cover_bound
31 #print axioms CircuitObstructions.restored_degree_and_cover_bound
32 #check CircuitObstructions.Boundary.target_separated
33 #print axioms CircuitObstructions.Boundary.target_separated
34 #check CircuitObstructions.canonical_input
35 #print axioms CircuitObstructions.canonical_input
36 #check CircuitObstructions.canonical_ancilla
37 #print axioms CircuitObstructions.canonical_ancilla
38 #check CircuitObstructions.canonical_target
39 #print axioms CircuitObstructions.canonical_target
40 #check CircuitObstructions.inverse_suffix_boundary
41 #print axioms CircuitObstructions.inverse_suffix_boundary
42 #check CircuitObstructions.direction_nonzero
43 #print axioms CircuitObstructions.direction_nonzero
44 #check CircuitObstructions.cut_transport_identity
45 #print axioms CircuitObstructions.cut_transport_identity
46 #check CircuitObstructions.cut_packet_safe
47 #print axioms CircuitObstructions.cut_packet_safe
48 #check CircuitObstructions.cut_cover_complete
49 #print axioms CircuitObstructions.cut_cover_complete
50 #check CircuitObstructions.complete_safe_cover
51 #print axioms CircuitObstructions.complete_safe_cover
52 #check CircuitObstructions.cut_states_equal_iff_reject
53 #print axioms CircuitObstructions.cut_states_equal_iff_reject
54 #check CircuitObstructions.every_index_cut
55 #print axioms CircuitObstructions.every_index_cut
56 #check CircuitObstructions.canonical_complete_safe_cover
57 #print axioms CircuitObstructions.canonical_complete_safe_cover
58 #check CircuitObstructions.bprod_nil
59 #print axioms CircuitObstructions.bprod_nil
60 #check CircuitObstructions.bprod_cons
61 #print axioms CircuitObstructions.bprod_cons
62 #check CircuitObstructions.bprod_append
63 #print axioms CircuitObstructions.bprod_append
64 #check CircuitObstructions.xor_and_right
65 #print axioms CircuitObstructions.xor_and_right
66 #check CircuitObstructions.and_xor_right
67 #print axioms CircuitObstructions.and_xor_right
68 #check CircuitObstructions.not_as_xor_one
69 #print axioms CircuitObstructions.not_as_xor_one
70 #check CircuitObstructions.DegreeLE.mono
71 #print axioms CircuitObstructions.DegreeLE.mono
72 #check CircuitObstructions.DegreeLE.one
73 #print axioms CircuitObstructions.DegreeLE.one
74 #check CircuitObstructions.DegreeLE.constant
75 #print axioms CircuitObstructions.DegreeLE.constant
76 #check CircuitObstructions.DegreeLE.variable
77 #print axioms CircuitObstructions.DegreeLE.variable
78 #check CircuitObstructions.DegreeLE.xor
79 #print axioms CircuitObstructions.DegreeLE.xor
80 #check CircuitObstructions.DegreeLE.not
81 #print axioms CircuitObstructions.DegreeLE.not
82 #check CircuitObstructions.DegreeLE.monomial_mul
83 #print axioms CircuitObstructions.DegreeLE.monomial_mul
84 #check CircuitObstructions.DegreeLE.mul
85 #print axioms CircuitObstructions.DegreeLE.mul
86 #check CircuitObstructions.DegreeLE.product
87 #print axioms CircuitObstructions.DegreeLE.product
88 #check CircuitObstructions.polyEval_append
89 #print axioms CircuitObstructions.polyEval_append
90 #check CircuitObstructions.DegreeLE.polynomial_witness
91 #print axioms CircuitObstructions.DegreeLE.polynomial_witness
92 #check CircuitObstructions.polynomial_degree_certificate
93 #print axioms CircuitObstructions.polynomial_degree_certificate
94 #check CircuitObstructions.degreeLE_iff_polynomial
95 #print axioms CircuitObstructions.degreeLE_iff_polynomial
96 #check CircuitObstructions.squareParity_add
97 #print axioms CircuitObstructions.squareParity_add
98 #check CircuitObstructions.affine_squareParity_zero
99 #print axioms CircuitObstructions.affine_squareParity_zero
100 #check CircuitObstructions.andTwo_degree_two
101 #print axioms CircuitObstructions.andTwo_degree_two
102 #check CircuitObstructions.andTwo_not_affine
103 #print axioms CircuitObstructions.andTwo_not_affine
104 #check CircuitObstructions.andTwo_no_degree_one_safe_cover
105 #print axioms CircuitObstructions.andTwo_no_degree_one_safe_cover
106 #check CircuitObstructions.beta_andTwo
107 #print axioms CircuitObstructions.beta_andTwo
108 #check CircuitObstructions.betaStar_andTwo
109 #print axioms CircuitObstructions.betaStar_andTwo
110 #check CircuitObstructions.restored_andTwo_needs_toffoli
111 #print axioms CircuitObstructions.restored_andTwo_needs_toffoli
112 #check CircuitObstructions.Examples.andOracle_restores
113 #print axioms CircuitObstructions.Examples.andOracle_restores
114 #check CircuitObstructions.Examples.andOracle_toffoli_count
115 #print axioms CircuitObstructions.Examples.andOracle_toffoli_count
116 #check CircuitObstructions.Examples.and_scratch_can_be_dirty
117 #print axioms CircuitObstructions.Examples.and_scratch_can_be_dirty
118 #check CircuitObstructions.Examples.andOracle_every_cut
119 #print axioms CircuitObstructions.Examples.andOracle_every_cut
120 #check CircuitObstructions.Examples.outputActiveOracle_restores
121 #print axioms CircuitObstructions.Examples.outputActiveOracle_restores
122 #check CircuitObstructions.Examples.outputActiveOracle_length
123 #print axioms CircuitObstructions.Examples.outputActiveOracle_length
124 #check CircuitObstructions.Examples.outputActiveOracle_toffoli_count
125 #print axioms CircuitObstructions.Examples.outputActiveOracle_toffoli_count
126 #check CircuitObstructions.Examples.moved_discrepancy_data
127 #print axioms CircuitObstructions.Examples.moved_discrepancy_data
128 #check CircuitObstructions.Examples.moved_discrepancy_target
129 #print axioms CircuitObstructions.Examples.moved_discrepancy_target
130 #check CircuitObstructions.Examples.target_only_reconstruction_is_false
131 #print axioms CircuitObstructions.Examples.target_only_reconstruction_is_false
132 #check CircuitObstructions.Examples.degenerate_encoding_control
133 #print axioms CircuitObstructions.Examples.degenerate_encoding_control
134 #check CircuitObstructions.write_same
135 #print axioms CircuitObstructions.write_same
136 #check CircuitObstructions.write_other
137 #print axioms CircuitObstructions.write_other
138 #check CircuitObstructions.xor_cancel_right
139 #print axioms CircuitObstructions.xor_cancel_right
140 #check CircuitObstructions.xor_cancel_left
141 #print axioms CircuitObstructions.xor_cancel_left
142 #check CircuitObstructions.xor_commute
143 #print axioms CircuitObstructions.xor_commute
144 #check CircuitObstructions.xor_true_iff_ne
145 #print axioms CircuitObstructions.xor_true_iff_ne
146 #check CircuitObstructions.Gate.eval_involutive
147 #print axioms CircuitObstructions.Gate.eval_involutive
148 #check CircuitObstructions.Gate.eval_injective
149 #print axioms CircuitObstructions.Gate.eval_injective
150 #check CircuitObstructions.run_nil
151 #print axioms CircuitObstructions.run_nil
152 #check CircuitObstructions.run_cons
153 #print axioms CircuitObstructions.run_cons
154 #check CircuitObstructions.run_append
155 #print axioms CircuitObstructions.run_append
156 #check CircuitObstructions.run_reverse_run
157 #print axioms CircuitObstructions.run_reverse_run
158 #check CircuitObstructions.run_run_reverse
159 #print axioms CircuitObstructions.run_run_reverse
160 #check CircuitObstructions.run_injective
161 #print axioms CircuitObstructions.run_injective
162 #check CircuitObstructions.toffoliCount_append
163 #print axioms CircuitObstructions.toffoliCount_append
164 #check CircuitObstructions.toffoliCount_reverse
165 #print axioms CircuitObstructions.toffoliCount_reverse
166 #check CircuitObstructions.withoutWire_length_le
167 #print axioms CircuitObstructions.withoutWire_length_le
168 #check CircuitObstructions.withoutWire_length_lt
169 #print axioms CircuitObstructions.withoutWire_length_lt
170 #check CircuitObstructions.bprod_write
171 #print axioms CircuitObstructions.bprod_write
172 #check CircuitObstructions.bprod_write_absent
173 #print axioms CircuitObstructions.bprod_write_absent
174 #check CircuitObstructions.workspaceDegree_initial
175 #print axioms CircuitObstructions.workspaceDegree_initial
176 #check CircuitObstructions.workspaceDegree_toggle
177 #print axioms CircuitObstructions.workspaceDegree_toggle
178 #check CircuitObstructions.workspaceDegree_gate
179 #print axioms CircuitObstructions.workspaceDegree_gate
180 #check CircuitObstructions.workspaceDegree_run
181 #print axioms CircuitObstructions.workspaceDegree_run
182 #check CircuitObstructions.run_coordinate_degree
183 #print axioms CircuitObstructions.run_coordinate_degree
184 #check CircuitObstructions.canonical_boundary_degree
185 #print axioms CircuitObstructions.canonical_boundary_degree
186 #check CircuitObstructions.canonical_run_coordinate_degree
187 #print axioms CircuitObstructions.canonical_run_coordinate_degree
188 #check CircuitObstructions.canonical_cut_packet_degree
189 #print axioms CircuitObstructions.canonical_cut_packet_degree
190 #check CircuitObstructions.CompleteSafeDegreeLE.mono
191 #print axioms CircuitObstructions.CompleteSafeDegreeLE.mono
192 #check CircuitObstructions.bprod_true_iff
193 #print axioms CircuitObstructions.bprod_true_iff
194 #check CircuitObstructions.pointIndicator_true_iff
195 #print axioms CircuitObstructions.pointIndicator_true_iff
196 #check CircuitObstructions.pointIndicator_degree
197 #print axioms CircuitObstructions.pointIndicator_degree
198 #check CircuitObstructions.completeSafeDegree_le_inputs
199 #print axioms CircuitObstructions.completeSafeDegree_le_inputs
200 #check CircuitObstructions.exists_least_degree
201 #print axioms CircuitObstructions.exists_least_degree
202 #check CircuitObstructions.beta_exists
203 #print axioms CircuitObstructions.beta_exists
204 #check CircuitObstructions.beta_spec
205 #print axioms CircuitObstructions.beta_spec
206 #check CircuitObstructions.beta_le_of_cover
207 #print axioms CircuitObstructions.beta_le_of_cover
208 #check CircuitObstructions.beta_le_iff
209 #print axioms CircuitObstructions.beta_le_iff
210 #check CircuitObstructions.beta_le_inputs
211 #print axioms CircuitObstructions.beta_le_inputs
212 #check CircuitObstructions.beta_zero
213 #print axioms CircuitObstructions.beta_zero
214 #check CircuitObstructions.canonical_cut_completeSafeDegree
215 #print axioms CircuitObstructions.canonical_cut_completeSafeDegree
216 #check CircuitObstructions.Gate.toffoliCost_le_one
217 #print axioms CircuitObstructions.Gate.toffoliCost_le_one
218 #check CircuitObstructions.toffoliCount_nil
219 #print axioms CircuitObstructions.toffoliCount_nil
220 #check CircuitObstructions.toffoliCount_cons
221 #print axioms CircuitObstructions.toffoliCount_cons
222 #check CircuitObstructions.exists_cut_with_toffoliCount
223 #print axioms CircuitObstructions.exists_cut_with_toffoliCount
224 #check CircuitObstructions.exists_balanced_toffoli_cut
225 #print axioms CircuitObstructions.exists_balanced_toffoli_cut
226 #check CircuitObstructions.canonical_restored_completeSafeDegree
227 #print axioms CircuitObstructions.canonical_restored_completeSafeDegree
228 #check CircuitObstructions.beta_le_half_toffoliCount
229 #print axioms CircuitObstructions.beta_le_half_toffoliCount
230 #check CircuitObstructions.beta_restoration_bound
231 #print axioms CircuitObstructions.beta_restoration_bound
232 #check CircuitObstructions.toffoliCount_ge_two_beta_sub_three
233 #print axioms CircuitObstructions.toffoliCount_ge_two_beta_sub_three
234 #print CircuitObstructions.Restores
235 #print CircuitObstructions.cut_transport_identity
236 #print CircuitObstructions.complete_safe_cover
237 #print CircuitObstructions.canonical_complete_safe_cover
238 #print CircuitObstructions.every_index_cut
239 #print CircuitObstructions.DegreeLE
240 #print CircuitObstructions.WorkspaceDegree
241 #print CircuitObstructions.workspaceDegree_run
242 #print CircuitObstructions.canonical_cut_packet_degree
243 #print CircuitObstructions.CompleteSafeDegreeLE
244 #print CircuitObstructions.beta
245 #print CircuitObstructions.betaStar
246 #print CircuitObstructions.betaStar_restoration_bound
247 #print CircuitObstructions.canonical_restored_output_degree
248 #print CircuitObstructions.restored_degree_and_cover_bound

Back to source controls

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: afe063bfb148be2928dd8e5927e71bcd163dd3fb9cb3ac2eb15d111852e747ae

Original source on GitHub

Back to Quantum and Circuits