KernelAudit.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIV
7 
8 /-!
9 # Paper IV v1.0.0 analytic bridge checkpoint kernel audit
10 
11 The explicit reports cover every declaration listed in the reviewed theorem
12 map. The command below additionally scans the whole `Komorebi.PaperIV`
13 namespace and rejects unsafe, axiom, opaque, or unexpected-axiom declarations.
14 -/
15 
16 #print axioms Komorebi.PaperIV.cyclicProjector
17 #print axioms Komorebi.PaperIV.coeff_cyclicProjector
18 #print axioms Komorebi.PaperIV.cyclicProjector_eq_zero_of_residue_ne
19 #print axioms Komorebi.PaperIV.cyclicProjector_eq_of_mod_eq
20 #print axioms Komorebi.PaperIV.cyclicProjector_idempotent
21 #print axioms Komorebi.PaperIV.cyclicProjector_orthogonal
22 #print axioms Komorebi.PaperIV.sum_cyclicProjector
23 #print axioms Komorebi.PaperIV.cyclicProjector_add
24 #print axioms Komorebi.PaperIV.cyclicProjector_sum
25 #print axioms Komorebi.PaperIV.cyclicProjector_product_packet
26 #print axioms Komorebi.PaperIV.cyclicProjector_product_other
27 #print axioms Komorebi.PaperIV.cyclic_product_law
28 #print axioms Komorebi.PaperIV.finiteRootAverage
29 #print axioms Komorebi.PaperIV.coeff_finiteRootAverage
30 #print axioms Komorebi.PaperIV.finiteRootAverage_eq_cyclicProjector
31 #print axioms Komorebi.PaperIV.exponentialGeneratingSeries
32 #print axioms Komorebi.PaperIV.coeff_exponentialGeneratingSeries
33 #print axioms Komorebi.PaperIV.transferSectionCoeff
34 #print axioms Komorebi.PaperIV.transferSection
35 #print axioms Komorebi.PaperIV.coeff_transferSection
36 #print axioms Komorebi.PaperIV.finiteRootAverage_exp_eq_transferSection
37 #print axioms Komorebi.PaperIV.finiteRootAverage_rescale_exp_eq_transferSection
38 #print axioms Komorebi.PaperIV.derivative_exponentialGeneratingSeries
39 #print axioms Komorebi.PaperIV.iterate_derivative_exponentialGeneratingSeries
40 #print axioms Komorebi.PaperIV.transferSectionCoeff_succ_of_pos
41 #print axioms Komorebi.PaperIV.transferSectionCoeff_succ_zero
42 #print axioms Komorebi.PaperIV.derivative_transferSection_of_pos
43 #print axioms Komorebi.PaperIV.derivative_transferSection_zero
44 #print axioms Komorebi.PaperIV.transferSectionCoeff_add_period
45 #print axioms Komorebi.PaperIV.iterate_derivative_transferSection
46 #print axioms Komorebi.PaperIV.constantCoeff_iterate_derivative_transferSection
47 #print axioms Komorebi.PaperIV.signedSectionCoeff
48 #print axioms Komorebi.PaperIV.signedSection
49 #print axioms Komorebi.PaperIV.coeff_signedSection
50 #print axioms Komorebi.PaperIV.signedSection_eq_inv_pow_mul_transferSection
51 #print axioms Komorebi.PaperIV.signedSectionCoeff_succ_of_pos
52 #print axioms Komorebi.PaperIV.signedSectionCoeff_succ_zero
53 #print axioms Komorebi.PaperIV.derivative_signedSection_of_pos
54 #print axioms Komorebi.PaperIV.derivative_signedSection_zero
55 #print axioms Komorebi.PaperIV.signedSectionCoeff_add_period
56 #print axioms Komorebi.PaperIV.iterate_derivative_signedSection
57 #print axioms Komorebi.PaperIV.constantCoeff_iterate_derivative_signedSection
58 #print axioms Komorebi.PaperIV.signedSection_eq_finiteRootAverage_rescale_exp
59 #print axioms Komorebi.PaperIV.signedSection_zero_eq_finite_exponential_average
60 #print axioms Komorebi.PaperIV.formalExpFamily
61 #print axioms Komorebi.PaperIV.formalExpFamily_zero
62 #print axioms Komorebi.PaperIV.formalExpFamily_one
63 #print axioms Komorebi.PaperIV.reducedDenominator
64 #print axioms Komorebi.PaperIV.coeff_reducedDenominator
65 #print axioms Komorebi.PaperIV.constantCoeff_reducedDenominator
66 #print axioms Komorebi.PaperIV.signedSection_zero_eq_expand_reducedDenominator
67 #print axioms Komorebi.PaperIV.negativeLogDenominator
68 #print axioms Komorebi.PaperIV.constantCoeff_negativeLogDenominator
69 #print axioms Komorebi.PaperIV.exp_subst_logOf
70 #print axioms Komorebi.PaperIV.mul_derivative_logOf
71 #print axioms Komorebi.PaperIV.formalExpFamily_eq_exp_subst
72 #print axioms Komorebi.PaperIV.reciprocalSeries
73 #print axioms Komorebi.PaperIV.constantCoeff_reciprocalSeries
74 #print axioms Komorebi.PaperIV.reciprocalSeries_zero
75 #print axioms Komorebi.PaperIV.reciprocalSeries_neg_one
76 #print axioms Komorebi.PaperIV.reciprocalSeries_one_eq_inverse
77 #print axioms Komorebi.PaperIV.reciprocalCoeff
78 #print axioms Komorebi.PaperIV.reciprocalOrdCoeff
79 #print axioms Komorebi.PaperIV.reciprocalCoeff_zero_parameter
80 #print axioms Komorebi.PaperIV.reciprocalCoeff_zero_parameter_of_pos
81 #print axioms Komorebi.PaperIV.formalExpFamily_semigroup
82 #print axioms Komorebi.PaperIV.blockCoeff
83 #print axioms Komorebi.PaperIV.blockCoeff_mul
84 #print axioms Komorebi.PaperIV.reciprocal_block_convolution
85 #print axioms Komorebi.PaperIV.reciprocalSeries_add
86 #print axioms Komorebi.PaperIV.reciprocalCoeff_addition
87 #print axioms Komorebi.PaperIV.egfCoeff
88 #print axioms Komorebi.PaperIV.egfCoeff_mul
89 #print axioms Komorebi.PaperIV.reciprocal_binomial_type
90 #print axioms Komorebi.PaperIV.derivative_rescale_exp
91 #print axioms Komorebi.PaperIV.derivative_formalExpFamily
92 #print axioms Komorebi.PaperIV.formalExpFamily_coefficient_recurrence
93 #print axioms Komorebi.PaperIV.kappaCoeff
94 #print axioms Komorebi.PaperIV.reducedTangentSeries
95 #print axioms Komorebi.PaperIV.coeff_reducedTangentSeries
96 #print axioms Komorebi.PaperIV.reducedDenominator_mul_reducedTangentSeries
97 #print axioms Komorebi.PaperIV.reducedTangent_coefficient_convolution
98 #print axioms Komorebi.PaperIV.derivative_reciprocalSeries
99 #print axioms Komorebi.PaperIV.reciprocalSeries_coefficient_recurrence
100 #print axioms Komorebi.PaperIV.reciprocalOrdCoeff_newton
101 #print axioms Komorebi.PaperIV.inverse_coefficient_convolution
102 #print axioms Komorebi.PaperIV.constantCoeff_inverse_of_one
103 #print axioms Komorebi.PaperIV.normalizedResidueSection
104 #print axioms Komorebi.PaperIV.coeff_normalizedResidueSection
105 #print axioms Komorebi.PaperIV.constantCoeff_normalizedResidueSection
106 #print axioms Komorebi.PaperIV.residueInverseCoeff
107 #print axioms Komorebi.PaperIV.residueInverseCoeff_triangular
108 #print axioms Komorebi.PaperIV.residueInverseCoeff_zero
109 #print axioms Komorebi.PaperIV.residueInverseCoeff_recurrence
110 #print axioms Komorebi.PaperIV.appellSeries
111 #print axioms Komorebi.PaperIV.appellCoeff
112 #print axioms Komorebi.PaperIV.egfCoeff_rescale_exp
113 #print axioms Komorebi.PaperIV.appellCoeff_zero_parameter
114 #print axioms Komorebi.PaperIV.appell_addition
115 #print axioms Komorebi.PaperIV.appellCoeff_at_zero
116 #print axioms Komorebi.PaperIV.appellPolynomial
117 #print axioms Komorebi.PaperIV.derivative_appellPolynomial
118 #print axioms Komorebi.PaperIV.formalAppellPolynomial
119 #print axioms Komorebi.PaperIV.derivative_formalAppellPolynomial
120 #print axioms Komorebi.PaperIV.eval_formalAppellPolynomial
121 #print axioms Komorebi.PaperIV.blockCoefficientSequence
122 #print axioms Komorebi.PaperIV.blockCoefficientSequence_mul
123 #print axioms Komorebi.PaperIV.appellPolynomial_eq_sparse_sum
124 #print axioms Komorebi.PaperIV.appellPolynomial_eq_block_sum
125 #print axioms Komorebi.PaperIV.residueAppellPolynomial_explicit
126 #print axioms Komorebi.PaperIV.appellSeries_two_parameter
127 #print axioms Komorebi.PaperIV.appell_two_parameter_convolution
128 #print axioms Komorebi.PaperIV.egfConstantCoeffAction
129 #print axioms Komorebi.PaperIV.egfConstantCoeffAction_X_pow
130 #print axioms Komorebi.PaperIV.egfConstantCoeffAction_residue_X_pow
131 #print axioms Komorebi.PaperIV.polynomialDifferentialEval
132 #print axioms Komorebi.PaperIV.polynomialDifferentialEval_X
133 #print axioms Komorebi.PaperIV.truncatedDifferentialOperator
134 #print axioms Komorebi.PaperIV.coeff_trunc_mul_trunc_of_lt
135 #print axioms Komorebi.PaperIV.X_pow_dvd_trunc_mul_trunc_sub_one
136 #print axioms Komorebi.PaperIV.truncatedDifferentialOperator_mul_apply_of_natDegree_le
137 #print axioms Komorebi.PaperIV.truncatedDifferentialOperator_normalizedResidueSection_inverse
138 #print axioms Komorebi.PaperIV.appellPolynomial_isMonicOfDegree
139 #print axioms Komorebi.PaperIV.blockAppellPolynomial_isMonicOfDegree
140 #print axioms Komorebi.PaperIV.eval_appellPolynomial_block_covariance
141 #print axioms Komorebi.PaperIV.residueAppellPolynomial_isMonicOfDegree
142 #print axioms Komorebi.PaperIV.eval_residueAppellPolynomial_covariance
143 #print axioms Komorebi.PaperIV.blockCoeff_rescale
144 #print axioms Komorebi.PaperIV.thetaSeries
145 #print axioms Komorebi.PaperIV.thetaCoeff
146 #print axioms Komorebi.PaperIV.thetaCoeff_reconstruction_unfactored
147 #print axioms Komorebi.PaperIV.thetaCoeff_reconstruction
148 #print axioms Komorebi.PaperIV.thetaSeries_zero
149 #print axioms Komorebi.PaperIV.thetaCoeff_zero_parameter
150 #print axioms Komorebi.PaperIV.thetaCoeff_zero_parameter_of_pos
151 #print axioms Komorebi.PaperIV.thetaSeries_neg_one_of_even
152 #print axioms Komorebi.PaperIV.thetaCoeff_neg_one_of_even_of_pos
153 #print axioms Komorebi.PaperIV.cyclicProjector_fixed_iff_rescale_covariant
154 #print axioms Komorebi.PaperIV.cyclicProjector_mem_range_iff_rescale_covariant
155 #print axioms Komorebi.PaperIV.bivariateExponentialGeneratingSeries
156 #print axioms Komorebi.PaperIV.coeff_bivariateExponentialGeneratingSeries
157 #print axioms Komorebi.PaperIV.separatedExponentialGeneratingSeries
158 #print axioms Komorebi.PaperIV.coeff_separatedExponentialGeneratingSeries
159 #print axioms Komorebi.PaperIV.transferSection_addition
160 #print axioms Komorebi.PaperIV.residuePochhammerProduct
161 #print axioms Komorebi.PaperIV.factorial_eq_residuePochhammerProduct
162 #print axioms Komorebi.PaperIV.residueZeroFCoeff
163 #print axioms Komorebi.PaperIV.residueZeroFSeries
164 #print axioms Komorebi.PaperIV.coeff_residueZeroFSeries
165 #print axioms Komorebi.PaperIV.residueZeroFCoeff_normalization
166 #print axioms Komorebi.PaperIV.residueParameter_eq_one
167 #print axioms Komorebi.PaperIV.omitted_residuePochhammer_eq_factorial
168 #print axioms Komorebi.PaperIV.transferSection_eq_residueZeroFSeries
169 #print axioms Komorebi.PaperIV.signedSection_addition
170 #print axioms Komorebi.PaperIV.signedDenominator_rescale_of_pow_eq_one
171 #print axioms Komorebi.PaperIV.signedDenominator_map_conj
172 #print axioms Komorebi.PaperIV.cyclicAlgebraPolynomial
173 #print axioms Komorebi.PaperIV.signedCyclicAlgebraPolynomial
174 #print axioms Komorebi.PaperIV.CyclicAlgebra
175 #print axioms Komorebi.PaperIV.SignedCyclicAlgebra
176 #print axioms Komorebi.PaperIV.cyclicGenerator
177 #print axioms Komorebi.PaperIV.signedCyclicGenerator
178 #print axioms Komorebi.PaperIV.cyclicGenerator_pow
179 #print axioms Komorebi.PaperIV.signedCyclicGenerator_pow
180 #print axioms Komorebi.PaperIV.cyclicGenerator_pow_eq_mod
181 #print axioms Komorebi.PaperIV.signedCyclicGenerator_pow_eq_mod
182 #print axioms Komorebi.PaperIV.cyclicAlgebraPowerBasis
183 #print axioms Komorebi.PaperIV.signedCyclicAlgebraPowerBasis
184 #print axioms Komorebi.PaperIV.cyclicAlgebraPowerBasis_dim
185 #print axioms Komorebi.PaperIV.signedCyclicAlgebraPowerBasis_dim
186 #print axioms Komorebi.PaperIV.cyclicAlgebraExponentialSeries
187 #print axioms Komorebi.PaperIV.signedCyclicAlgebraExponentialSeries
188 #print axioms Komorebi.PaperIV.cyclicAlgebra_exponential_eq_sections
189 #print axioms Komorebi.PaperIV.signedCyclicAlgebra_exponential_eq_sections
190 #print axioms Komorebi.PaperIV.signedShiftPowerMatrix
191 #print axioms Komorebi.PaperIV.signedShiftMatrix
192 #print axioms Komorebi.PaperIV.signedShiftPowerMatrix_apply
193 #print axioms Komorebi.PaperIV.signedShiftPowerMatrix_zero
194 #print axioms Komorebi.PaperIV.signedShiftPowerMatrix_mul
195 #print axioms Komorebi.PaperIV.signedShiftMatrix_pow
196 #print axioms Komorebi.PaperIV.signedShiftMatrix_pow_apply
197 #print axioms Komorebi.PaperIV.signedShiftMatrix_pow_order
198 #print axioms Komorebi.PaperIV.signedFundamentalMatrix
199 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_add
200 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_neg
201 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_mul_neg
202 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_isUnit
203 #print axioms Komorebi.PaperIV.reducedDenominator_reciprocalSeries_differentialEquation
204 #print axioms Komorebi.PaperIV.reciprocalOrdCoeff_parameter_equation
205 #print axioms Komorebi.PaperIV.reciprocalCoeff_parameter_equation
206 #print axioms Komorebi.PaperIV.reciprocalCoeff_parameter_recurrence
207 #print axioms Komorebi.PaperIV.reciprocalCoeff_block_zero
208 #print axioms Komorebi.PaperIV.reciprocalCoeff_one
209 #print axioms Komorebi.PaperIV.reciprocalCoeff_two_recurrence_form
210 #print axioms Komorebi.PaperIV.reciprocalCoeff_three_recurrence_form
211 #print axioms Komorebi.PaperIV.reciprocalCoeffPolynomial
212 #print axioms Komorebi.PaperIV.X_dvd_reciprocalCoeffPolynomial
213 #print axioms Komorebi.PaperIV.coeff_zero_reciprocalCoeffPolynomial
214 #print axioms Komorebi.PaperIV.reciprocalCoeffPolynomialOver
215 #print axioms Komorebi.PaperIV.eval_reciprocalCoeffPolynomialOver
216 #print axioms Komorebi.PaperIV.formalTransferTangent
217 #print axioms Komorebi.PaperIV.transferTangentCoeff
218 #print axioms Komorebi.PaperIV.transferTangentCoeff_eq_kappa
219 #print axioms Komorebi.PaperIV.transferTangentCoeff_convolution
220 #print axioms Komorebi.PaperIV.transferTangentCoeff_recurrence
221 #print axioms Komorebi.PaperIV.transferTangentCoeff_zero
222 #print axioms Komorebi.PaperIV.differentialBellSeries
223 #print axioms Komorebi.PaperIV.differentialBellSeries_zero
224 #print axioms Komorebi.PaperIV.differentialBellSeries_succ
225 #print axioms Komorebi.PaperIV.iterate_derivative_eq_differentialBellSeries_mul
226 #print axioms Komorebi.PaperIV.derivative_signedSection_zero_eq_neg_formalTransferTangent_mul
227 #print axioms Komorebi.PaperIV.differentialBellSeries_neg_formalTransferTangent_eq_neg_one
228 #print axioms Komorebi.PaperIV.normalizedResidueSectionAlg
229 #print axioms Komorebi.PaperIV.coeff_normalizedResidueSectionAlg
230 #print axioms Komorebi.PaperIV.constantCoeff_normalizedResidueSectionAlg
231 #print axioms Komorebi.PaperIV.normalizedResidueSectionAlg_eq_normalizedResidueSection
232 #print axioms Komorebi.PaperIV.normalizedResidueNegativeLog
233 #print axioms Komorebi.PaperIV.constantCoeff_normalizedResidueNegativeLog
234 #print axioms Komorebi.PaperIV.residuePowerSeries
235 #print axioms Komorebi.PaperIV.constantCoeff_residuePowerSeries
236 #print axioms Komorebi.PaperIV.residuePowerSeries_zero
237 #print axioms Komorebi.PaperIV.residuePowerSeries_neg_one
238 #print axioms Komorebi.PaperIV.residuePowerSeries_one_eq_inverse
239 #print axioms Komorebi.PaperIV.residuePowerCoeff
240 #print axioms Komorebi.PaperIV.residuePowerCoeff_zero
241 #print axioms Komorebi.PaperIV.residuePowerCoeff_one_eq_residueInverseCoeff
242 #print axioms Komorebi.PaperIV.residuePowerSeries_add
243 #print axioms Komorebi.PaperIV.residuePowerCoeff_addition
244 #print axioms Komorebi.PaperIV.residuePowerCoeffPolynomial
245 #print axioms Komorebi.PaperIV.eval_residuePowerCoeffPolynomial
246 #print axioms Komorebi.PaperIV.coeff_residuePowerCoeffPolynomial_parameterDegree
247 #print axioms Komorebi.PaperIV.natDegree_residuePowerCoeffPolynomial
248 #print axioms Komorebi.PaperIV.expandedResidueNegativeLog
249 #print axioms Komorebi.PaperIV.constantCoeff_expandedResidueNegativeLog
250 #print axioms Komorebi.PaperIV.expand_residuePowerSeries
251 #print axioms Komorebi.PaperIV.egfCoeff_expand_residuePowerSeries
252 #print axioms Komorebi.PaperIV.residueAppellPolynomialParam
253 #print axioms Komorebi.PaperIV.residueAppellPolynomialParam_eq_block
254 #print axioms Komorebi.PaperIV.residueAppellPolynomialParam_explicit
255 #print axioms Komorebi.PaperIV.derivative_residueAppellPolynomialParam
256 #print axioms Komorebi.PaperIV.eval_residueAppellPolynomialParam_add
257 #print axioms Komorebi.PaperIV.eval_residueAppellPolynomialParam_two_parameter
258 #print axioms Komorebi.PaperIV.residueAppellPolynomialParam_isMonicOfDegree
259 #print axioms Komorebi.PaperIV.eval_residueAppellPolynomialParam_covariance
260 #print axioms Komorebi.PaperIV.egfConstantCoeffAction_residuePowerSeries_X_pow
261 #print axioms Komorebi.PaperIV.truncatedDifferentialOperator_residuePowerSeries_inverse
262 #print axioms Komorebi.PaperIV.thetaPolynomial
263 #print axioms Komorebi.PaperIV.eval_thetaPolynomial
264 #print axioms Komorebi.PaperIV.natDegree_thetaPolynomial_le
265 #print axioms Komorebi.PaperIV.X_dvd_thetaPolynomial
266 #print axioms Komorebi.PaperIV.X_add_one_dvd_thetaPolynomial_of_even
267 #print axioms Komorebi.PaperIV.derivative_rescale_series
268 #print axioms Komorebi.PaperIV.rescale_C_series
269 #print axioms Komorebi.PaperIV.scaledReciprocalLogDerivative
270 #print axioms Komorebi.PaperIV.derivative_rescale_reciprocalSeries
271 #print axioms Komorebi.PaperIV.thetaLogDerivativeSeries
272 #print axioms Komorebi.PaperIV.derivative_thetaSeries
273 #print axioms Komorebi.PaperIV.coeff_thetaLogDerivativeSeries
274 #print axioms Komorebi.PaperIV.thetaOrdCoeff
275 #print axioms Komorebi.PaperIV.thetaOrdCoeff_zero
276 #print axioms Komorebi.PaperIV.thetaOrdCoeff_newton
277 #print axioms Komorebi.PaperIV.factorial_mul_kappaCoeff_one
278 #print axioms Komorebi.PaperIV.thetaCoeff_one
279 
280 #print axioms Komorebi.PaperIV.bellInput
281 #print axioms Komorebi.PaperIV.completeExponentialBell
282 #print axioms Komorebi.PaperIV.constantCoeff_bellInput
283 #print axioms Komorebi.PaperIV.completeExponentialBell_generating_coefficient
284 #print axioms Komorebi.PaperIV.completeExponentialBell_zero
285 #print axioms Komorebi.PaperIV.bellInput_reciprocal
286 #print axioms Komorebi.PaperIV.reciprocalCoeff_bell_formula
287 #print axioms Komorebi.PaperIV.coeff_one_negativeLogDenominator
288 #print axioms Komorebi.PaperIV.coeff_reciprocalCoeffPolynomialOver_parameterDegree
289 #print axioms Komorebi.PaperIV.natDegree_reciprocalCoeffPolynomialOver
290 #print axioms Komorebi.PaperIV.X_dvd_reciprocalCoeffPolynomialOver
291 #print axioms Komorebi.PaperIV.exponentialSumJet
292 #print axioms Komorebi.PaperIV.analyticAt_exponentialSumJet
293 #print axioms Komorebi.PaperIV.hasDerivAt_exponentialSumJet
294 #print axioms Komorebi.PaperIV.iteratedDeriv_exponentialSum
295 #print axioms Komorebi.PaperIV.exponentialSum_ode
296 #print axioms Komorebi.PaperIV.entireTransfer
297 #print axioms Komorebi.PaperIV.analyticAt_entireTransfer
298 #print axioms Komorebi.PaperIV.entireTransfer_eq_exponentialSum
299 #print axioms Komorebi.PaperIV.hasSum_finiteRootAverage
300 #print axioms Komorebi.PaperIV.hasSum_entireTransfer
301 #print axioms Komorebi.PaperIV.entireTransfer_eq_tsum
302 #print axioms Komorebi.PaperIV.entireTransfer_independent_root
303 #print axioms Komorebi.PaperIV.entireTransfer_ode
304 #print axioms Komorebi.PaperIV.entireSigned
305 #print axioms Komorebi.PaperIV.analyticAt_entireSigned
306 #print axioms Komorebi.PaperIV.hasSum_entireSigned
307 #print axioms Komorebi.PaperIV.entireSigned_eq_tsum
308 #print axioms Komorebi.PaperIV.entireSigned_independent_roots
309 #print axioms Komorebi.PaperIV.entireSigned_zero_eq_average
310 #print axioms Komorebi.PaperIV.entireTransfer_derivative_at_zero
311 #print axioms Komorebi.PaperIV.entireTransfer_initial_data
312 #print axioms Komorebi.PaperIV.entireSigned_eq_exponentialSum
313 #print axioms Komorebi.PaperIV.entireSigned_ode
314 #print axioms Komorebi.PaperIV.entireSigned_derivative_eq_scaled_transfer
315 #print axioms Komorebi.PaperIV.entireSigned_initial_data
316 #print axioms Komorebi.PaperIV.exponentialJetMatrix
317 #print axioms Komorebi.PaperIV.exponentialJetMatrix_factor
318 #print axioms Komorebi.PaperIV.det_exponentialJetMatrix
319 #print axioms Komorebi.PaperIV.det_exponentialJetMatrix_constant
320 #print axioms Komorebi.PaperIV.analyticWronskian
321 #print axioms Komorebi.PaperIV.transferWronskian_constant
322 #print axioms Komorebi.PaperIV.transferWronskian_eq
323 #print axioms Komorebi.PaperIV.signedWronskian_constant
324 #print axioms Komorebi.PaperIV.signedWronskian_eq_one
325 #print axioms Komorebi.PaperIV.hasSum_signedFundamentalMatrix_entry
326 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_first_column
327 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_diagonal
328 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_trace
329 
330 #print axioms Komorebi.PaperIV.hasSum_exponentialSumJet
331 #print axioms Komorebi.PaperIV.entireSigned_derivative_at_zero
332 #print axioms Komorebi.PaperIV.hasSum_entireSigned_derivative
333 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_entry_eq_derivative
334 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_det
335 #print axioms Komorebi.PaperIV.companionDisplacement
336 #print axioms Komorebi.PaperIV.companionDisplacement_lt
337 #print axioms Komorebi.PaperIV.companionEntrySign
338 #print axioms Komorebi.PaperIV.signedShiftMatrix_pow_entry_packet
339 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_entry
340 #print axioms Komorebi.PaperIV.aeval_signedShiftMatrix_first_column
341 #print axioms Komorebi.PaperIV.signedShiftMatrix_no_small_annihilator
342 #print axioms Komorebi.PaperIV.aeval_signedShiftMatrix_X_pow_add_one
343 #print axioms Komorebi.PaperIV.signedShiftMatrix_charpoly
344 #print axioms Komorebi.PaperIV.signedShiftMatrix_mem_spectrum_iff
345 #print axioms Komorebi.PaperIV.signedShiftMatrix_charpoly_separable
346 #print axioms Komorebi.PaperIV.signedShiftMatrix_charpoly_roots_card
347 #print axioms Komorebi.PaperIV.signedShiftMatrix_charpoly_roots_nodup
348 #print axioms Komorebi.PaperIV.ode_all_derivatives_zero
349 #print axioms Komorebi.PaperIV.entire_ode_zero_of_initial_zero
350 #print axioms Komorebi.PaperIV.entire_ode_unique
351 #print axioms Komorebi.PaperIV.transferCombination
352 #print axioms Komorebi.PaperIV.analyticAt_transferCombination
353 #print axioms Komorebi.PaperIV.transferCombination_derivative
354 #print axioms Komorebi.PaperIV.transferCombination_ode
355 #print axioms Komorebi.PaperIV.transferCombination_initial
356 #print axioms Komorebi.PaperIV.entireTransfer_solution_expansion
357 #print axioms Komorebi.PaperIV.transferCombination_injective
358 #print axioms Komorebi.PaperIV.entire_eq_of_all_derivatives
359 #print axioms Komorebi.PaperIV.entire_derivative_of_formal
360 #print axioms Komorebi.PaperIV.entireTransfer_derivative_of_pos
361 #print axioms Komorebi.PaperIV.entireTransfer_derivative_zero
362 #print axioms Komorebi.PaperIV.entireSigned_derivative_of_pos
363 #print axioms Komorebi.PaperIV.entireSigned_derivative_zero
364 #print axioms Komorebi.PaperIV.canonicalPrimitiveRoot
365 #print axioms Komorebi.PaperIV.canonicalSignedRoot
366 #print axioms Komorebi.PaperIV.canonicalPrimitiveRoot_isPrimitive
367 #print axioms Komorebi.PaperIV.canonicalSignedRoot_pow
368 #print axioms Komorebi.PaperIV.signedFundamentalMatrix_det_one
369 #print axioms Komorebi.PaperIV.norm_signedRoot
370 #print axioms Komorebi.PaperIV.norm_entireSigned_zero_le
371 #print axioms Komorebi.PaperIV.entireSigned_two_eq_cos
372 #print axioms Komorebi.PaperIV.entireSigned_two_zero_iff
373 #print axioms Komorebi.PaperIV.entireSigned_two_zero_derivative_ne_zero
374 #print axioms Komorebi.PaperIV.entireSigned_two_zero_iff_nat
375 #print axioms Komorebi.PaperIV.entireSigned_two_zero_order_one
376 #print axioms Komorebi.PaperIV.orderTwo_zero_spacing
377 #print axioms Komorebi.PaperIV.oddExponentialCenter
378 #print axioms Komorebi.PaperIV.near_cancellation_exists
379 #print axioms Komorebi.PaperIV.oddExponentialCenter_separation
380 #print axioms Komorebi.PaperIV.near_cancellation_unique
381 
382 #print axioms Komorebi.PaperIV.signedCombination
383 #print axioms Komorebi.PaperIV.signedCombination_eq_transfer
384 #print axioms Komorebi.PaperIV.entireSigned_solution_expansion
385 #print axioms Komorebi.PaperIV.signedCombination_injective
386 
387 #print axioms Komorebi.PaperIV.norm_one_add_lower_half
388 #print axioms Komorebi.PaperIV.log_one_add_lipschitz_half
389 #print axioms Komorebi.PaperIV.logarithmicZeroMap
390 #print axioms Komorebi.PaperIV.logarithmicZeroMap_mapsTo
391 #print axioms Komorebi.PaperIV.logarithmicZeroMap_lipschitz
392 #print axioms Komorebi.PaperIV.logarithmicZeroMap_fixed_iff
393 #print axioms Komorebi.PaperIV.perturbed_exponential_unique_zero
394 #print axioms Komorebi.PaperIV.perturbed_exponential_zero_distance
395 #print axioms Komorebi.PaperIV.perturbed_exponential_pointwise_distance
396 #print axioms Komorebi.PaperIV.hasDerivAt_perturbed_exponential
397 #print axioms Komorebi.PaperIV.perturbed_exponential_zero_derivative_lower
398 #print axioms Komorebi.PaperIV.perturbed_exponential_zero_order_one
399 #print axioms Komorebi.PaperIV.perturbed_exponential_derivative_error
400 #print axioms Komorebi.PaperIV.norm_log_one_add_sub_self_half
401 #print axioms Komorebi.PaperIV.perturbed_exponential_first_correction
402 #print axioms Komorebi.PaperIV.finiteExponentialRemainder
403 #print axioms Komorebi.PaperIV.analyticAt_finiteExponentialRemainder
404 #print axioms Komorebi.PaperIV.hasDerivAt_finiteExponentialRemainder
405 #print axioms Komorebi.PaperIV.iteratedDeriv_finiteExponentialRemainder
406 #print axioms Komorebi.PaperIV.finiteExponentialRemainder_strip_bound
407 #print axioms Komorebi.PaperIV.finite_two_term_normalization
408 #print axioms Komorebi.PaperIV.signedExponentialRemainder
409 #print axioms Komorebi.PaperIV.signed_two_term_normalization
410 #print axioms Komorebi.PaperIV.signed_two_term_zero_iff
411 #print axioms Komorebi.PaperIV.canonicalSignedVertex
412 #print axioms Komorebi.PaperIV.signedPolygonGap
413 #print axioms Komorebi.PaperIV.canonicalSignedVertex_exp
414 #print axioms Komorebi.PaperIV.canonicalSignedVertex_re
415 #print axioms Komorebi.PaperIV.canonicalSignedVertex_im
416 #print axioms Komorebi.PaperIV.norm_canonicalSignedVertex
417 #print axioms Komorebi.PaperIV.canonicalSignedVertex_last_angle
418 #print axioms Komorebi.PaperIV.canonicalSignedVertex_last_re
419 #print axioms Komorebi.PaperIV.canonicalSignedVertex_last_im
420 #print axioms Komorebi.PaperIV.signedPolygonGap_pos
421 #print axioms Komorebi.PaperIV.canonicalSignedVertex_re_gap
422 #print axioms Komorebi.PaperIV.canonicalSignedRemainder_strip_bound
423 #print axioms Komorebi.PaperIV.canonicalSignedVertex_adjacent_difference
424 #print axioms Komorebi.PaperIV.canonicalSignedDenominator
425 #print axioms Komorebi.PaperIV.signedZeroFrequency
426 #print axioms Komorebi.PaperIV.signedZeroCenter
427 #print axioms Komorebi.PaperIV.signed_sine_pos
428 #print axioms Komorebi.PaperIV.signedZeroFrequency_ne_zero
429 #print axioms Komorebi.PaperIV.signedZeroCenter_cancellation
430 #print axioms Komorebi.PaperIV.canonicalSignedRemainder_disk_bound
431 #print axioms Komorebi.PaperIV.signedRemainder_eventually_small_on_disks
432 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_conj
433 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_eventual_local_zero
434 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_unique_zero_real
435 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_local_zero_simple
436 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_eventual_positive_simple_zeros
437 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_local_zero_exponential_distance
438 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_local_strings
439 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_zero_lattice_distance
440 #print axioms Komorebi.PaperIV.signedRemainderScale
441 #print axioms Komorebi.PaperIV.signedRemainderEnvelope
442 #print axioms Komorebi.PaperIV.signedRemainderEnvelope_pos
443 #print axioms Komorebi.PaperIV.signedRemainderEnvelope_bounds
444 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_first_correction
445 #print axioms Komorebi.PaperIV.signedRemainderEnvelope_sq
446 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_normalized_derivative_error
447 
448 #print axioms Komorebi.PaperIV.signedFundamentalSector
449 #print axioms Komorebi.PaperIV.signed_cosine_pos
450 #print axioms Komorebi.PaperIV.cosine_arc_upper
451 #print axioms Komorebi.PaperIV.canonicalSignedVertex_upper_boundary
452 #print axioms Komorebi.PaperIV.canonicalSignedVertex_upper_projection
453 #print axioms Komorebi.PaperIV.canonicalSignedVertex_sector_gap
454 #print axioms Komorebi.PaperIV.finite_one_term_normalization
455 #print axioms Komorebi.PaperIV.finite_exponential_zero_balance
456 #print axioms Komorebi.PaperIV.signedSectorWidth
457 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_upper_sector_zero_bound
458 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_sector_zero_bound
459 #print axioms Komorebi.PaperIV.signedSectorWidth_pos
460 #print axioms Komorebi.PaperIV.signedRemainder_eventually_small_on_strip
461 #print axioms Komorebi.PaperIV.signed_integer_center
462 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_sector_exhaustion
463 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_rotation
464 #print axioms Komorebi.PaperIV.signedFundamentalSector_polar
465 #print axioms Komorebi.PaperIV.exists_signed_sector_rotation
466 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_global_exhaustion
467 #print axioms Komorebi.PaperIV.signedZeroFrequency_norm
468 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_order_rotation
469 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_derivative_rotation
470 #print axioms Komorebi.PaperIV.positive_real_rotation_unique
471 #print axioms Komorebi.PaperIV.signedZeroCenter_disk_index_unique
472 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_large_zero_orbits
473 #print axioms Komorebi.PaperIV.signedNormalizationFactor
474 #print axioms Komorebi.PaperIV.signedNormalizationFactor_ne_zero
475 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_derivative_normalization
476 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_relative_derivative_error
477 #print axioms Komorebi.PaperIV.signed_derivative_leading_norm
478 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_derivative_modulus_error
479 #print axioms Komorebi.PaperIV.signedFundamentalSector_of_arg
480 #print axioms Komorebi.PaperIV.canonicalSignedRemainder_three_jet_bound
481 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_two_term_dominance
482 
483 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_zero
484 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_finite_zeros_on_compact
485 #print axioms Komorebi.PaperIV.onSignedZeroRay
486 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_eventually_simple_on_rays
487 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_finite_exceptional_zeros
488 #print axioms Komorebi.PaperIV.entireReducedDenominator
489 #print axioms Komorebi.PaperIV.reducedDenominator_coeff_complex
490 #print axioms Komorebi.PaperIV.reducedDenominator_coeff_norm
491 #print axioms Komorebi.PaperIV.reducedDenominator_entire_radius
492 #print axioms Komorebi.PaperIV.analyticAt_entireReducedDenominator
493 #print axioms Komorebi.PaperIV.hasSum_entireReducedDenominator
494 #print axioms Komorebi.PaperIV.entireReducedDenominator_zero
495 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_eq_reduced_power
496 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_order_eq_reduced
497 #print axioms Komorebi.PaperIV.exists_complex_nth_root
498 #print axioms Komorebi.PaperIV.entireReducedDenominator_zero_ne_zero
499 #print axioms Komorebi.PaperIV.entireReducedDenominator_finite_zeros_on_compact
500 #print axioms Komorebi.PaperIV.onSignedZeroRay_power_positive
501 #print axioms Komorebi.PaperIV.entireReducedDenominator_finite_exceptional_zeros
502 #print axioms Komorebi.PaperIV.entireReducedDenominator_eventually_positive_simple
503 #print axioms Komorebi.PaperIV.entireReducedDenominator_two_zero_iff
504 #print axioms Komorebi.PaperIV.entireReducedDenominator_two_zero_order_one
505 #print axioms Komorebi.PaperIV.isLocalizedPositiveZero
506 #print axioms Komorebi.PaperIV.signedPositiveZero
507 #print axioms Komorebi.PaperIV.signedPositiveZero_spec
508 #print axioms Komorebi.PaperIV.signedPositiveZero_eq_of_unique
509 #print axioms Komorebi.PaperIV.signedPositiveZero_local_strings
510 #print axioms Komorebi.PaperIV.signedPositiveZero_global_strings
511 #print axioms Komorebi.PaperIV.signedZeroCenter_ge_radius
512 #print axioms Komorebi.PaperIV.signedPositiveZero_pos
513 #print axioms Komorebi.PaperIV.signedPositiveZero_injective_on_tail
514 #print axioms Komorebi.PaperIV.reducedPositiveZero
515 #print axioms Komorebi.PaperIV.reducedPositiveZero_global_strings
516 #print axioms Komorebi.PaperIV.reducedPositiveZero_injective_on_tail
517 #print axioms Komorebi.PaperIV.reducedPositiveZero_local_strings
518 #print axioms Komorebi.PaperIV.signedZeroCenter_tendsto_atTop
519 #print axioms Komorebi.PaperIV.signedPositiveZero_sub_center_isBigO_one
520 #print axioms Komorebi.PaperIV.signedPositiveZero_equivalent_center
521 #print axioms Komorebi.PaperIV.signedPositiveZero_tendsto_atTop
522 #print axioms Komorebi.PaperIV.reducedPositiveZero_equivalent_center_power
523 #print axioms Komorebi.PaperIV.signedPositiveZero_reciprocal_rpow_summable_iff
524 #print axioms Komorebi.PaperIV.reducedPositiveZero_reciprocal_rpow_summable_iff
525 #print axioms Komorebi.PaperIV.reducedPositiveZero_reciprocal_summable
526 #print axioms Komorebi.PaperIV.sequenceCounting
527 #print axioms Komorebi.PaperIV.lattice_window_counting
528 #print axioms Komorebi.PaperIV.signedPositiveZero_lattice_windows
529 #print axioms Komorebi.PaperIV.signedPositiveZero_tail_counting
530 #print axioms Komorebi.PaperIV.reducedTailProduct
531 #print axioms Komorebi.PaperIV.reducedPositiveZero_pos
532 #print axioms Komorebi.PaperIV.reducedTail_reciprocal_summable
533 #print axioms Komorebi.PaperIV.reducedTail_factors_norm_summable
534 #print axioms Komorebi.PaperIV.reducedTailProduct_multipliable
535 #print axioms Komorebi.PaperIV.reducedTailProduct_uniform_on_compact
536 #print axioms Komorebi.PaperIV.reducedTailProduct_locally_uniform
537 #print axioms Komorebi.PaperIV.analyticAt_reducedTailProduct
538 #print axioms Komorebi.PaperIV.reducedTailProduct_zero
539 #print axioms Komorebi.PaperIV.reducedTailProduct_ne_zero
540 #print axioms Komorebi.PaperIV.reducedTailProduct_zero_iff
541 
542 #print axioms Komorebi.PaperIV.finiteWeight
543 #print axioms Komorebi.PaperIV.finiteWeight_of_finite
544 #print axioms Komorebi.PaperIV.finiteWeight_mono
545 #print axioms Komorebi.PaperIV.finiteWeight_union_le
546 #print axioms Komorebi.PaperIV.finiteWeight_eq_ncard
547 #print axioms Komorebi.PaperIV.finiteWeight_between_tail_and_exceptions
548 #print axioms Komorebi.PaperIV.zeroDisk
549 #print axioms Komorebi.PaperIV.analyticZeroCount
550 #print axioms Komorebi.PaperIV.entire_analyticOrderAt_ne_top
551 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_order_ne_top
552 #print axioms Komorebi.PaperIV.entireReducedDenominator_order_ne_top
553 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_zeroDisk_finite
554 #print axioms Komorebi.PaperIV.entireReducedDenominator_zeroDisk_finite
555 #print axioms Komorebi.PaperIV.signedZeroEnumeration_exists_ge_three
556 #print axioms Komorebi.PaperIV.signedZeroEnumeration_exists_two
557 #print axioms Komorebi.PaperIV.signedZeroEnumeration_exists
558 #print axioms Komorebi.PaperIV.canonicalZeroEnumeration
559 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbit
560 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbit_norm
561 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbit_injective
562 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbit_zero_simple
563 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbitDisk
564 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.exceptions
565 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.exceptions_finite
566 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbitDisk_finite_card
567 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbitDisk_subset
568 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.zeroDisk_subset_union
569 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.weighted_count_bounds
570 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_zero_counting
571 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedRoot
572 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedDisk
573 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedExceptions
574 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedRoot_norm
575 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedRoot_injective
576 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedRoot_zero_simple
577 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedExceptions_finite
578 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedDisk_finite_card
579 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedDisk_subset
580 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedZeroDisk_subset_union
581 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reduced_weighted_count_bounds
582 #print axioms Komorebi.PaperIV.entireReducedDenominator_zero_counting_power
583 #print axioms Komorebi.PaperIV.entireReducedDenominator_zero_counting
584 #print axioms Komorebi.PaperIV.ZeroPowerSummable
585 #print axioms Komorebi.PaperIV.summable_iff_comp_of_finite_complement
586 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.root_equivalent_lattice
587 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.root_reciprocal_rpow_summable_iff
588 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedRoot_reciprocal_rpow_summable_iff
589 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbitZero
590 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbitZero_injective
591 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbitZero_finite_complement
592 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedZero
593 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedZero_injective
594 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedZero_finite_complement
595 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_zero_power_summable_iff
596 #print axioms Komorebi.PaperIV.entireReducedDenominator_zero_power_summable_iff
597 #print axioms Komorebi.PaperIV.entireReducedDenominator_reciprocal_zeros_summable
598 #print axioms Komorebi.PaperIV.weightedDirichletTerm
599 #print axioms Komorebi.PaperIV.weightedDirichletTerm_norm
600 #print axioms Komorebi.PaperIV.weightedDirichletTerm_differentiable
601 #print axioms Komorebi.PaperIV.weightedDirichletTerm_strip_bound
602 #print axioms Komorebi.PaperIV.weightedDirichlet_locally_uniform
603 #print axioms Komorebi.PaperIV.weightedDirichlet_differentiableOn
604 #print axioms Komorebi.PaperIV.absoluteZeroZetaTerm
605 #print axioms Komorebi.PaperIV.absoluteZeroZeta
606 #print axioms Komorebi.PaperIV.zero_norm_pos_of_value_at_zero
607 #print axioms Komorebi.PaperIV.absoluteZeroZetaTerm_norm
608 #print axioms Komorebi.PaperIV.absoluteZeroZeta_summable_norm_iff
609 #print axioms Komorebi.PaperIV.absoluteZeroZeta_locally_uniform
610 #print axioms Komorebi.PaperIV.absoluteZeroZeta_differentiableOn
611 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_zeta_absolute_convergence
612 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_zeta_locally_uniform
613 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_zeta_holomorphic
614 #print axioms Komorebi.PaperIV.entireReducedDenominator_zeta_absolute_convergence
615 #print axioms Komorebi.PaperIV.entireReducedDenominator_zeta_locally_uniform
616 #print axioms Komorebi.PaperIV.entireReducedDenominator_zeta_holomorphic
617 #print axioms Komorebi.PaperIV.signedPositiveZero_derivative_asymptotic
618 #print axioms Komorebi.PaperIV.signedPositiveZero_unique_global_strings
619 #print axioms Komorebi.PaperIV.signedPositiveZero_derivative_rotation
620 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_large_zero_strings
621 
622 #print axioms Komorebi.PaperIV.entireSigned_canonical_conj
623 #print axioms Komorebi.PaperIV.entireSigned_canonical_real
624 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_derivative_real
625 #print axioms Komorebi.PaperIV.signed_sine_mul_center
626 #print axioms Komorebi.PaperIV.signedZeroCenter_positive_phase
627 #print axioms Komorebi.PaperIV.signedZeroCenter_negative_phase
628 #print axioms Komorebi.PaperIV.signedDerivativeScale
629 #print axioms Komorebi.PaperIV.signedDerivativeMainTerm
630 #print axioms Komorebi.PaperIV.signedDerivativeScale_pos
631 #print axioms Komorebi.PaperIV.signedDerivativeMainTerm_ne_zero
632 #print axioms Komorebi.PaperIV.signed_derivative_leading_phase
633 #print axioms Komorebi.PaperIV.signedLeadingCorrection
634 #print axioms Komorebi.PaperIV.signedLeadingCorrection_eq_real_quotient
635 #print axioms Komorebi.PaperIV.signedLeadingCorrection_real
636 #print axioms Komorebi.PaperIV.signedRemainderEnvelope_center_tendsto_zero
637 #print axioms Komorebi.PaperIV.signedPositiveZero_first_correction
638 #print axioms Komorebi.PaperIV.norm_real_phase_sub_one_le
639 #print axioms Komorebi.PaperIV.relative_error_through_unit_phase
640 #print axioms Komorebi.PaperIV.signedPositiveZero_signed_derivative_asymptotic
641 #print axioms Komorebi.PaperIV.signedPositiveZero_eventual_derivative_sign
642 #print axioms Komorebi.PaperIV.signedPolygonGap_three
643 #print axioms Komorebi.PaperIV.signedZeroCenter_three
644 #print axioms Komorebi.PaperIV.canonicalSignedVertex_three_one
645 #print axioms Komorebi.PaperIV.canonicalSignedVertex_three_two
646 #print axioms Komorebi.PaperIV.signedExponentialRemainder_three
647 #print axioms Komorebi.PaperIV.signedLeadingCorrection_three
648 #print axioms Komorebi.PaperIV.signedPositiveZero_three_correction
649 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_derivative_lower_bound
650 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_derivative_power_bound
651 #print axioms Komorebi.PaperIV.branchedDirichletTerm
652 #print axioms Komorebi.PaperIV.branchedDirichletTerm_differentiable
653 #print axioms Komorebi.PaperIV.branchedDirichletTerm_norm
654 #print axioms Komorebi.PaperIV.branchedDirichletTerm_strip_bound
655 #print axioms Komorebi.PaperIV.branchedDirichlet_summable_norm
656 #print axioms Komorebi.PaperIV.branchedDirichlet_locally_uniform
657 #print axioms Komorebi.PaperIV.branchedDirichlet_entire
658 #print axioms Komorebi.PaperIV.branchedDirichlet_halfplane
659 #print axioms Komorebi.PaperIV.SimpleZeros
660 #print axioms Komorebi.PaperIV.SimpleZeros.toZero
661 #print axioms Komorebi.PaperIV.SimpleZeros.toZero_injective
662 #print axioms Komorebi.PaperIV.SimpleZeros.order_one
663 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_simple_zero_power_summable
664 #print axioms Komorebi.PaperIV.simple_logarithm_re
665 #print axioms Komorebi.PaperIV.derivativeZeroWeight
666 #print axioms Komorebi.PaperIV.derivativeZeroWeight_norm
667 #print axioms Komorebi.PaperIV.derivativeZeroWeight_power_summable
668 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_two_derivative_norm
669 #print axioms Komorebi.PaperIV.derivativeZeroWeight_two_power_summable
670 #print axioms Komorebi.PaperIV.derivativeWeightedZeroZetaTerm
671 #print axioms Komorebi.PaperIV.derivativeWeightedZeroZeta
672 #print axioms Komorebi.PaperIV.derivativeWeightedZeroZetaTerm_eq
673 #print axioms Komorebi.PaperIV.derivativeWeightedZeroZeta_summable_norm
674 #print axioms Komorebi.PaperIV.derivativeWeightedZeroZeta_two_summable_norm
675 #print axioms Komorebi.PaperIV.derivativeWeightedZeroZeta_entire
676 #print axioms Komorebi.PaperIV.derivativeWeightedZeroZeta_two_holomorphic
677 
678 #print axioms Komorebi.PaperIV.positiveZetaTerm
679 #print axioms Komorebi.PaperIV.exponentialZetaDifference
680 #print axioms Komorebi.PaperIV.positiveZetaTerm_entire
681 #print axioms Komorebi.PaperIV.exponentialZetaDifference_entire
682 #print axioms Komorebi.PaperIV.real_log_lipschitz_one
683 #print axioms Komorebi.PaperIV.positiveZetaTerm_norm_le_rpow
684 #print axioms Komorebi.PaperIV.exponentialZetaDifference_factor
685 #print axioms Komorebi.PaperIV.summable_polynomial_exponential
686 #print axioms Komorebi.PaperIV.exponentialZetaDifference_majorant
687 #print axioms Komorebi.PaperIV.exponentialZetaDifference_locally_uniform
688 #print axioms Komorebi.PaperIV.exponentialZetaDifference_sum_entire
689 #print axioms Komorebi.PaperIV.hurwitzRegularPart
690 #print axioms Komorebi.PaperIV.hurwitzRegularPart_entire
691 #print axioms Komorebi.PaperIV.hurwitzZeta_meromorphicAt
692 #print axioms Komorebi.PaperIV.hurwitzLatticeModel
693 #print axioms Komorebi.PaperIV.hurwitzLatticeModel_meromorphicAt
694 #print axioms Komorebi.PaperIV.hurwitzLatticeModel_differentiableAt
695 #print axioms Komorebi.PaperIV.hurwitzLatticeModel_residue
696 #print axioms Komorebi.PaperIV.meromorphicOrderAt_eq_neg_one_of_residue
697 #print axioms Komorebi.PaperIV.positiveZetaTerm_mul
698 #print axioms Komorebi.PaperIV.positiveZetaTerm_eq_cpow
699 #print axioms Komorebi.PaperIV.positiveZetaTerm_norm
700 #print axioms Komorebi.PaperIV.positiveZetaTerm_lattice_hasSum
701 #print axioms Komorebi.PaperIV.signedZeroCenter_positive
702 #print axioms Komorebi.PaperIV.signedZeroCenter_reciprocal_square_summable
703 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.root_tendsto_atTop
704 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.latticeCorrection
705 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.latticeCorrection_locally_uniform
706 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.latticeCorrection_entire
707 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.positiveZetaTerm_summable
708 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.latticePrefix
709 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.latticePrefix_entire
710 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.root_zeta_eq_model
711 #print axioms Komorebi.PaperIV.tsum_injection_add_complement
712 #print axioms Komorebi.PaperIV.finite_subtype_tsum_entire
713 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedExceptionZeta
714 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.absoluteExceptionZeta
715 #print axioms Komorebi.PaperIV.absoluteZeroZetaTerm_entire
716 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedExceptionZeta_entire
717 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.absoluteExceptionZeta_entire
718 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedZetaTerm
719 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.orbitZetaTerm
720 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedZeta_decomposition
721 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.absoluteZeta_decomposition
722 #print axioms Komorebi.PaperIV.reducedZetaCorrection
723 #print axioms Komorebi.PaperIV.absoluteZetaCorrection
724 #print axioms Komorebi.PaperIV.reducedZetaCorrection_entire
725 #print axioms Komorebi.PaperIV.absoluteZetaCorrection_entire
726 #print axioms Komorebi.PaperIV.entireReducedDenominator_zeta_eq_hurwitz
727 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_zeta_eq_hurwitz
728 #print axioms Komorebi.PaperIV.reducedZetaContinuation
729 #print axioms Komorebi.PaperIV.absoluteZetaContinuation
730 #print axioms Komorebi.PaperIV.reducedZetaContinuation_meromorphic
731 #print axioms Komorebi.PaperIV.absoluteZetaContinuation_meromorphic
732 #print axioms Komorebi.PaperIV.reducedZetaContinuation_holomorphic_off_pole
733 #print axioms Komorebi.PaperIV.absoluteZetaContinuation_holomorphic_off_pole
734 #print axioms Komorebi.PaperIV.entire_add_preserves_residue
735 #print axioms Komorebi.PaperIV.reducedZetaContinuation_residue
736 #print axioms Komorebi.PaperIV.absoluteZetaContinuation_residue
737 #print axioms Komorebi.PaperIV.reducedZetaContinuation_simple_pole
738 #print axioms Komorebi.PaperIV.absoluteZetaContinuation_simple_pole
739 #print axioms Komorebi.PaperIV.branchedZeroZetaTerm
740 #print axioms Komorebi.PaperIV.branchedZeroZeta
741 #print axioms Komorebi.PaperIV.branchedZeroZetaTerm_entire
742 #print axioms Komorebi.PaperIV.RealLogOnReducedTail
743 #print axioms Komorebi.PaperIV.reducedBranchCorrection
744 #print axioms Komorebi.PaperIV.reducedBranchCorrection_entire
745 #print axioms Komorebi.PaperIV.branchedZeroZetaTerm_eq_absolute_on_tail
746 #print axioms Komorebi.PaperIV.branchedReducedZeta_summable
747 #print axioms Komorebi.PaperIV.branchedReducedZeta_eq_absolute_add_entire
748 #print axioms Komorebi.PaperIV.branchedReducedZetaContinuation
749 #print axioms Komorebi.PaperIV.branchedReducedZetaContinuation_eq
750 #print axioms Komorebi.PaperIV.branchedReducedZetaContinuation_meromorphic
751 #print axioms Komorebi.PaperIV.branchedReducedZetaContinuation_holomorphic_off_pole
752 #print axioms Komorebi.PaperIV.branchedReducedZetaContinuation_residue
753 #print axioms Komorebi.PaperIV.branchedReducedZetaContinuation_simple_pole
754 #print axioms Komorebi.PaperIV.branchedReducedZetaContinuation_difference_entire
755 #print axioms Komorebi.PaperIV.quartic_root_square
756 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_four_eq_cos_cosh
757 #print axioms Komorebi.PaperIV.complex_cos_zero_iff_nat
758 #print axioms Komorebi.PaperIV.quarticPositiveZero
759 #print axioms Komorebi.PaperIV.quarticPositiveZero_pos
760 #print axioms Komorebi.PaperIV.quarticPositiveZero_div_sqrt
761 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_four_zero_iff
762 #print axioms Komorebi.PaperIV.quarticPositiveZero_simple
763 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_four_zero_order_one
764 #print axioms Komorebi.PaperIV.exactLatticeEnumeration
765 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.reducedZero_surjective_of_orbitZero
766 #print axioms Komorebi.PaperIV.SignedZeroEnumeration.exceptions_zero_of_surjective
767 #print axioms Komorebi.PaperIV.zero_zeta_exact_of_lattice
768 #print axioms Komorebi.PaperIV.signedZeroCenter_four
769 #print axioms Komorebi.PaperIV.orderTwo_full_lattice
770 #print axioms Komorebi.PaperIV.orderFour_full_lattice
771 #print axioms Komorebi.PaperIV.orderTwo_exact_zero_zeta_models
772 #print axioms Komorebi.PaperIV.orderFour_exact_zero_zeta_models
773 #print axioms Komorebi.PaperIV.entire_zero_of_halfplane
774 #print axioms Komorebi.PaperIV.zero_zeta_corrections_of_lattice
775 #print axioms Komorebi.PaperIV.orderTwo_zeta_corrections_zero
776 #print axioms Komorebi.PaperIV.orderFour_zeta_corrections_zero
777 #print axioms Komorebi.PaperIV.ZeroMultiplicityIndex
778 #print axioms Komorebi.PaperIV.indexedZero
779 #print axioms Komorebi.PaperIV.fullCanonicalProduct
780 #print axioms Komorebi.PaperIV.zeroMultiplicity_reciprocal_summable
781 #print axioms Komorebi.PaperIV.fullCanonicalProduct_factors_summable
782 #print axioms Komorebi.PaperIV.fullCanonicalProduct_multipliable
783 #print axioms Komorebi.PaperIV.fullCanonicalProduct_uniform_on_compact
784 #print axioms Komorebi.PaperIV.fullCanonicalProduct_locally_uniform
785 #print axioms Komorebi.PaperIV.fullCanonicalProduct_entire
786 #print axioms Komorebi.PaperIV.fullCanonicalProduct_zero
787 #print axioms Komorebi.PaperIV.fullCanonicalProduct_ne_zero
788 #print axioms Komorebi.PaperIV.fullCanonicalProduct_zero_iff_index
789 #print axioms Komorebi.PaperIV.indexedZero_ne_zero
790 #print axioms Komorebi.PaperIV.entire_zero_multiplicity_pos
791 #print axioms Komorebi.PaperIV.fullCanonicalProduct_zero_iff
792 #print axioms Komorebi.PaperIV.zeroMultiplicityIndex_countable
793 #print axioms Komorebi.PaperIV.entireReducedDenominator_full_product_properties
794 #print axioms Komorebi.PaperIV.reciprocalProduct
795 #print axioms Komorebi.PaperIV.reciprocalProduct_locally_uniform
796 #print axioms Komorebi.PaperIV.reciprocalProduct_entire
797 #print axioms Komorebi.PaperIV.reciprocalProduct_ne_zero
798 #print axioms Komorebi.PaperIV.zeroIndexFiberEquiv
799 #print axioms Komorebi.PaperIV.otherZeroProduct
800 #print axioms Komorebi.PaperIV.otherZeroProduct_entire
801 #print axioms Komorebi.PaperIV.otherZeroProduct_ne_zero_at_zero
802 #print axioms Komorebi.PaperIV.fullCanonicalProduct_factor_at_zero
803 #print axioms Komorebi.PaperIV.linear_zero_factor_order
804 #print axioms Komorebi.PaperIV.fullCanonicalProduct_order_at_zero
805 #print axioms Komorebi.PaperIV.fullCanonicalProduct_same_orders
806 #print axioms Komorebi.PaperIV.entireReducedDenominator_full_product_same_orders
807 #print axioms Komorebi.PaperIV.canonicalProductQuotient
808 #print axioms Komorebi.PaperIV.rawCanonicalProductQuotient_meromorphic
809 #print axioms Komorebi.PaperIV.rawCanonicalProductQuotient_order_zero
810 #print axioms Komorebi.PaperIV.canonicalProductQuotient_entire
811 #print axioms Komorebi.PaperIV.canonicalProductQuotient_ne_zero
812 #print axioms Komorebi.PaperIV.canonicalProductQuotient_eq_div
813 #print axioms Komorebi.PaperIV.fullCanonicalProduct_times_quotient
814 #print axioms Komorebi.PaperIV.canonicalProductQuotient_zero
815 #print axioms Komorebi.PaperIV.entireReducedDenominator_product_quotient
816 #print axioms Komorebi.PaperIV.entire_normalized_exists_log
817 #print axioms Komorebi.PaperIV.entire_realPart_sublinear_constant
818 #print axioms Komorebi.PaperIV.entire_zeroFree_sublinear_logNorm_eq_one
819 #print axioms Komorebi.PaperIV.entireReducedDenominator_product_quotient_has_log
820 
821 #print axioms Komorebi.PaperIV.entire_logCounting_poles_zero
822 #print axioms Komorebi.PaperIV.entire_normalized_proximity_inv_le
823 #print axioms Komorebi.PaperIV.entire_eventually_codiscrete_ne_zero
824 #print axioms Komorebi.PaperIV.entire_quotient_proximity_le
825 #print axioms Komorebi.PaperIV.entire_re_le_three_proximity_exp
826 #print axioms Komorebi.PaperIV.entire_proximity_le_of_growth
827 #print axioms Komorebi.PaperIV.entire_sublinear_factor_rigidity
828 #print axioms Komorebi.PaperIV.log_one_add_le_rpow_div
829 #print axioms Komorebi.PaperIV.zeroMultiplicity_reciprocal_rpow_summable
830 #print axioms Komorebi.PaperIV.reciprocalPowerMass
831 #print axioms Komorebi.PaperIV.reciprocalPowerMass_nonneg
832 #print axioms Komorebi.PaperIV.fullCanonicalProduct_growth
833 #print axioms Komorebi.PaperIV.entireReducedDenominator_norm_le
834 #print axioms Komorebi.PaperIV.entireReducedDenominator_and_product_growth
835 #print axioms Komorebi.PaperIV.entireReducedDenominator_quotient_eq_one
836 #print axioms Komorebi.PaperIV.entireReducedDenominator_eq_fullCanonicalProduct
837 #print axioms Komorebi.PaperIV.entireReducedDenominator_hadamard_uniform
838 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_hadamard
839 #print axioms Komorebi.PaperIV.zeroPartialFraction
840 #print axioms Komorebi.PaperIV.zeroPartialFraction_uniform_majorant
841 #print axioms Komorebi.PaperIV.zeroPartialFraction_norm_summable
842 #print axioms Komorebi.PaperIV.zeroPartialFraction_uniform_on_compact
843 #print axioms Komorebi.PaperIV.logDeriv_linear_factor
844 #print axioms Komorebi.PaperIV.fullCanonicalProduct_logDeriv
845 #print axioms Komorebi.PaperIV.entireReducedDenominator_partialFractions
846 #print axioms Komorebi.PaperIV.zeroPartialFraction_locally_uniform
847 #print axioms Komorebi.PaperIV.analyticTransferTangent
848 #print axioms Komorebi.PaperIV.analyticTransferTangent_eq_reduced_logDeriv
849 #print axioms Komorebi.PaperIV.analyticTransferTangent_mittagLeffler
850 #print axioms Komorebi.PaperIV.analyticTransferTangent_mittagLeffler_absolute
851 #print axioms Komorebi.PaperIV.analyticTransferTangent_mittagLeffler_locally_uniform
852 #print axioms Komorebi.PaperIV.locally_uniform_sum_deriv
853 #print axioms Komorebi.PaperIV.zeroResolventJet
854 #print axioms Komorebi.PaperIV.zeroResolventJet_hasDerivAt
855 #print axioms Komorebi.PaperIV.zeroResolventJet_locally_uniform
856 #print axioms Komorebi.PaperIV.zeroPowerSum
857 #print axioms Komorebi.PaperIV.zeroPowerSum_hasSum_from_resolvent
858 #print axioms Komorebi.PaperIV.zeroPowerSum_resolvent_derivative
859 #print axioms Komorebi.PaperIV.entireReducedDenominator_iteratedDeriv_zero
860 #print axioms Komorebi.PaperIV.zeroResolvent_analyticAt_zero
861 #print axioms Komorebi.PaperIV.reducedZeroPowerSum_convolution
862 #print axioms Komorebi.PaperIV.zeroMomentSeries
863 #print axioms Komorebi.PaperIV.reducedDenominator_mul_zeroMomentSeries
864 #print axioms Komorebi.PaperIV.kappaCoeff_eq_zeroPowerSum
865 #print axioms Komorebi.PaperIV.reducedZeroPowerSum_newton
866 #print axioms Komorebi.PaperIV.transferTangentCoeff_zero_sum
867 #print axioms Komorebi.PaperIV.analyticTransferTangent_coefficient_hasSum
868 #print axioms Komorebi.PaperIV.bellInput_zero_sums
869 #print axioms Komorebi.PaperIV.reciprocalCoeff_zero_sum_bell
870 #print axioms Komorebi.PaperIV.powerSeries_linear_ode_unique
871 #print axioms Komorebi.PaperIV.thetaZeroBellInput
872 #print axioms Komorebi.PaperIV.thetaZeroBellInput_derivative
873 #print axioms Komorebi.PaperIV.thetaSeries_eq_zero_bell_exp
874 #print axioms Komorebi.PaperIV.thetaCoeff_zero_sum_bell
875 #print axioms Komorebi.PaperIV.differentiableOn_ball_taylor_hasSum
876 #print axioms Komorebi.PaperIV.reducedZeroPowerSum_logarithm
877 #print axioms Komorebi.PaperIV.reducedZeroPowerSum_resolvent_hasSum
878 
879 #print axioms Komorebi.PaperIV.finite_positive_gap
880 #print axioms Komorebi.PaperIV.finite_exponential_dominant_bound
881 #print axioms Komorebi.PaperIV.finite_exponential_dominant_tendsto
882 #print axioms Komorebi.PaperIV.unit_complex_re_lt_one
883 #print axioms Komorebi.PaperIV.canonicalSignedVertex_injective
884 #print axioms Komorebi.PaperIV.canonicalSignedVertex_mul_star_self
885 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_dominant_ray
886 #print axioms Komorebi.PaperIV.diskMaximumModulus
887 #print axioms Komorebi.PaperIV.entireGrowthOrder
888 #print axioms Komorebi.PaperIV.entireExponentialType
889 #print axioms Komorebi.PaperIV.norm_le_diskMaximumModulus
890 #print axioms Komorebi.PaperIV.diskMaximumModulus_le
891 #print axioms Komorebi.PaperIV.log_growth_ratio_of_exp_bounds
892 #print axioms Komorebi.PaperIV.order_ratio_of_log_growth
893 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_ray_lower
894 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_maximum_bounds
895 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_type_limit
896 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_order_limit
897 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_order_one
898 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_type_one
899 #print axioms Komorebi.PaperIV.entireReducedDenominator_maximum_bounds
900 #print axioms Komorebi.PaperIV.entireReducedDenominator_growth_limit
901 #print axioms Komorebi.PaperIV.entireReducedDenominator_order_limit
902 #print axioms Komorebi.PaperIV.entireReducedDenominator_order_exact
903 #print axioms Komorebi.PaperIV.rayDirection
904 #print axioms Komorebi.PaperIV.norm_rayDirection
905 #print axioms Komorebi.PaperIV.signedProjection
906 #print axioms Komorebi.PaperIV.signedIndicator
907 #print axioms Komorebi.PaperIV.signedProjection_cos
908 #print axioms Komorebi.PaperIV.signedIndicator_cos
909 #print axioms Komorebi.PaperIV.continuous_signedProjection
910 #print axioms Komorebi.PaperIV.continuous_signedIndicator
911 #print axioms Komorebi.PaperIV.signedProjection_le_indicator
912 #print axioms Komorebi.PaperIV.canonicalSignedVertex_sum_zero
913 #print axioms Komorebi.PaperIV.signedIndicator_nonneg
914 #print axioms Komorebi.PaperIV.canonicalSignedVertex_pow
915 #print axioms Komorebi.PaperIV.signed_root_in_vertices
916 #print axioms Komorebi.PaperIV.unit_complex_same_real
917 #print axioms Komorebi.PaperIV.signed_maximizer_strict_of_not_tie
918 #print axioms Komorebi.PaperIV.signedTieDirection
919 #print axioms Komorebi.PaperIV.signedTieDirection_iff
920 #print axioms Komorebi.PaperIV.range_erase_nonempty
921 #print axioms Komorebi.PaperIV.vertexProjectionGap
922 #print axioms Komorebi.PaperIV.directionSeparation
923 #print axioms Komorebi.PaperIV.continuous_vertexProjectionGap
924 #print axioms Komorebi.PaperIV.continuous_directionSeparation
925 #print axioms Komorebi.PaperIV.directionSeparation_pos
926 #print axioms Komorebi.PaperIV.compact_directions_uniform_gap
927 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_dominant_error
928 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_compact_dominant_sectors
929 #print axioms Komorebi.PaperIV.alignedRadii
930 #print axioms Komorebi.PaperIV.alignedRadii_tendsto
931 #print axioms Komorebi.PaperIV.alignedRadii_phase
932 #print axioms Komorebi.PaperIV.alignedRadii_equal_projection
933 #print axioms Komorebi.PaperIV.alignedRadii_lower_projection
934 #print axioms Komorebi.PaperIV.finite_unit_exponential_aligned_limit
935 #print axioms Komorebi.PaperIV.log_norm_slope_of_normalized_limit
936 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_indicator_upper
937 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_log_indicator_upper
938 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_real_normalization
939 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_indicator_sequence
940 #print axioms Komorebi.PaperIV.limsup_eq_of_upper_and_sequence
941 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_indicator
942 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_indicator_nonzero_radii
943 
944 #print axioms Komorebi.PaperIV.IsHilbertTraceClass
945 #print axioms Komorebi.PaperIV.diagonalHilbertBasis
946 #print axioms Komorebi.PaperIV.diagonalHilbertBasis_inner
947 #print axioms Komorebi.PaperIV.diagonalHilbertBasis_norm
948 #print axioms Komorebi.PaperIV.diagonalHilbertBasis_apply
949 #print axioms Komorebi.PaperIV.diagonalRankOne
950 #print axioms Komorebi.PaperIV.diagonalRankOne_norm
951 #print axioms Komorebi.PaperIV.diagonalRankOne_summable
952 #print axioms Komorebi.PaperIV.diagonalOperator
953 #print axioms Komorebi.PaperIV.diagonalOperator_traceClass
954 #print axioms Komorebi.PaperIV.diagonalOperator_apply
955 #print axioms Komorebi.PaperIV.diagonalOperator_apply_basis
956 #print axioms Komorebi.PaperIV.diagonalOperator_pow_apply
957 #print axioms Komorebi.PaperIV.hilbertBasis_hasSum_squared_coordinates
958 #print axioms Komorebi.PaperIV.diagonal_trace_double_summable
959 #print axioms Komorebi.PaperIV.hilbertBasisTrace
960 #print axioms Komorebi.PaperIV.diagonalOperator_trace_in_any_basis
961 #print axioms Komorebi.PaperIV.diagonalOperator_trace_eq
962 #print axioms Komorebi.PaperIV.diagonalOperator_pow_eq
963 #print axioms Komorebi.PaperIV.diagonalOperator_pow_trace
964 #print axioms Komorebi.PaperIV.diagonalCompression
965 #print axioms Komorebi.PaperIV.diagonalCompression_eq_diagonal
966 #print axioms Komorebi.PaperIV.diagonalCompression_determinant
967 #print axioms Komorebi.PaperIV.diagonalFredholmDeterminant
968 #print axioms Komorebi.PaperIV.diagonalFredholmDeterminant_compression_limit
969 #print axioms Komorebi.PaperIV.reducedZeroEigenvalue
970 #print axioms Komorebi.PaperIV.reducedZeroEigenvalue_norm_summable
971 #print axioms Komorebi.PaperIV.reducedZeroOperator
972 #print axioms Komorebi.PaperIV.reducedZeroOperator_traceClass
973 #print axioms Komorebi.PaperIV.reducedZeroOperator_basis
974 #print axioms Komorebi.PaperIV.reducedZeroOperator_fredholm
975 #print axioms Komorebi.PaperIV.reducedZeroOperator_trace_power
976 #print axioms Komorebi.PaperIV.reducedZeroOperator_finite_determinants_uniform
977 #print axioms Komorebi.PaperIV.powerSumLog
978 #print axioms Komorebi.PaperIV.powerSumLog_constantCoeff
979 #print axioms Komorebi.PaperIV.powerSumLog_derivative_coeff
980 #print axioms Komorebi.PaperIV.homogeneousSeries
981 #print axioms Komorebi.PaperIV.homogeneousCoeff
982 #print axioms Komorebi.PaperIV.homogeneousSeries_constantCoeff
983 #print axioms Komorebi.PaperIV.homogeneousSeries_derivative
984 #print axioms Komorebi.PaperIV.homogeneousCoeff_recurrence
985 #print axioms Komorebi.PaperIV.homogeneousGeometric
986 #print axioms Komorebi.PaperIV.homogeneousGeometric_coeff
987 #print axioms Komorebi.PaperIV.homogeneousGeometric_constantCoeff
988 #print axioms Komorebi.PaperIV.homogeneousGeometric_inverse
989 #print axioms Komorebi.PaperIV.homogeneousGeometric_derivative
990 #print axioms Komorebi.PaperIV.finiteHomogeneousSeries
991 #print axioms Komorebi.PaperIV.finiteHomogeneousSeries_constantCoeff
992 #print axioms Komorebi.PaperIV.finiteHomogeneousSeries_derivative
993 #print axioms Komorebi.PaperIV.finiteHomogeneousSeries_eq_homogeneous
994 #print axioms Komorebi.PaperIV.finiteHomogeneousSeries_monomials
995 #print axioms Komorebi.PaperIV.summable_norm_positive_powers
996 #print axioms Komorebi.PaperIV.homogeneousCoeff_zero
997 #print axioms Komorebi.PaperIV.homogeneousCoeff_succ
998 #print axioms Komorebi.PaperIV.homogeneousCoeff_continuous
999 #print axioms Komorebi.PaperIV.homogeneousSeries_congr_positive
1000 #print axioms Komorebi.PaperIV.completeHomogeneous
1001 #print axioms Komorebi.PaperIV.finiteHomogeneousSeries_coefficient_limit
1002 #print axioms Komorebi.PaperIV.completeHomogeneous_monomial_limit
1003 #print axioms Komorebi.PaperIV.repeatedEigenvalue
1004 #print axioms Komorebi.PaperIV.repeatedEigenvalue_norm_summable
1005 #print axioms Komorebi.PaperIV.repeatedEigenvalue_powerSum
1006 #print axioms Komorebi.PaperIV.reciprocalSeries_eq_homogeneous_zero_sums
1007 #print axioms Komorebi.PaperIV.reciprocalCoeff_completeHomogeneous
1008 #print axioms Komorebi.PaperIV.reciprocalCoeff_symmetric_polynomial_continuation
1009 #print axioms Komorebi.PaperIV.entireNormalizedSection
1010 #print axioms Komorebi.PaperIV.normalizedSection_coeff_norm
1011 #print axioms Komorebi.PaperIV.normalizedSection_entire_radius
1012 #print axioms Komorebi.PaperIV.analyticAt_entireNormalizedSection
1013 #print axioms Komorebi.PaperIV.hasSum_entireNormalizedSection
1014 #print axioms Komorebi.PaperIV.entireNormalizedSection_zero
1015 #print axioms Komorebi.PaperIV.entireNormalizedSection_iteratedDeriv_zero
1016 #print axioms Komorebi.PaperIV.entireNormalizedSection_transfer
1017 #print axioms Komorebi.PaperIV.entireTransfer_unit_norm_le
1018 #print axioms Komorebi.PaperIV.finite_sum_le_finsum_nonneg
1019 #print axioms Komorebi.PaperIV.entire_divisor_eq_orderNat
1020 #print axioms Komorebi.PaperIV.entire_zero_finite_weight_growth
1021 #print axioms Komorebi.PaperIV.entire_zero_subtype_weight_growth
1022 #print axioms Komorebi.PaperIV.entire_zero_bounded_finite
1023 #print axioms Komorebi.PaperIV.weighted_growth_summable_large
1024 #print axioms Komorebi.PaperIV.weighted_growth_summable
1025 #print axioms Komorebi.PaperIV.entire_growth_zeroPowerSummable
1026 #print axioms Komorebi.PaperIV.entire_sublinear_growth_hadamard
1027 #print axioms Komorebi.PaperIV.entireNormalizedSection_norm_le
1028 #print axioms Komorebi.PaperIV.normalizedSectionGrowthConstant
1029 #print axioms Komorebi.PaperIV.normalizedSectionGrowthConstant_pos
1030 #print axioms Komorebi.PaperIV.entireNormalizedSection_disk_growth
1031 #print axioms Komorebi.PaperIV.entireNormalizedSection_zeroPowerSummable
1032 #print axioms Komorebi.PaperIV.entireTransfer_positive_ray
1033 #print axioms Komorebi.PaperIV.log_growth_ratio_of_polynomial_exp_bounds
1034 #print axioms Komorebi.PaperIV.entireTransfer_positive_ray_lower
1035 #print axioms Komorebi.PaperIV.entireNormalizedSection_maximum_bounds
1036 #print axioms Komorebi.PaperIV.entireNormalizedSection_growth_limit
1037 #print axioms Komorebi.PaperIV.entireNormalizedSection_order_exact
1038 #print axioms Komorebi.PaperIV.entireNormalizedSection_hadamard
1039 #print axioms Komorebi.PaperIV.entireNormalizedSection_hadamard_uniform
1040 #print axioms Komorebi.PaperIV.analyticTaylorSeries_entireNormalizedSection
1041 #print axioms Komorebi.PaperIV.normalized_zeroMomentSeries
1042 #print axioms Komorebi.PaperIV.normalized_zeroPowerSum
1043 #print axioms Komorebi.PaperIV.bellInput_normalized_zeros
1044 #print axioms Komorebi.PaperIV.residuePowerCoeff_zero_sum_bell
1045 #print axioms Komorebi.PaperIV.powerSeries_eq_of_derivative_constant
1046 #print axioms Komorebi.PaperIV.analyticTaylorSeries_log
1047 #print axioms Komorebi.PaperIV.analyticTaylorSeries_exp
1048 #print axioms Komorebi.PaperIV.normalizedAnalyticPower
1049 #print axioms Komorebi.PaperIV.normalizedAnalyticPower_taylor
1050 #print axioms Komorebi.PaperIV.normalizedAnalyticPower_zero_sum_bell
1051 #print axioms Komorebi.PaperIV.analyticTaylorSeries
1052 #print axioms Komorebi.PaperIV.analyticTaylorSeries_coeff
1053 #print axioms Komorebi.PaperIV.analyticTaylorSeries_constantCoeff
1054 #print axioms Komorebi.PaperIV.analyticTaylorSeries_congr
1055 #print axioms Komorebi.PaperIV.analyticTaylorSeries_mul
1056 #print axioms Komorebi.PaperIV.analyticTaylorSeries_add
1057 #print axioms Komorebi.PaperIV.analyticTaylorSeries_const
1058 #print axioms Komorebi.PaperIV.analyticTaylorSeries_pow
1059 #print axioms Komorebi.PaperIV.analyticTaylorSeries_inverse_product
1060 #print axioms Komorebi.PaperIV.analyticTaylorSeries_neg
1061 #print axioms Komorebi.PaperIV.analyticTaylorSeries_deriv
1062 #print axioms Komorebi.PaperIV.analyticTaylorSeries_zeroResolvent
1063 #print axioms Komorebi.PaperIV.hadamard_taylor_zeroMoment_identity
1064 #print axioms Komorebi.PaperIV.analyticTaylorCoefficient
1065 #print axioms Komorebi.PaperIV.analyticTaylorCoefficient_norm_le
1066 #print axioms Komorebi.PaperIV.analyticTaylorCoefficient_isBigO
1067 #print axioms Komorebi.PaperIV.analyticTaylorCoefficient_block_error
1068 #print axioms Komorebi.PaperIV.principalPartSeries
1069 #print axioms Komorebi.PaperIV.principalPartSeries_coefficient
1070 #print axioms Komorebi.PaperIV.principalPartSeries_inverse
1071 #print axioms Komorebi.PaperIV.lower_principal_part_choose_bound
1072 #print axioms Komorebi.PaperIV.poleTerm
1073 #print axioms Komorebi.PaperIV.polePrincipalPart
1074 #print axioms Komorebi.PaperIV.rawPoleRemainder
1075 #print axioms Komorebi.PaperIV.poleTerm_analyticAt
1076 #print axioms Komorebi.PaperIV.poleTerm_meromorphicAt
1077 #print axioms Komorebi.PaperIV.polePrincipalPart_analyticAt
1078 #print axioms Komorebi.PaperIV.rawPoleRemainder_meromorphic
1079 #print axioms Komorebi.PaperIV.rawPoleRemainder_analyticAt
1080 #print axioms Komorebi.PaperIV.meromorphicOrderAt_nonneg_of_bounded
1081 #print axioms Komorebi.PaperIV.rawPoleRemainder_bounded_at_pole
1082 #print axioms Komorebi.PaperIV.removedPoleRemainder
1083 #print axioms Komorebi.PaperIV.removedPoleRemainder_analyticOnNhd
1084 #print axioms Komorebi.PaperIV.removedPoleRemainder_eq_raw
1085 #print axioms Komorebi.PaperIV.analyticTaylorSeries_sub
1086 #print axioms Komorebi.PaperIV.analyticTaylorSeries_finsetSum
1087 #print axioms Komorebi.PaperIV.analyticTaylorSeries_id
1088 #print axioms Komorebi.PaperIV.analyticTaylorSeries_poleTerm
1089 #print axioms Komorebi.PaperIV.analyticTaylorCoefficient_principalPart
1090 #print axioms Komorebi.PaperIV.analyticTaylorSeries_canonicalSignedDenominator
1091 #print axioms Komorebi.PaperIV.reciprocalSeries_nat
1092 #print axioms Komorebi.PaperIV.analyticTaylorSeries_reciprocal_signed
1093 #print axioms Komorebi.PaperIV.reciprocalCoeff_analyticTaylor
1094 #print axioms Komorebi.PaperIV.poleNumerator
1095 #print axioms Komorebi.PaperIV.canonicalPoleCoefficient
1096 #print axioms Komorebi.PaperIV.poleNumerator_analyticAt
1097 #print axioms Komorebi.PaperIV.canonicalPoleCoefficient_leading
1098 #print axioms Komorebi.PaperIV.poleNumerator_identity
1099 #print axioms Komorebi.PaperIV.polePrincipalPart_scaled
1100 #print axioms Komorebi.PaperIV.canonicalPoleCoefficient_local_bound
1101 #print axioms Komorebi.PaperIV.polePrincipalPart_scaled_general
1102 #print axioms Komorebi.PaperIV.polePrincipalPart_scaled_limit
1103 #print axioms Komorebi.PaperIV.principalPart_leading_coefficient
1104 #print axioms Komorebi.PaperIV.removedPoleRemainder_taylor
1105 #print axioms Komorebi.PaperIV.nearest_pole_taylor_bound
1106 #print axioms Komorebi.PaperIV.reciprocalCoeff_nearest_pole_bound
1107 #print axioms Komorebi.PaperIV.principalCoefficientSum
1108 #print axioms Komorebi.PaperIV.leadingPoleCoefficient
1109 #print axioms Komorebi.PaperIV.lowerPrincipalConstant
1110 #print axioms Komorebi.PaperIV.lowerPrincipalConstant_nonneg
1111 #print axioms Komorebi.PaperIV.lowerPrincipalConstant_one
1112 #print axioms Komorebi.PaperIV.principalCoefficientSum_split
1113 #print axioms Komorebi.PaperIV.principalCoefficientSum_leading_error
1114 #print axioms Komorebi.PaperIV.principalCoefficientSum_one
1115 #print axioms Komorebi.PaperIV.reciprocalCoeff_leading_bound
1116 #print axioms Komorebi.PaperIV.leadingZeroWeight
1117 #print axioms Komorebi.PaperIV.leadingZeroWeight_rotation
1118 #print axioms Komorebi.PaperIV.leadingPoleCoefficient_eq_zero_weights
1119 #print axioms Komorebi.PaperIV.leading_zero_sum_orbit_reduction
1120 #print axioms Komorebi.PaperIV.reciprocalCoeff_orbit_leading_bound
1121 #print axioms Komorebi.PaperIV.cosineNearestZeros
1122 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_two_cos
1123 #print axioms Komorebi.PaperIV.cosineNearestZeros_norm
1124 #print axioms Komorebi.PaperIV.cosineNearestZeros_root
1125 #print axioms Komorebi.PaperIV.cosineNearestZeros_simple
1126 #print axioms Komorebi.PaperIV.cosine_nearest_zero_exhaustion
1127 #print axioms Komorebi.PaperIV.secant_leading_coefficient
1128 #print axioms Komorebi.PaperIV.secant_coefficient_error
1129 #print axioms Komorebi.PaperIV.secantMainTerm
1130 #print axioms Komorebi.PaperIV.secantMainTerm_norm
1131 #print axioms Komorebi.PaperIV.secantMainTerm_ne_zero
1132 #print axioms Komorebi.PaperIV.secant_relative_error
1133 #print axioms Komorebi.PaperIV.secant_coefficient_ratio_limit
1134 #print axioms Komorebi.PaperIV.secant_coefficient_asymptotic
1135 #print axioms Komorebi.PaperIV.pointwiseRootAverage
1136 #print axioms Komorebi.PaperIV.root_weight_sum
1137 #print axioms Komorebi.PaperIV.mapsTo_root_pow
1138 #print axioms Komorebi.PaperIV.pointwiseRootAverage_covariant
1139 #print axioms Komorebi.PaperIV.pointwiseRootAverage_of_covariant
1140 #print axioms Komorebi.PaperIV.pointwiseRootAverage_projector
1141 #print axioms Komorebi.PaperIV.pointwiseRootAverage_resolution
1142 #print axioms Komorebi.PaperIV.differentiableOn_pointwiseRootAverage
1143 #print axioms Komorebi.PaperIV.pointwiseRootAverage_range_iff
1144 #print axioms Komorebi.PaperIV.pointwiseRootAverage_sum
1145 #print axioms Komorebi.PaperIV.pointwiseRootAverage_product
1146 #print axioms Komorebi.PaperIV.pointwiseRootAverage_hasSum
1147 #print axioms Komorebi.PaperIV.pointwiseRootAverage_scaled_exp
1148 #print axioms Komorebi.PaperIV.entireTransfer_addition
1149 #print axioms Komorebi.PaperIV.signed_addition_weight
1150 #print axioms Komorebi.PaperIV.entireSigned_addition
1151 #print axioms Komorebi.PaperIV.IsLogarithmOn
1152 #print axioms Komorebi.PaperIV.logarithmPower
1153 #print axioms Komorebi.PaperIV.logarithmPower_add
1154 #print axioms Komorebi.PaperIV.IsLogarithmOn.nonzero
1155 #print axioms Komorebi.PaperIV.IsLogarithmOn.deriv
1156 #print axioms Komorebi.PaperIV.hasDerivAt_logarithmPower
1157 #print axioms Komorebi.PaperIV.reciprocal_fixed_log_derivative
1158 #print axioms Komorebi.PaperIV.analyticDifferentialBell
1159 #print axioms Komorebi.PaperIV.analyticOnNhd_differentialBell
1160 #print axioms Komorebi.PaperIV.iteratedDeriv_eq_analyticDifferentialBell
1161 #print axioms Komorebi.PaperIV.analytic_higher_riccati
1162 #print axioms Komorebi.PaperIV.truncatedDifferentialOperator_apply
1163 #print axioms Komorebi.PaperIV.truncatedDifferentialOperator_egfAction
1164 #print axioms Komorebi.PaperIV.residueAppell_operator_forward
1165 #print axioms Komorebi.PaperIV.residueAppell_operator_inverse
1166 #print axioms Komorebi.PaperIV.canonicalSignedDenominator_one
1167 #print axioms Komorebi.PaperIV.analyticTransferTangent_one
1168 #print axioms Komorebi.PaperIV.transferTangentCoeff_one_order
1169 #print axioms Komorebi.PaperIV.analyticTransferTangent_one_hasSum
1170 #print axioms Komorebi.PaperIV.analyticTransferTangent_hasSum_all_orders
1171 #print axioms Komorebi.PaperIV.reciprocalCoeff_two_compact
1172 #print axioms Komorebi.PaperIV.reciprocalCoeff_three_compact
1173 #print axioms Komorebi.PaperIV.newtonHessenberg
1174 #print axioms Komorebi.PaperIV.newtonHessenberg_det
1175 #print axioms Komorebi.PaperIV.reciprocalOrdCoeff_newton_determinant
1176 #print axioms Komorebi.PaperIV.residueHypergeometricParameters
1177 #print axioms Komorebi.PaperIV.residueHypergeometricParameters_card
1178 #print axioms Komorebi.PaperIV.residueHypergeometricParameters_re_pos
1179 #print axioms Komorebi.PaperIV.regularized_zeroF_normalization
1180 #print axioms Komorebi.PaperIV.residueHypergeometric
1181 #print axioms Komorebi.PaperIV.residueHypergeometric_hasSum
1182 #print axioms Komorebi.PaperIV.entireTransfer_hypergeometric
1183 #print axioms Komorebi.PaperIV.finiteAlgebraExponential
1184 #print axioms Komorebi.PaperIV.hasSum_cyclicAlgebra_exponential
1185 #print axioms Komorebi.PaperIV.hasSum_signedAlgebra_exponential
1186 #print axioms Komorebi.PaperIV.cyclicAlgebraNormedAddCommGroup
1187 #print axioms Komorebi.PaperIV.cyclicAlgebraNormedSpace
1188 #print axioms Komorebi.PaperIV.signedAlgebraNormedAddCommGroup
1189 #print axioms Komorebi.PaperIV.signedAlgebraNormedSpace
1190 #print axioms Komorebi.PaperIV.cyclicAlgebra_pointwise_exponential
1191 #print axioms Komorebi.PaperIV.signedAlgebra_pointwise_exponential
1192 open Lean Meta Elab Command
1193 
1194 run_cmd do
1195   let env ← getEnv
1196   let mut audited : Nat := 0
1197   let mut theorems : Nat := 0
1198   for (name, info) in env.checked.get.constants.toList do
1199     if Name.isPrefixOf `Komorebi.PaperIV name then
1200       audited := audited + 1
1201       match info with
1202       | .thmInfo _ => theorems := theorems + 1
1203       | _ => pure ()
1204       if info.isUnsafe then
1205         throwError "unsafe Paper IV declaration: {name}"
1206       match info with
1207       | .axiomInfo _ =>
1208           throwError "Paper IV axiom declaration: {name}"
1209       | .opaqueInfo _ =>
1210           throwError "opaque Paper IV declaration: {name}"
1211       | _ => pure ()
1212       let axioms ← Lean.collectAxioms name
1213       for axiomName in axioms do
1214         unless axiomName == ``propext || axiomName == ``Classical.choice ||
1215             axiomName == ``Quot.sound do
1216           throwError "unexpected axiom {axiomName} in Paper IV declaration {name}"
1217   if audited != 2234 then
1218     throwError "Paper IV namespace declaration count changed: expected 2234, found {audited}"
1219   if theorems != 1999 then
1220     throwError "Paper IV namespace theorem count changed: expected 1999, found {theorems}"
1221   logInfo m!"FAIL-CLOSED PAPER IV v1.0.0 KERNEL AUDIT PASS: {audited} declarations ({theorems} theoremInfo); 1164 explicit mapped targets; allowed axioms only: propext, Classical.choice, Quot.sound"

Back to source controls