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/provenance/exact_period_verification/ContinuationAxiomAudit.lean210 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/strengthening/provenance/exact_period_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 @[expose] public section
19 #print axioms KomorebiPaperIX.AllResidueStepAmplification.normalized_precision
20 #print axioms KomorebiPaperIX.AllResidueStepAmplification.unnormalized_bound
21 #print axioms KomorebiPaperIX.AllResidueStepAmplification.unnormalized_precision
22 #print axioms KomorebiPaperIX.AllRowsControls.zero_step_every_order
23 #print axioms KomorebiPaperIX.AllRowsControls.zeroth_row_every_order
24 #print axioms KomorebiPaperIX.AllRowsControls.zeroth_row_every_step
25 #print axioms KomorebiPaperIX.ChargedDworkClosure.B
26 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_charge_shift
27 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_deriv
28 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_mul
29 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_zero_one
30 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded
31 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_add
32 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_charge_shift
33 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_deriv
34 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_inverse
35 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_middle
36 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_mono
37 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_mul
38 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_nat_mul
39 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_neg
40 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_sub
41 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_succ
42 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_sum
43 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_zero
44 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat
45 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat_charge_shift
46 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat_inverse
47 #print axioms KomorebiPaperIX.ChargedDworkClosure.inverse_defect
48 #print axioms KomorebiPaperIX.ChargedDworkClosure.iterate_B_deriv
49 #print axioms KomorebiPaperIX.DyadicFourAllRows.B
50 #print axioms KomorebiPaperIX.DyadicFourAllRows.CoeffFlat
51 #print axioms KomorebiPaperIX.DyadicFourAllRows.Flat
52 #print axioms KomorebiPaperIX.DyadicFourAllRows.actual_packet_flat
53 #print axioms KomorebiPaperIX.DyadicFourAllRows.base_step_bound
54 #print axioms KomorebiPaperIX.DyadicFourAllRows.decode_B
55 #print axioms KomorebiPaperIX.DyadicFourAllRows.decode_B_iter
56 #print axioms KomorebiPaperIX.DyadicFourAllRows.difference_coe
57 #print axioms KomorebiPaperIX.DyadicFourAllRows.flat_encode_iff
58 #print axioms KomorebiPaperIX.DyadicFourAllRows.flat_reciprocal
59 #print axioms KomorebiPaperIX.DyadicFourAllRows.lifted_flat
60 #print axioms KomorebiPaperIX.DyadicFourAllRows.normalized_bound
61 #print axioms KomorebiPaperIX.DyadicFourAllRows.normalized_precision
62 #print axioms KomorebiPaperIX.DyadicFourAllRows.packed_difference_support
63 #print axioms KomorebiPaperIX.DyadicFourAllRows.packed_flat_of_kummer
64 #print axioms KomorebiPaperIX.DyadicFourAllRows.source_flat
65 #print axioms KomorebiPaperIX.DyadicFourAllRows.unnormalized_bound
66 #print axioms KomorebiPaperIX.DyadicFourAllRows.unnormalized_precision
67 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period
68 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period_degree
69 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period_precision
70 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period
71 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period_degree
72 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period_precision
73 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_period
74 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_step_bound
75 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_step_precision
76 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.unnormalized_step_bound
77 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.unnormalized_step_precision
78 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.exact_displacement
79 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.least_packet_period
80 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.normalized_exact_displacement
81 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.originalBonus
82 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.originalBonus_values
83 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.original_degree_exact_displacement
84 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.period_iff_dvd
85 #print axioms KomorebiPaperIX.DyadicFourLeastPeriods.precision_iff_dvd
86 #print axioms KomorebiPaperIX.DyadicFourPrefix.bonus
87 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_0_1
88 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_0_2
89 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_1_1
90 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_1_2
91 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_1
92 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_2
93 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_3
94 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_4
95 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_5
96 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_2_6
97 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_3_1
98 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_3_2
99 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_3_3
100 #print axioms KomorebiPaperIX.DyadicFourPrefix.coeff_3_4
101 #print axioms KomorebiPaperIX.DyadicFourPrefix.first_nonzero
102 #print axioms KomorebiPaperIX.DyadicFourPrefix.first_valuation
103 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahlerCoeff
104 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_0_1
105 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_0_2
106 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_1_1
107 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_1_2
108 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_1
109 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_2
110 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_3
111 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_4
112 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_5
113 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_2_6
114 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_3_1
115 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_3_2
116 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_3_3
117 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_3_4
118 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_0_1
119 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_0_2
120 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_1_1
121 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_1_2
122 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_1
123 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_2
124 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_3
125 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_4
126 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_5
127 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_2_6
128 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_3_1
129 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_3_2
130 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_3_3
131 #print axioms KomorebiPaperIX.DyadicFourPrefix.mahler_valuation_3_4
132 #print axioms KomorebiPaperIX.DyadicFourPrefix.precision_of_order_le
133 #print axioms KomorebiPaperIX.DyadicFourPrefix.tail_precision
134 #print axioms KomorebiPaperIX.DyadicFourPrefix.valuation_two_power_odd
135 #print axioms KomorebiPaperIX.DyadicFourSharpening.all_rows_even
136 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_difference_bound
137 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_difference_precision
138 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_even
139 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period
140 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period_degree
141 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period_precision
142 #print axioms KomorebiPaperIX.DyadicFourSharpening.normalized_period
143 #print axioms KomorebiPaperIX.DyadicFourSharpening.unnormalized_difference_factorial
144 #print axioms KomorebiPaperIX.DyadicLogThresholds.five_add_log_le
145 #print axioms KomorebiPaperIX.DyadicLogThresholds.log_two_succ_le
146 #print axioms KomorebiPaperIX.DyadicLogThresholds.offset_log_bound_of_le
147 #print axioms KomorebiPaperIX.DyadicLogThresholds.three_add_log_le
148 #print axioms KomorebiPaperIX.DyadicLogThresholds.two_add_log_le
149 #print axioms KomorebiPaperIX.DyadicSharpTower.bernoulli_dyadic_valuation
150 #print axioms KomorebiPaperIX.DyadicSharpTower.bernoulli_even_nonzero
151 #print axioms KomorebiPaperIX.DyadicSharpTower.beta_bernoulli
152 #print axioms KomorebiPaperIX.DyadicSharpTower.cosh_derivative
153 #print axioms KomorebiPaperIX.DyadicSharpTower.cothNormalized
154 #print axioms KomorebiPaperIX.DyadicSharpTower.coth_times_sinh
155 #print axioms KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_row_weight
156 #print axioms KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_sharp
157 #print axioms KomorebiPaperIX.DyadicSharpTower.expAt_derivative
158 #print axioms KomorebiPaperIX.DyadicSharpTower.first_omitted_error
159 #print axioms KomorebiPaperIX.DyadicSharpTower.first_omitted_error_valuation
160 #print axioms KomorebiPaperIX.DyadicSharpTower.hyperbolic_identity
161 #print axioms KomorebiPaperIX.DyadicSharpTower.inverse_eq_coth_derivative
162 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa
163 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic
164 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_coe
165 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_divisible
166 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_norm
167 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_bernoulli
168 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_nonzero
169 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_valuation
170 #print axioms KomorebiPaperIX.DyadicSharpTower.odd_factor_valuation
171 #print axioms KomorebiPaperIX.DyadicSharpTower.sinh_derivative
172 #print axioms KomorebiPaperIX.DyadicSharpTower.summandPadic_divisible
173 #print axioms KomorebiPaperIX.DyadicSharpTower.summandPadic_kappa
174 #print axioms KomorebiPaperIX.DyadicSharpTower.summand_kappa
175 #print axioms KomorebiPaperIX.DyadicSharpTower.summand_valuation
176 #print axioms KomorebiPaperIX.DyadicStepAmplification.normalized_bound
177 #print axioms KomorebiPaperIX.DyadicStepAmplification.normalized_precision
178 #print axioms KomorebiPaperIX.DyadicStepAmplification.prime_power_step_bound
179 #print axioms KomorebiPaperIX.DyadicStepAmplification.unnormalized_factorial_bound
180 #print axioms KomorebiPaperIX.DyadicStepAmplification.unnormalized_factorial_precision
181 #print axioms KomorebiPaperIX.ExactPeriodClassification.IsPeriod
182 #print axioms KomorebiPaperIX.ExactPeriodClassification.isPeriod_iff_dvd
183 #print axioms KomorebiPaperIX.ExactPeriodClassification.least_period
184 #print axioms KomorebiPaperIX.ExactPeriodClassification.precision_iff_dvd
185 #print axioms KomorebiPaperIX.ExactPeriodControls.address_three_mod1024_least
186 #print axioms KomorebiPaperIX.ExactPeriodControls.address_two_mod1024_period96
187 #print axioms KomorebiPaperIX.ExactPeriodControls.address_two_mod32
188 #print axioms KomorebiPaperIX.ExactPeriodControls.address_two_mod64_least
189 #print axioms KomorebiPaperIX.ExactPeriodControls.address_two_period_one_fails_mod64
190 #print axioms KomorebiPaperIX.ExactPeriodControls.positive_shift_nonzero
191 #print axioms KomorebiPaperIX.NewtonDominance.choose_precision
192 #print axioms KomorebiPaperIX.NewtonDominance.displacement_expansion
193 #print axioms KomorebiPaperIX.NewtonDominance.exact_displacement
194 #print axioms KomorebiPaperIX.NewtonDominance.first_difference_tail
195 #print axioms KomorebiPaperIX.NewtonDominance.precision_add
196 #print axioms KomorebiPaperIX.NewtonDominance.precision_mono
197 #print axioms KomorebiPaperIX.NewtonDominance.precision_mul
198 #print axioms KomorebiPaperIX.NewtonDominance.precision_mul_nat
199 #print axioms KomorebiPaperIX.NewtonDominance.precision_sum
200 #print axioms KomorebiPaperIX.NewtonDominance.strict_dominance
201 #print axioms KomorebiPaperIX.NewtonDominance.translated_tail
202 #print axioms KomorebiPaperIX.StepAmplification.binomial_step_precision
203 #print axioms KomorebiPaperIX.StepAmplification.difference_compose
204 #print axioms KomorebiPaperIX.StepAmplification.offset_displacement
205 #print axioms KomorebiPaperIX.StepAmplification.repeated_offset
206 #print axioms KomorebiPaperIX.StepAmplification.repeated_precision
207 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_first_difference
208 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_first_difference_valuation
209 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_second_coefficient
210 #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: 25aea2b581e1e44d3b44cc9279ef6b5ec37b1f3d1da308be114f0b27ab8146ab
Original source on GitHub
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation