KernelAudit.lean

1 import KomorebiPaperV
2 
3 /- Checked-target audit harness. Author: Komorebi P. -/
4 
5 
6 #print axioms KomorebiPaperV.Binary.cutSum_eq_root
7 #print axioms KomorebiPaperV.Binary.value_le_cost
8 #print axioms KomorebiPaperV.Binary.best_cost
9 #print axioms KomorebiPaperV.Binary.best_is_global_minimum
10 #print axioms KomorebiPaperV.Binary.root_le_envelope
11 #print axioms KomorebiPaperV.Binary.cut_perturbation
12 #print axioms KomorebiPaperV.CRT.residue_pair_iff
13 #print axioms KomorebiPaperV.CRT.residue_mask_factorization
14 #print axioms KomorebiPaperV.CRT.dyadic_odd_coprime
15 #print axioms KomorebiPaperV.CRT.dyadic_odd_packet_factorization
16 #print axioms KomorebiPaperV.CompletePrunings.terminal_exists
17 #print axioms KomorebiPaperV.CompletePrunings.node_on_terminal
18 #print axioms KomorebiPaperV.CompletePrunings.selected_stop_iff
19 #print axioms KomorebiPaperV.CompletePrunings.selected_split_root_false
20 #print axioms KomorebiPaperV.CompletePrunings.selected_split_down_iff
21 #print axioms KomorebiPaperV.CompletePrunings.cut_complete
22 #print axioms KomorebiPaperV.CompletePrunings.ancestor_onPath
23 #print axioms KomorebiPaperV.CompletePrunings.path_nodes_comparable
24 #print axioms KomorebiPaperV.CompletePrunings.complete_iff_covering_antichain
25 #print axioms KomorebiPaperV.CompletePrunings.complete_root_unique
26 #print axioms KomorebiPaperV.CompletePrunings.complete_child
27 #print axioms KomorebiPaperV.CompletePrunings.complete_has_cut
28 #print axioms KomorebiPaperV.CompletePrunings.cut_ext
29 #print axioms KomorebiPaperV.CompletePrunings.complete_pruning_finite
30 #print axioms KomorebiPaperV.CompletePrunings.complete_pruning_minimum
31 #print axioms KomorebiPaperV.CyclicSeries.coeff_cyclicProjector
32 #print axioms KomorebiPaperV.CyclicSeries.cyclicProjector_idempotent
33 #print axioms KomorebiPaperV.CyclicSeries.cyclicProjector_orthogonal
34 #print axioms KomorebiPaperV.CyclicSeries.cyclicProjector_eq_zero_of_residue_ne
35 #print axioms KomorebiPaperV.CyclicSeries.cyclicProjector_eq_of_mod_eq
36 #print axioms KomorebiPaperV.CyclicSeries.cyclicProjector_add
37 #print axioms KomorebiPaperV.CyclicSeries.cyclicProjector_sum
38 #print axioms KomorebiPaperV.CyclicSeries.sum_cyclicProjector
39 #print axioms KomorebiPaperV.CyclicSeries.cyclicProjector_product_packet
40 #print axioms KomorebiPaperV.CyclicSeries.cyclicProjector_product_other
41 #print axioms KomorebiPaperV.CyclicSeries.cyclic_product_law
42 #print axioms KomorebiPaperV.CyclicSeries.pure_finite_product
43 #print axioms KomorebiPaperV.CyclicSeries.project_finite_product
44 #print axioms KomorebiPaperV.CyclicSeries.sum_fin_projector
45 #print axioms KomorebiPaperV.CyclicSeries.cyclic_power_law
46 #print axioms KomorebiPaperV.FIRTransfer.tapEquiv_symm
47 #print axioms KomorebiPaperV.FIRTransfer.tapIndex_equiv
48 #print axioms KomorebiPaperV.FIRTransfer.transfer_address
49 #print axioms KomorebiPaperV.FIRTransfer.fir_reindex
50 #print axioms KomorebiPaperV.FIRTransfer.sum_pair_fiber
51 #print axioms KomorebiPaperV.FIRTransfer.fir_polyphase_transfer
52 #print axioms KomorebiPaperV.FilterBank.act_apply
53 #print axioms KomorebiPaperV.FilterBank.act_is_fir
54 #print axioms KomorebiPaperV.FilterBank.act_impulse
55 #print axioms KomorebiPaperV.FilterBank.act_single
56 #print axioms KomorebiPaperV.FilterBank.evalZ_apply
57 #print axioms KomorebiPaperV.FilterBank.filter_transform
58 #print axioms KomorebiPaperV.FilterBank.bank_mul
59 #print axioms KomorebiPaperV.FilterBank.bank_impulse
60 #print axioms KomorebiPaperV.FilterBank.bank_faithful
61 #print axioms KomorebiPaperV.FilterBank.gain_delay_action
62 #print axioms KomorebiPaperV.FilterBank.perfect_reconstruction_iff
63 #print axioms KomorebiPaperV.FilterBank.bank_transform
64 #print axioms KomorebiPaperV.FilterBank.original_sample_delay
65 #print axioms KomorebiPaperV.FiniteAdaptive.cutSum_eq_root
66 #print axioms KomorebiPaperV.FiniteAdaptive.cutSum_eq_identity
67 #print axioms KomorebiPaperV.FiniteAdaptive.pathHits_one
68 #print axioms KomorebiPaperV.FiniteAdaptive.arbitrary_objective_minimum
69 #print axioms KomorebiPaperV.FiniteAdaptive.strict_minimum_positive_gap
70 #print axioms KomorebiPaperV.FiniteAdaptive.value_le_cost
71 #print axioms KomorebiPaperV.FiniteAdaptive.best_cost
72 #print axioms KomorebiPaperV.FiniteAdaptive.best_is_global_minimum
73 #print axioms KomorebiPaperV.FiniteAdaptive.best_preserves_synthesis
74 #print axioms KomorebiPaperV.FiniteAdaptive.stop_on_tie
75 #print axioms KomorebiPaperV.FiniteAdaptive.root_le_envelope
76 #print axioms KomorebiPaperV.FiniteAdaptive.cost_le_envelope
77 #print axioms KomorebiPaperV.FiniteAdaptive.envelope_attained
78 #print axioms KomorebiPaperV.FiniteAdaptive.cut_perturbation
79 #print axioms KomorebiPaperV.FiniteAdaptive.value_perturbation
80 #print axioms KomorebiPaperV.FiniteAdaptive.best_unchanged_of_gap
81 #print axioms KomorebiPaperV.FiniteAdaptive.one_comparison_per_internal_node
82 #print axioms KomorebiPaperV.FiniteAdaptive.selector_probability
83 #print axioms KomorebiPaperV.finite_minimum
84 #print axioms KomorebiPaperV.positive_gap
85 #print axioms KomorebiPaperV.gap_stability
86 #print axioms KomorebiPaperV.singleton_minimum
87 #print axioms KomorebiPaperV.singleton_selection_unchanged
88 #print axioms KomorebiPaperV.FiniteTransforms.unpair_pair
89 #print axioms KomorebiPaperV.FiniteTransforms.pair_unpair
90 #print axioms KomorebiPaperV.FiniteTransforms.flat_synthesis_analysis
91 #print axioms KomorebiPaperV.FiniteTransforms.flat_analysis_synthesis
92 #print axioms KomorebiPaperV.FiniteTransforms.unlift_lift_flat
93 #print axioms KomorebiPaperV.FiniteTransforms.lift_unlift_flat
94 #print axioms KomorebiPaperV.FiniteTransforms.haar_involution
95 #print axioms KomorebiPaperV.FiniteTransforms.haar_pair_energy
96 #print axioms KomorebiPaperV.FiniteTransforms.haar_finite_energy
97 #print axioms KomorebiPaperV.FiniteTransforms.haar_flat_involution
98 #print axioms KomorebiPaperV.FiniteTransforms.matrix_eq_of_all_vectors
99 #print axioms KomorebiPaperV.FiniteTransforms.perfect_reconstruction_matrix_iff
100 #print axioms KomorebiPaperV.HaarChannels.norm_sq_tsum
101 #print axioms KomorebiPaperV.HaarChannels.channel_energy
102 #print axioms KomorebiPaperV.HaarChannels.even_apply
103 #print axioms KomorebiPaperV.HaarChannels.odd_apply
104 #print axioms KomorebiPaperV.HaarChannels.interleaved_energy
105 #print axioms KomorebiPaperV.HaarChannels.haar_energy
106 #print axioms KomorebiPaperV.HaarChannels.haar_low_samples
107 #print axioms KomorebiPaperV.HaarChannels.haar_high_samples
108 #print axioms KomorebiPaperV.HaarHilbert.inverse_low
109 #print axioms KomorebiPaperV.HaarHilbert.inverse_high
110 #print axioms KomorebiPaperV.HaarHilbert.energy
111 #print axioms KomorebiPaperV.HaarHilbert.low_apply
112 #print axioms KomorebiPaperV.HaarHilbert.high_apply
113 #print axioms KomorebiPaperV.HilbertPackets.projection_apply
114 #print axioms KomorebiPaperV.HilbertPackets.projection_norm_le
115 #print axioms KomorebiPaperV.HilbertPackets.projector_apply
116 #print axioms KomorebiPaperV.HilbertPackets.projector_idempotent
117 #print axioms KomorebiPaperV.HilbertPackets.projector_annihilate
118 #print axioms KomorebiPaperV.HilbertPackets.projector_complete
119 #print axioms KomorebiPaperV.HilbertPackets.projector_refinement
120 #print axioms KomorebiPaperV.HilbertPackets.reindex_norm
121 #print axioms KomorebiPaperV.HilbertPackets.polyphase_apply
122 #print axioms KomorebiPaperV.HilbertPackets.polyphase_synthesis_analysis
123 #print axioms KomorebiPaperV.HilbertPackets.polyphase_analysis_synthesis
124 #print axioms KomorebiPaperV.HilbertPackets.polyphase_energy
125 #print axioms KomorebiPaperV.HilbertPackets.impulse_expansion
126 #print axioms KomorebiPaperV.HilbertPackets.projector_symmetric
127 #print axioms KomorebiPaperV.HilbertPackets.projector_orthogonal
128 #print axioms KomorebiPaperV.HilbertPackets.impulse_basis_apply
129 #print axioms KomorebiPaperV.HilbertPackets.impulse_dense_span
130 #print axioms KomorebiPaperV.HilbertPackets.shift_apply
131 #print axioms KomorebiPaperV.HilbertPackets.reindex_single
132 #print axioms KomorebiPaperV.HilbertPackets.shift_impulse
133 #print axioms KomorebiPaperV.HilbertPackets.residue_projector_refinement
134 #print axioms KomorebiPaperV.HilbertPackets.shift_generated_dense_span
135 #print axioms KomorebiPaperV.HilbertPackets.finite_impulse_expansion
136 #print axioms KomorebiPaperV.IntegerPolyphase.phase_val
137 #print axioms KomorebiPaperV.IntegerPolyphase.address_phase_quotient
138 #print axioms KomorebiPaperV.IntegerPolyphase.address_divmod
139 #print axioms KomorebiPaperV.IntegerPolyphase.phase_address
140 #print axioms KomorebiPaperV.IntegerPolyphase.quotient_address
141 #print axioms KomorebiPaperV.IntegerPolyphase.synthesis_analysis
142 #print axioms KomorebiPaperV.IntegerPolyphase.analysis_synthesis
143 #print axioms KomorebiPaperV.IntegerPolyphase.channel_delay
144 #print axioms KomorebiPaperV.IntegerPolyphase.sample_delay
145 #print axioms KomorebiPaperV.IntegerPolyphase.emod_coarsen
146 #print axioms KomorebiPaperV.IntegerPolyphase.residue_refinement
147 #print axioms KomorebiPaperV.known_edge_error
148 #print axioms KomorebiPaperV.estimated_edge_error
149 #print axioms KomorebiPaperV.several_known_edges_error
150 #print axioms KomorebiPaperV.known_edge_norm
151 #print axioms KomorebiPaperV.several_known_edges_norm
152 #print axioms KomorebiPaperV.estimated_edge_norm_bound
153 #print axioms KomorebiPaperV.lifting_synthesis_analysis
154 #print axioms KomorebiPaperV.lifting_analysis_synthesis
155 #print axioms KomorebiPaperV.lifting_determinant
156 #print axioms KomorebiPaperV.lifting_coordinates_roundtrip
157 #print axioms KomorebiPaperV.MaskPerturbation.jump_measurable
158 #print axioms KomorebiPaperV.MaskPerturbation.symmetric_difference_norm
159 #print axioms KomorebiPaperV.MaskPerturbation.indicator_difference_norm
160 #print axioms KomorebiPaperV.MaskPerturbation.jump_sub_same_set
161 #print axioms KomorebiPaperV.MaskPerturbation.jump_error_decomposition
162 #print axioms KomorebiPaperV.MaskPerturbation.finite_p_perturbation
163 #print axioms KomorebiPaperV.MaskPerturbation.pointwise_sup_bound
164 #print axioms KomorebiPaperV.MaskPerturbation.infinity_perturbation
165 #print axioms KomorebiPaperV.MaskPerturbation.full_signal_perturbation
166 #print axioms KomorebiPaperV.packet_idempotent
167 #print axioms KomorebiPaperV.packet_annihilate
168 #print axioms KomorebiPaperV.packet_complete
169 #print axioms KomorebiPaperV.packet_refinement
170 #print axioms KomorebiPaperV.address_synthesize_analyze
171 #print axioms KomorebiPaperV.address_analyze_synthesize
172 #print axioms KomorebiPaperV.residuePacket_idempotent
173 #print axioms KomorebiPaperV.residuePacket_complete
174 #print axioms KomorebiPaperV.PruningAlgorithm.solve_correct
175 #print axioms KomorebiPaperV.PruningAlgorithm.solve_comparisons
176 #print axioms KomorebiPaperV.PruningAlgorithm.solve_visits
177 #print axioms KomorebiPaperV.PruningAlgorithm.solve_additions
178 #print axioms KomorebiPaperV.PruningAlgorithm.internal_le_nodes
179 #print axioms KomorebiPaperV.PruningAlgorithm.solve_linear_work
180 #print axioms KomorebiPaperV.PruningAlgorithm.computed_antichain_optimal
181 #print axioms KomorebiPaperV.PruningAlgorithm.antichain_probability
182 #print axioms KomorebiPaperV.PruningSums.node_sum_branch
183 #print axioms KomorebiPaperV.PruningSums.mem_selectedNodes
184 #print axioms KomorebiPaperV.PruningSums.cutSum_eq_nodeSum
185 #print axioms KomorebiPaperV.PruningSums.pruning_nodeSum
186 #print axioms KomorebiPaperV.PruningSums.antichain_synthesis
187 #print axioms KomorebiPaperV.PruningSums.packet_projector_synthesis
188 #print axioms KomorebiPaperV.PruningSums.selected_global_minimum
189 #print axioms KomorebiPaperV.PruningSums.antichain_perturbation
190 #print axioms KomorebiPaperV.PruningSums.antichain_envelope_attained
191 #print axioms KomorebiPaperV.PruningSums.antichain_selector_stable
192 #print axioms KomorebiPaperV.PruningSums.objective_minimum
193 #print axioms KomorebiPaperV.PruningSums.objective_positive_gap
194 #print axioms KomorebiPaperV.PruningSums.objective_stability
195 #print axioms KomorebiPaperV.PruningSums.singleton_selector
196 #print axioms KomorebiPaperV.PruningSums.objective_gap_attained
197 #print axioms KomorebiPaperV.SmithAction.action_mul
198 #print axioms KomorebiPaperV.SmithAction.action_one
199 #print axioms KomorebiPaperV.SmithAction.action_scale
200 #print axioms KomorebiPaperV.SmithAction.action_nonzero
201 #print axioms KomorebiPaperV.SmithAction.half_turn
202 #print axioms KomorebiPaperV.SmithAction.half_turn_zero
203 #print axioms KomorebiPaperV.SmithAction.half_turn_infinity
204 #print axioms KomorebiPaperV.SmithAction.homogeneous_chart
205 #print axioms KomorebiPaperV.SmithAction.chart_composition
206 #print axioms KomorebiPaperV.SmithAction.finite_half_turn
207 #print axioms KomorebiPaperV.SmithCyclic.omega_ne_zero
208 #print axioms KomorebiPaperV.SmithCyclic.omega_pow
209 #print axioms KomorebiPaperV.SmithCyclic.omega_two
210 #print axioms KomorebiPaperV.SmithCyclic.action_respects_scaling
211 #print axioms KomorebiPaperV.SmithCyclic.projective_mul
212 #print axioms KomorebiPaperV.SmithCyclic.projective_one
213 #print axioms KomorebiPaperV.SmithCyclic.cyclic_zero
214 #print axioms KomorebiPaperV.SmithCyclic.cyclic_composition
215 #print axioms KomorebiPaperV.SmithCyclic.cayley_conjugacy
216 #print axioms KomorebiPaperV.SmithCyclic.cyclic_chart
217 #print axioms KomorebiPaperV.SmithCyclic.two_phase_swap
218 #print axioms KomorebiPaperV.SmithCyclic.two_phase_impedance_admittance
219 #print axioms KomorebiPaperV.WaveletPackets.low_norm_bound
220 #print axioms KomorebiPaperV.WaveletPackets.high_norm_bound
221 #print axioms KomorebiPaperV.WaveletPackets.child_energy
222 #print axioms KomorebiPaperV.WaveletPackets.packet_energy
223 #print axioms KomorebiPaperV.WaveletPackets.energy_implies_adjoint_identity
224 #print axioms KomorebiPaperV.WaveletPackets.packet_operator_reconstruction
225 #print axioms KomorebiPaperV.WaveletPackets.packet_reconstruction
226 #print axioms KomorebiPaperV.ZTransform.transform_unique
227 #print axioms KomorebiPaperV.ZTransform.delay_transform
228 #print axioms KomorebiPaperV.ZTransform.finite_transfer_transform
229 #print axioms KomorebiPaperV.ZTransform.fir_channel_transform
230 #print axioms KomorebiPaperV.ZTransform.fir_matrix_transform
231 
232 open Lean Meta Elab Command
233 
234 run_cmd do
235   let env ← getEnv
236   let targets : Array Name := #[
237     `KomorebiPaperV.Binary.cutSum_eq_root,
238     `KomorebiPaperV.Binary.value_le_cost,
239     `KomorebiPaperV.Binary.best_cost,
240     `KomorebiPaperV.Binary.best_is_global_minimum,
241     `KomorebiPaperV.Binary.root_le_envelope,
242     `KomorebiPaperV.Binary.cut_perturbation,
243     `KomorebiPaperV.CRT.residue_pair_iff,
244     `KomorebiPaperV.CRT.residue_mask_factorization,
245     `KomorebiPaperV.CRT.dyadic_odd_coprime,
246     `KomorebiPaperV.CRT.dyadic_odd_packet_factorization,
247     `KomorebiPaperV.CompletePrunings.terminal_exists,
248     `KomorebiPaperV.CompletePrunings.node_on_terminal,
249     `KomorebiPaperV.CompletePrunings.selected_stop_iff,
250     `KomorebiPaperV.CompletePrunings.selected_split_root_false,
251     `KomorebiPaperV.CompletePrunings.selected_split_down_iff,
252     `KomorebiPaperV.CompletePrunings.cut_complete,
253     `KomorebiPaperV.CompletePrunings.ancestor_onPath,
254     `KomorebiPaperV.CompletePrunings.path_nodes_comparable,
255     `KomorebiPaperV.CompletePrunings.complete_iff_covering_antichain,
256     `KomorebiPaperV.CompletePrunings.complete_root_unique,
257     `KomorebiPaperV.CompletePrunings.complete_child,
258     `KomorebiPaperV.CompletePrunings.complete_has_cut,
259     `KomorebiPaperV.CompletePrunings.cut_ext,
260     `KomorebiPaperV.CompletePrunings.complete_pruning_finite,
261     `KomorebiPaperV.CompletePrunings.complete_pruning_minimum,
262     `KomorebiPaperV.CyclicSeries.coeff_cyclicProjector,
263     `KomorebiPaperV.CyclicSeries.cyclicProjector_idempotent,
264     `KomorebiPaperV.CyclicSeries.cyclicProjector_orthogonal,
265     `KomorebiPaperV.CyclicSeries.cyclicProjector_eq_zero_of_residue_ne,
266     `KomorebiPaperV.CyclicSeries.cyclicProjector_eq_of_mod_eq,
267     `KomorebiPaperV.CyclicSeries.cyclicProjector_add,
268     `KomorebiPaperV.CyclicSeries.cyclicProjector_sum,
269     `KomorebiPaperV.CyclicSeries.sum_cyclicProjector,
270     `KomorebiPaperV.CyclicSeries.cyclicProjector_product_packet,
271     `KomorebiPaperV.CyclicSeries.cyclicProjector_product_other,
272     `KomorebiPaperV.CyclicSeries.cyclic_product_law,
273     `KomorebiPaperV.CyclicSeries.pure_finite_product,
274     `KomorebiPaperV.CyclicSeries.project_finite_product,
275     `KomorebiPaperV.CyclicSeries.sum_fin_projector,
276     `KomorebiPaperV.CyclicSeries.cyclic_power_law,
277     `KomorebiPaperV.FIRTransfer.tapEquiv_symm,
278     `KomorebiPaperV.FIRTransfer.tapIndex_equiv,
279     `KomorebiPaperV.FIRTransfer.transfer_address,
280     `KomorebiPaperV.FIRTransfer.fir_reindex,
281     `KomorebiPaperV.FIRTransfer.sum_pair_fiber,
282     `KomorebiPaperV.FIRTransfer.fir_polyphase_transfer,
283     `KomorebiPaperV.FilterBank.act_apply,
284     `KomorebiPaperV.FilterBank.act_is_fir,
285     `KomorebiPaperV.FilterBank.act_impulse,
286     `KomorebiPaperV.FilterBank.act_single,
287     `KomorebiPaperV.FilterBank.evalZ_apply,
288     `KomorebiPaperV.FilterBank.filter_transform,
289     `KomorebiPaperV.FilterBank.bank_mul,
290     `KomorebiPaperV.FilterBank.bank_impulse,
291     `KomorebiPaperV.FilterBank.bank_faithful,
292     `KomorebiPaperV.FilterBank.gain_delay_action,
293     `KomorebiPaperV.FilterBank.perfect_reconstruction_iff,
294     `KomorebiPaperV.FilterBank.bank_transform,
295     `KomorebiPaperV.FilterBank.original_sample_delay,
296     `KomorebiPaperV.FiniteAdaptive.cutSum_eq_root,
297     `KomorebiPaperV.FiniteAdaptive.cutSum_eq_identity,
298     `KomorebiPaperV.FiniteAdaptive.pathHits_one,
299     `KomorebiPaperV.FiniteAdaptive.arbitrary_objective_minimum,
300     `KomorebiPaperV.FiniteAdaptive.strict_minimum_positive_gap,
301     `KomorebiPaperV.FiniteAdaptive.value_le_cost,
302     `KomorebiPaperV.FiniteAdaptive.best_cost,
303     `KomorebiPaperV.FiniteAdaptive.best_is_global_minimum,
304     `KomorebiPaperV.FiniteAdaptive.best_preserves_synthesis,
305     `KomorebiPaperV.FiniteAdaptive.stop_on_tie,
306     `KomorebiPaperV.FiniteAdaptive.root_le_envelope,
307     `KomorebiPaperV.FiniteAdaptive.cost_le_envelope,
308     `KomorebiPaperV.FiniteAdaptive.envelope_attained,
309     `KomorebiPaperV.FiniteAdaptive.cut_perturbation,
310     `KomorebiPaperV.FiniteAdaptive.value_perturbation,
311     `KomorebiPaperV.FiniteAdaptive.best_unchanged_of_gap,
312     `KomorebiPaperV.FiniteAdaptive.one_comparison_per_internal_node,
313     `KomorebiPaperV.FiniteAdaptive.selector_probability,
314     `KomorebiPaperV.finite_minimum,
315     `KomorebiPaperV.positive_gap,
316     `KomorebiPaperV.gap_stability,
317     `KomorebiPaperV.singleton_minimum,
318     `KomorebiPaperV.singleton_selection_unchanged,
319     `KomorebiPaperV.FiniteTransforms.unpair_pair,
320     `KomorebiPaperV.FiniteTransforms.pair_unpair,
321     `KomorebiPaperV.FiniteTransforms.flat_synthesis_analysis,
322     `KomorebiPaperV.FiniteTransforms.flat_analysis_synthesis,
323     `KomorebiPaperV.FiniteTransforms.unlift_lift_flat,
324     `KomorebiPaperV.FiniteTransforms.lift_unlift_flat,
325     `KomorebiPaperV.FiniteTransforms.haar_involution,
326     `KomorebiPaperV.FiniteTransforms.haar_pair_energy,
327     `KomorebiPaperV.FiniteTransforms.haar_finite_energy,
328     `KomorebiPaperV.FiniteTransforms.haar_flat_involution,
329     `KomorebiPaperV.FiniteTransforms.matrix_eq_of_all_vectors,
330     `KomorebiPaperV.FiniteTransforms.perfect_reconstruction_matrix_iff,
331     `KomorebiPaperV.HaarChannels.norm_sq_tsum,
332     `KomorebiPaperV.HaarChannels.channel_energy,
333     `KomorebiPaperV.HaarChannels.even_apply,
334     `KomorebiPaperV.HaarChannels.odd_apply,
335     `KomorebiPaperV.HaarChannels.interleaved_energy,
336     `KomorebiPaperV.HaarChannels.haar_energy,
337     `KomorebiPaperV.HaarChannels.haar_low_samples,
338     `KomorebiPaperV.HaarChannels.haar_high_samples,
339     `KomorebiPaperV.HaarHilbert.inverse_low,
340     `KomorebiPaperV.HaarHilbert.inverse_high,
341     `KomorebiPaperV.HaarHilbert.energy,
342     `KomorebiPaperV.HaarHilbert.low_apply,
343     `KomorebiPaperV.HaarHilbert.high_apply,
344     `KomorebiPaperV.HilbertPackets.projection_apply,
345     `KomorebiPaperV.HilbertPackets.projection_norm_le,
346     `KomorebiPaperV.HilbertPackets.projector_apply,
347     `KomorebiPaperV.HilbertPackets.projector_idempotent,
348     `KomorebiPaperV.HilbertPackets.projector_annihilate,
349     `KomorebiPaperV.HilbertPackets.projector_complete,
350     `KomorebiPaperV.HilbertPackets.projector_refinement,
351     `KomorebiPaperV.HilbertPackets.reindex_norm,
352     `KomorebiPaperV.HilbertPackets.polyphase_apply,
353     `KomorebiPaperV.HilbertPackets.polyphase_synthesis_analysis,
354     `KomorebiPaperV.HilbertPackets.polyphase_analysis_synthesis,
355     `KomorebiPaperV.HilbertPackets.polyphase_energy,
356     `KomorebiPaperV.HilbertPackets.impulse_expansion,
357     `KomorebiPaperV.HilbertPackets.projector_symmetric,
358     `KomorebiPaperV.HilbertPackets.projector_orthogonal,
359     `KomorebiPaperV.HilbertPackets.impulse_basis_apply,
360     `KomorebiPaperV.HilbertPackets.impulse_dense_span,
361     `KomorebiPaperV.HilbertPackets.shift_apply,
362     `KomorebiPaperV.HilbertPackets.reindex_single,
363     `KomorebiPaperV.HilbertPackets.shift_impulse,
364     `KomorebiPaperV.HilbertPackets.residue_projector_refinement,
365     `KomorebiPaperV.HilbertPackets.shift_generated_dense_span,
366     `KomorebiPaperV.HilbertPackets.finite_impulse_expansion,
367     `KomorebiPaperV.IntegerPolyphase.phase_val,
368     `KomorebiPaperV.IntegerPolyphase.address_phase_quotient,
369     `KomorebiPaperV.IntegerPolyphase.address_divmod,
370     `KomorebiPaperV.IntegerPolyphase.phase_address,
371     `KomorebiPaperV.IntegerPolyphase.quotient_address,
372     `KomorebiPaperV.IntegerPolyphase.synthesis_analysis,
373     `KomorebiPaperV.IntegerPolyphase.analysis_synthesis,
374     `KomorebiPaperV.IntegerPolyphase.channel_delay,
375     `KomorebiPaperV.IntegerPolyphase.sample_delay,
376     `KomorebiPaperV.IntegerPolyphase.emod_coarsen,
377     `KomorebiPaperV.IntegerPolyphase.residue_refinement,
378     `KomorebiPaperV.known_edge_error,
379     `KomorebiPaperV.estimated_edge_error,
380     `KomorebiPaperV.several_known_edges_error,
381     `KomorebiPaperV.known_edge_norm,
382     `KomorebiPaperV.several_known_edges_norm,
383     `KomorebiPaperV.estimated_edge_norm_bound,
384     `KomorebiPaperV.lifting_synthesis_analysis,
385     `KomorebiPaperV.lifting_analysis_synthesis,
386     `KomorebiPaperV.lifting_determinant,
387     `KomorebiPaperV.lifting_coordinates_roundtrip,
388     `KomorebiPaperV.MaskPerturbation.jump_measurable,
389     `KomorebiPaperV.MaskPerturbation.symmetric_difference_norm,
390     `KomorebiPaperV.MaskPerturbation.indicator_difference_norm,
391     `KomorebiPaperV.MaskPerturbation.jump_sub_same_set,
392     `KomorebiPaperV.MaskPerturbation.jump_error_decomposition,
393     `KomorebiPaperV.MaskPerturbation.finite_p_perturbation,
394     `KomorebiPaperV.MaskPerturbation.pointwise_sup_bound,
395     `KomorebiPaperV.MaskPerturbation.infinity_perturbation,
396     `KomorebiPaperV.MaskPerturbation.full_signal_perturbation,
397     `KomorebiPaperV.packet_idempotent,
398     `KomorebiPaperV.packet_annihilate,
399     `KomorebiPaperV.packet_complete,
400     `KomorebiPaperV.packet_refinement,
401     `KomorebiPaperV.address_synthesize_analyze,
402     `KomorebiPaperV.address_analyze_synthesize,
403     `KomorebiPaperV.residuePacket_idempotent,
404     `KomorebiPaperV.residuePacket_complete,
405     `KomorebiPaperV.PruningAlgorithm.solve_correct,
406     `KomorebiPaperV.PruningAlgorithm.solve_comparisons,
407     `KomorebiPaperV.PruningAlgorithm.solve_visits,
408     `KomorebiPaperV.PruningAlgorithm.solve_additions,
409     `KomorebiPaperV.PruningAlgorithm.internal_le_nodes,
410     `KomorebiPaperV.PruningAlgorithm.solve_linear_work,
411     `KomorebiPaperV.PruningAlgorithm.computed_antichain_optimal,
412     `KomorebiPaperV.PruningAlgorithm.antichain_probability,
413     `KomorebiPaperV.PruningSums.node_sum_branch,
414     `KomorebiPaperV.PruningSums.mem_selectedNodes,
415     `KomorebiPaperV.PruningSums.cutSum_eq_nodeSum,
416     `KomorebiPaperV.PruningSums.pruning_nodeSum,
417     `KomorebiPaperV.PruningSums.antichain_synthesis,
418     `KomorebiPaperV.PruningSums.packet_projector_synthesis,
419     `KomorebiPaperV.PruningSums.selected_global_minimum,
420     `KomorebiPaperV.PruningSums.antichain_perturbation,
421     `KomorebiPaperV.PruningSums.antichain_envelope_attained,
422     `KomorebiPaperV.PruningSums.antichain_selector_stable,
423     `KomorebiPaperV.PruningSums.objective_minimum,
424     `KomorebiPaperV.PruningSums.objective_positive_gap,
425     `KomorebiPaperV.PruningSums.objective_stability,
426     `KomorebiPaperV.PruningSums.singleton_selector,
427     `KomorebiPaperV.PruningSums.objective_gap_attained,
428     `KomorebiPaperV.SmithAction.action_mul,
429     `KomorebiPaperV.SmithAction.action_one,
430     `KomorebiPaperV.SmithAction.action_scale,
431     `KomorebiPaperV.SmithAction.action_nonzero,
432     `KomorebiPaperV.SmithAction.half_turn,
433     `KomorebiPaperV.SmithAction.half_turn_zero,
434     `KomorebiPaperV.SmithAction.half_turn_infinity,
435     `KomorebiPaperV.SmithAction.homogeneous_chart,
436     `KomorebiPaperV.SmithAction.chart_composition,
437     `KomorebiPaperV.SmithAction.finite_half_turn,
438     `KomorebiPaperV.SmithCyclic.omega_ne_zero,
439     `KomorebiPaperV.SmithCyclic.omega_pow,
440     `KomorebiPaperV.SmithCyclic.omega_two,
441     `KomorebiPaperV.SmithCyclic.action_respects_scaling,
442     `KomorebiPaperV.SmithCyclic.projective_mul,
443     `KomorebiPaperV.SmithCyclic.projective_one,
444     `KomorebiPaperV.SmithCyclic.cyclic_zero,
445     `KomorebiPaperV.SmithCyclic.cyclic_composition,
446     `KomorebiPaperV.SmithCyclic.cayley_conjugacy,
447     `KomorebiPaperV.SmithCyclic.cyclic_chart,
448     `KomorebiPaperV.SmithCyclic.two_phase_swap,
449     `KomorebiPaperV.SmithCyclic.two_phase_impedance_admittance,
450     `KomorebiPaperV.WaveletPackets.low_norm_bound,
451     `KomorebiPaperV.WaveletPackets.high_norm_bound,
452     `KomorebiPaperV.WaveletPackets.child_energy,
453     `KomorebiPaperV.WaveletPackets.packet_energy,
454     `KomorebiPaperV.WaveletPackets.energy_implies_adjoint_identity,
455     `KomorebiPaperV.WaveletPackets.packet_operator_reconstruction,
456     `KomorebiPaperV.WaveletPackets.packet_reconstruction,
457     `KomorebiPaperV.ZTransform.transform_unique,
458     `KomorebiPaperV.ZTransform.delay_transform,
459     `KomorebiPaperV.ZTransform.finite_transfer_transform,
460     `KomorebiPaperV.ZTransform.fir_channel_transform,
461     `KomorebiPaperV.ZTransform.fir_matrix_transform
462   ]
463   for target in targets do
464     match env.find? target with
465     | some (.thmInfo _) => pure ()
466     | _ => throwError "missing or non-theorem candidate target: {target}"
467   let mut audited : Nat := 0
468   for (name, info) in env.checked.get.constants.toList do
469     if Name.isPrefixOf `KomorebiPaperV name then
470       audited := audited + 1
471       if info.isUnsafe then
472         throwError "unsafe candidate declaration: {name}"
473       match info with
474       | .axiomInfo _ => throwError "candidate axiom declaration: {name}"
475       | .opaqueInfo _ => throwError "candidate opaque declaration: {name}"
476       | _ => pure ()
477       let axioms ← Lean.collectAxioms name
478       for axiomName in axioms do
479         unless axiomName == ``propext || axiomName == ``Classical.choice ||
480             axiomName == ``Quot.sound do
481           throwError "unexpected axiom {axiomName} in {name}"
482   logInfo m!"PAPER_V_CANDIDATE_TARGET_AUDIT_PASS: {targets.size} theorem targets; {audited} namespace declarations"

Back to source controls