Paper IX · Lean source
ContinuationAxiomAudit.lean

Selected results recorded Coverage and evidence
Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
strengthening/verification/ContinuationAxiomAudit.lean270 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/strengthening/verification/ContinuationAxiomAudit.lean
1 module
2 public import StepAmplification
3 public import DyadicStepAmplification
4 public import AllResidueStepAmplification
5 public import StepAmplificationExamples
6 public import DyadicSharpTower
7 public import ChargedDworkClosure
8 public import DyadicFourAllRows
9 public import AllRowsControls
10 public import DyadicFourSharpening
11 public import DyadicFourFinalStrengthening
12 public import DyadicLogThresholds
13 public import NewtonDominance
14 public import DyadicFourPrefix
15 public import ExactPeriodClassification
16 public import DyadicFourLeastPeriods
17 public import ExactPeriodControls
18 public import CompactSelfIsometry
19 public import DensePadicIsometry
20 public import RationalPadicEmbedding
21 public import DyadicPacketRational
22 public import DyadicFourIsometry
23 public import DyadicIsometryControls
24 @[expose] public section
25 #print axioms KomorebiPaperIX.AllResidueStepAmplification.normalized_precision
26 #print axioms KomorebiPaperIX.AllResidueStepAmplification.unnormalized_bound
27 #print axioms KomorebiPaperIX.AllResidueStepAmplification.unnormalized_precision
28 #print axioms KomorebiPaperIX.AllRowsControls.zero_step_every_order
29 #print axioms KomorebiPaperIX.AllRowsControls.zeroth_row_every_order
30 #print axioms KomorebiPaperIX.AllRowsControls.zeroth_row_every_step
31 #print axioms KomorebiPaperIX.ChargedDworkClosure.B
32 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_charge_shift
33 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_deriv
34 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_mul
35 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_zero_one
36 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded
37 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_add
38 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_charge_shift
39 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_deriv
40 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_inverse
41 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_middle
42 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_mono
43 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_mul
44 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_nat_mul
45 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_neg
46 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_sub
47 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_succ
48 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_sum
49 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_zero
50 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat
51 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat_charge_shift
52 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat_inverse
53 #print axioms KomorebiPaperIX.ChargedDworkClosure.inverse_defect
54 #print axioms KomorebiPaperIX.ChargedDworkClosure.iterate_B_deriv
55 #print axioms KomorebiPaperIX.CompactSelfIsometry.denseRange
56 #print axioms KomorebiPaperIX.CompactSelfIsometry.iterate_isometry
57 #print axioms KomorebiPaperIX.CompactSelfIsometry.surjective
58 #print axioms KomorebiPaperIX.DensePadicIsometry.existsUnique_extensionEquiv
59 #print axioms KomorebiPaperIX.DensePadicIsometry.extension
60 #print axioms KomorebiPaperIX.DensePadicIsometry.extensionEquiv
61 #print axioms KomorebiPaperIX.DensePadicIsometry.extensionEquiv_apply
62 #print axioms KomorebiPaperIX.DensePadicIsometry.extensionEquiv_nat
63 #print axioms KomorebiPaperIX.DensePadicIsometry.extensionEquiv_unique
64 #print axioms KomorebiPaperIX.DensePadicIsometry.extensionEquiv_unique_continuous
65 #print axioms KomorebiPaperIX.DensePadicIsometry.extension_continuous
66 #print axioms KomorebiPaperIX.DensePadicIsometry.extension_isometry
67 #print axioms KomorebiPaperIX.DensePadicIsometry.extension_nat
68 #print axioms KomorebiPaperIX.DensePadicIsometry.extension_surjective
69 #print axioms KomorebiPaperIX.DensePadicIsometry.extension_unique
70 #print axioms KomorebiPaperIX.DensePadicIsometry.onNaturalRange
71 #print axioms KomorebiPaperIX.DensePadicIsometry.onNaturalRange_isometry
72 #print axioms KomorebiPaperIX.DensePadicIsometry.onNaturalRange_nat
73 #print axioms KomorebiPaperIX.DyadicFourAllRows.B
74 #print axioms KomorebiPaperIX.DyadicFourAllRows.CoeffFlat
75 #print axioms KomorebiPaperIX.DyadicFourAllRows.Flat
76 #print axioms KomorebiPaperIX.DyadicFourAllRows.actual_packet_flat
77 #print axioms KomorebiPaperIX.DyadicFourAllRows.base_step_bound
78 #print axioms KomorebiPaperIX.DyadicFourAllRows.decode_B
79 #print axioms KomorebiPaperIX.DyadicFourAllRows.decode_B_iter
80 #print axioms KomorebiPaperIX.DyadicFourAllRows.difference_coe
81 #print axioms KomorebiPaperIX.DyadicFourAllRows.flat_encode_iff
82 #print axioms KomorebiPaperIX.DyadicFourAllRows.flat_reciprocal
83 #print axioms KomorebiPaperIX.DyadicFourAllRows.lifted_flat
84 #print axioms KomorebiPaperIX.DyadicFourAllRows.normalized_bound
85 #print axioms KomorebiPaperIX.DyadicFourAllRows.normalized_precision
86 #print axioms KomorebiPaperIX.DyadicFourAllRows.packed_difference_support
87 #print axioms KomorebiPaperIX.DyadicFourAllRows.packed_flat_of_kummer
88 #print axioms KomorebiPaperIX.DyadicFourAllRows.source_flat
89 #print axioms KomorebiPaperIX.DyadicFourAllRows.unnormalized_bound
90 #print axioms KomorebiPaperIX.DyadicFourAllRows.unnormalized_precision
91 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period
92 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period_degree
93 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period_precision
94 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period
95 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period_degree
96 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period_precision
97 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_period
98 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_step_bound
99 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_step_precision
100 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.unnormalized_step_bound
101 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.unnormalized_step_precision
102 #print axioms KomorebiPaperIX.DyadicFourIsometry.existsUnique_isometry
103 #print axioms KomorebiPaperIX.DyadicFourIsometry.isometry
104 #print axioms KomorebiPaperIX.DyadicFourIsometry.isometry_continuous
105 #print axioms KomorebiPaperIX.DyadicFourIsometry.isometry_dist
106 #print axioms KomorebiPaperIX.DyadicFourIsometry.isometry_nat
107 #print axioms KomorebiPaperIX.DyadicFourIsometry.isometry_surjective
108 #print axioms KomorebiPaperIX.DyadicFourIsometry.isometry_zero
109 #print axioms KomorebiPaperIX.DyadicFourIsometry.originalExtension
110 #print axioms KomorebiPaperIX.DyadicFourIsometry.originalExtension_continuous
111 #print axioms KomorebiPaperIX.DyadicFourIsometry.originalExtension_dist
112 #print axioms KomorebiPaperIX.DyadicFourIsometry.originalExtension_injective
113 #print axioms KomorebiPaperIX.DyadicFourIsometry.originalExtension_nat
114 #print axioms KomorebiPaperIX.DyadicFourIsometry.originalExtension_range
115 #print axioms KomorebiPaperIX.DyadicFourIsometry.samples
116 #print axioms KomorebiPaperIX.DyadicFourIsometry.samples_coe
117 #print axioms KomorebiPaperIX.DyadicFourIsometry.samples_dist
118 #print axioms KomorebiPaperIX.DyadicFourIsometry.unique_continuous
119 #print axioms KomorebiPaperIX.DyadicFourIsometry.unique_original_preimage
120 #print axioms KomorebiPaperIX.DyadicFourIsometry.unique_preimage
121 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.exact_displacement
122 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.least_packet_period
123 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.normalized_exact_displacement
124 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.originalBonus
125 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.originalBonus_values
126 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.original_degree_exact_displacement
127 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.period_iff_dvd
128 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.precision_iff_dvd
129 #print axioms KomorebiPaperIX.DyadicFourPrefix.bonus
130 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_0_1
131 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_0_2
132 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_1_1
133 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_1_2
134 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_1
135 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_2
136 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_3
137 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_4
138 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_5
139 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_6
140 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_3_1
141 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_3_2
142 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_3_3
143 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_3_4
144 #print axioms KomorebiPaperIX.DyadicFourPrefix.first_nonzero
145 #print axioms KomorebiPaperIX.DyadicFourPrefix.first_valuation
146 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahlerCoeff
147 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_0_1
148 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_0_2
149 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_1_1
150 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_1_2
151 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_1
152 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_2
153 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_3
154 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_4
155 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_5
156 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_6
157 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_3_1
158 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_3_2
159 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_3_3
160 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_3_4
161 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_0_1
162 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_0_2
163 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_1_1
164 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_1_2
165 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_1
166 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_2
167 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_3
168 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_4
169 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_5
170 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_6
171 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_3_1
172 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_3_2
173 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_3_3
174 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_3_4
175 #print axioms KomorebiPaperIX.DyadicFourPrefix.precision_of_order_le
176 #print axioms KomorebiPaperIX.DyadicFourPrefix.tail_precision
177 #print axioms KomorebiPaperIX.DyadicFourPrefix.valuation_two_power_odd
178 #print axioms KomorebiPaperIX.DyadicFourSharpening.all_rows_even
179 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_difference_bound
180 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_difference_precision
181 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_even
182 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period
183 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period_degree
184 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period_precision
185 #print axioms KomorebiPaperIX.DyadicFourSharpening.normalized_period
186 #print axioms KomorebiPaperIX.DyadicFourSharpening.unnormalized_difference_factorial
187 #print axioms KomorebiPaperIX.DyadicIsometryControls.address_zero_at_one
188 #print axioms KomorebiPaperIX.DyadicIsometryControls.address_zero_at_two
189 #print axioms KomorebiPaperIX.DyadicIsometryControls.address_zero_inverse_at_thirty_four
190 #print axioms KomorebiPaperIX.DyadicIsometryControls.address_zero_not_additive
191 #print axioms KomorebiPaperIX.DyadicIsometryControls.original_address_zero_ne_zero
192 #print axioms KomorebiPaperIX.DyadicIsometryControls.original_address_zero_not_surjective
193 #print axioms KomorebiPaperIX.DyadicLogThresholds.five_add_log_le
194 #print axioms KomorebiPaperIX.DyadicLogThresholds.log_two_succ_le
195 #print axioms KomorebiPaperIX.DyadicLogThresholds.offset_log_bound_of_le
196 #print axioms KomorebiPaperIX.DyadicLogThresholds.three_add_log_le
197 #print axioms KomorebiPaperIX.DyadicLogThresholds.two_add_log_le
198 #print axioms KomorebiPaperIX.DyadicPacketRational.exact_displacement
199 #print axioms KomorebiPaperIX.DyadicPacketRational.norm_displacement
200 #print axioms KomorebiPaperIX.DyadicPacketRational.norm_le_one
201 #print axioms KomorebiPaperIX.DyadicPacketRational.norm_sub
202 #print axioms KomorebiPaperIX.DyadicPacketRational.packet
203 #print axioms KomorebiPaperIX.DyadicPacketRational.packet_sub
204 #print axioms KomorebiPaperIX.DyadicPacketRational.packet_zero
205 #print axioms KomorebiPaperIX.DyadicSharpTower.bernoulli_dyadic_valuation
206 #print axioms KomorebiPaperIX.DyadicSharpTower.bernoulli_even_nonzero
207 #print axioms KomorebiPaperIX.DyadicSharpTower.beta_bernoulli
208 #print axioms KomorebiPaperIX.DyadicSharpTower.cosh_derivative
209 #print axioms KomorebiPaperIX.DyadicSharpTower.cothNormalized
210 #print axioms KomorebiPaperIX.DyadicSharpTower.coth_times_sinh
211 #print axioms KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_row_weight
212 #print axioms KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_sharp
213 #print axioms KomorebiPaperIX.DyadicSharpTower.expAt_derivative
214 #print axioms KomorebiPaperIX.DyadicSharpTower.first_omitted_error
215 #print axioms KomorebiPaperIX.DyadicSharpTower.first_omitted_error_valuation
216 #print axioms KomorebiPaperIX.DyadicSharpTower.hyperbolic_identity
217 #print axioms KomorebiPaperIX.DyadicSharpTower.inverse_eq_coth_derivative
218 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa
219 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic
220 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_coe
221 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_divisible
222 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_norm
223 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_bernoulli
224 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_nonzero
225 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_valuation
226 #print axioms KomorebiPaperIX.DyadicSharpTower.odd_factor_valuation
227 #print axioms KomorebiPaperIX.DyadicSharpTower.sinh_derivative
228 #print axioms KomorebiPaperIX.DyadicSharpTower.summandPadic_divisible
229 #print axioms KomorebiPaperIX.DyadicSharpTower.summandPadic_kappa
230 #print axioms KomorebiPaperIX.DyadicSharpTower.summand_kappa
231 #print axioms KomorebiPaperIX.DyadicSharpTower.summand_valuation
232 #print axioms KomorebiPaperIX.DyadicStepAmplification.normalized_bound
233 #print axioms KomorebiPaperIX.DyadicStepAmplification.normalized_precision
234 #print axioms KomorebiPaperIX.DyadicStepAmplification.prime_power_step_bound
235 #print axioms KomorebiPaperIX.DyadicStepAmplification.unnormalized_factorial_bound
236 #print axioms KomorebiPaperIX.DyadicStepAmplification.unnormalized_factorial_precision
237 #print axioms KomorebiPaperIX.ExactPeriodClassification.IsPeriod
238 #print axioms KomorebiPaperIX.ExactPeriodClassification.isPeriod_iff_dvd
239 #print axioms KomorebiPaperIX.ExactPeriodClassification.least_period
240 #print axioms KomorebiPaperIX.ExactPeriodClassification.precision_iff_dvd
241 #print axioms KomorebiPaperIX.ExactPeriodControls.address_three_mod1024_least
242 #print axioms KomorebiPaperIX.ExactPeriodControls.address_two_mod1024_period96
243 #print axioms KomorebiPaperIX.ExactPeriodControls.address_two_mod32
244 #print axioms KomorebiPaperIX.ExactPeriodControls.address_two_mod64_least
245 #print axioms KomorebiPaperIX.ExactPeriodControls.address_two_period_one_fails_mod64
246 #print axioms KomorebiPaperIX.ExactPeriodControls.positive_shift_nonzero
247 #print axioms KomorebiPaperIX.NewtonDominance.choose_precision
248 #print axioms KomorebiPaperIX.NewtonDominance.displacement_expansion
249 #print axioms KomorebiPaperIX.NewtonDominance.exact_displacement
250 #print axioms KomorebiPaperIX.NewtonDominance.first_difference_tail
251 #print axioms KomorebiPaperIX.NewtonDominance.precision_add
252 #print axioms KomorebiPaperIX.NewtonDominance.precision_mono
253 #print axioms KomorebiPaperIX.NewtonDominance.precision_mul
254 #print axioms KomorebiPaperIX.NewtonDominance.precision_mul_nat
255 #print axioms KomorebiPaperIX.NewtonDominance.precision_sum
256 #print axioms KomorebiPaperIX.NewtonDominance.strict_dominance
257 #print axioms KomorebiPaperIX.NewtonDominance.translated_tail
258 #print axioms KomorebiPaperIX.RationalPadicEmbedding.norm_le_one
259 #print axioms KomorebiPaperIX.RationalPadicEmbedding.samples
260 #print axioms KomorebiPaperIX.RationalPadicEmbedding.samples_coe
261 #print axioms KomorebiPaperIX.RationalPadicEmbedding.samples_dist
262 #print axioms KomorebiPaperIX.StepAmplification.binomial_step_precision
263 #print axioms KomorebiPaperIX.StepAmplification.difference_compose
264 #print axioms KomorebiPaperIX.StepAmplification.offset_displacement
265 #print axioms KomorebiPaperIX.StepAmplification.repeated_offset
266 #print axioms KomorebiPaperIX.StepAmplification.repeated_precision
267 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_first_difference
268 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_first_difference_valuation
269 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_second_coefficient
270 #print axioms KomorebiPaperIX.StepAmplificationExamples.no_uniform_extra_digit
Back to source controls
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 0a8c21c63cafd9003b5ff54e6291622b9a4fd552eeed08ea76796ec75ace8519
Original source on GitHub
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation