Mathematics · proofs · software

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/sharp_dyadic_verification/ContinuationAxiomAudit.lean121 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/strengthening/provenance/sharp_dyadic_verification/ContinuationAxiomAudit.lean

Skip source text

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 @[expose] public section
13 #print axioms KomorebiPaperIX.AllResidueStepAmplification.normalized_precision
14 #print axioms KomorebiPaperIX.AllResidueStepAmplification.unnormalized_bound
15 #print axioms KomorebiPaperIX.AllResidueStepAmplification.unnormalized_precision
16 #print axioms KomorebiPaperIX.AllRowsControls.zero_step_every_order
17 #print axioms KomorebiPaperIX.AllRowsControls.zeroth_row_every_order
18 #print axioms KomorebiPaperIX.AllRowsControls.zeroth_row_every_step
19 #print axioms KomorebiPaperIX.ChargedDworkClosure.B
20 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_charge_shift
21 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_deriv
22 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_mul
23 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_zero_one
24 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded
25 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_add
26 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_charge_shift
27 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_deriv
28 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_inverse
29 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_middle
30 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_mono
31 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_mul
32 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_nat_mul
33 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_neg
34 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_sub
35 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_succ
36 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_sum
37 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_zero
38 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat
39 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat_charge_shift
40 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat_inverse
41 #print axioms KomorebiPaperIX.ChargedDworkClosure.inverse_defect
42 #print axioms KomorebiPaperIX.ChargedDworkClosure.iterate_B_deriv
43 #print axioms KomorebiPaperIX.DyadicFourAllRows.B
44 #print axioms KomorebiPaperIX.DyadicFourAllRows.CoeffFlat
45 #print axioms KomorebiPaperIX.DyadicFourAllRows.Flat
46 #print axioms KomorebiPaperIX.DyadicFourAllRows.actual_packet_flat
47 #print axioms KomorebiPaperIX.DyadicFourAllRows.base_step_bound
48 #print axioms KomorebiPaperIX.DyadicFourAllRows.decode_B
49 #print axioms KomorebiPaperIX.DyadicFourAllRows.decode_B_iter
50 #print axioms KomorebiPaperIX.DyadicFourAllRows.difference_coe
51 #print axioms KomorebiPaperIX.DyadicFourAllRows.flat_encode_iff
52 #print axioms KomorebiPaperIX.DyadicFourAllRows.flat_reciprocal
53 #print axioms KomorebiPaperIX.DyadicFourAllRows.lifted_flat
54 #print axioms KomorebiPaperIX.DyadicFourAllRows.normalized_bound
55 #print axioms KomorebiPaperIX.DyadicFourAllRows.normalized_precision
56 #print axioms KomorebiPaperIX.DyadicFourAllRows.packed_difference_support
57 #print axioms KomorebiPaperIX.DyadicFourAllRows.packed_flat_of_kummer
58 #print axioms KomorebiPaperIX.DyadicFourAllRows.source_flat
59 #print axioms KomorebiPaperIX.DyadicFourAllRows.unnormalized_bound
60 #print axioms KomorebiPaperIX.DyadicFourAllRows.unnormalized_precision
61 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period
62 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period_degree
63 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_half_period_precision
64 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period
65 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period_degree
66 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.all_rows_period_precision
67 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_period
68 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_step_bound
69 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.normalized_step_precision
70 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.unnormalized_step_bound
71 #print axioms KomorebiPaperIX.DyadicFourFinalStrengthening.unnormalized_step_precision
72 #print axioms KomorebiPaperIX.DyadicFourSharpening.all_rows_even
73 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_difference_bound
74 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_difference_precision
75 #print axioms KomorebiPaperIX.DyadicFourSharpening.factorial_even
76 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period
77 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period_degree
78 #print axioms KomorebiPaperIX.DyadicFourSharpening.half_period_precision
79 #print axioms KomorebiPaperIX.DyadicFourSharpening.normalized_period
80 #print axioms KomorebiPaperIX.DyadicFourSharpening.unnormalized_difference_factorial
81 #print axioms KomorebiPaperIX.DyadicSharpTower.bernoulli_dyadic_valuation
82 #print axioms KomorebiPaperIX.DyadicSharpTower.bernoulli_even_nonzero
83 #print axioms KomorebiPaperIX.DyadicSharpTower.beta_bernoulli
84 #print axioms KomorebiPaperIX.DyadicSharpTower.cosh_derivative
85 #print axioms KomorebiPaperIX.DyadicSharpTower.cothNormalized
86 #print axioms KomorebiPaperIX.DyadicSharpTower.coth_times_sinh
87 #print axioms KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_row_weight
88 #print axioms KomorebiPaperIX.DyadicSharpTower.dyadic_supercongruence_sharp
89 #print axioms KomorebiPaperIX.DyadicSharpTower.expAt_derivative
90 #print axioms KomorebiPaperIX.DyadicSharpTower.first_omitted_error
91 #print axioms KomorebiPaperIX.DyadicSharpTower.first_omitted_error_valuation
92 #print axioms KomorebiPaperIX.DyadicSharpTower.hyperbolic_identity
93 #print axioms KomorebiPaperIX.DyadicSharpTower.inverse_eq_coth_derivative
94 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa
95 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic
96 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_coe
97 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_divisible
98 #print axioms KomorebiPaperIX.DyadicSharpTower.kappaPadic_norm
99 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_bernoulli
100 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_nonzero
101 #print axioms KomorebiPaperIX.DyadicSharpTower.kappa_valuation
102 #print axioms KomorebiPaperIX.DyadicSharpTower.odd_factor_valuation
103 #print axioms KomorebiPaperIX.DyadicSharpTower.sinh_derivative
104 #print axioms KomorebiPaperIX.DyadicSharpTower.summandPadic_divisible
105 #print axioms KomorebiPaperIX.DyadicSharpTower.summandPadic_kappa
106 #print axioms KomorebiPaperIX.DyadicSharpTower.summand_kappa
107 #print axioms KomorebiPaperIX.DyadicSharpTower.summand_valuation
108 #print axioms KomorebiPaperIX.DyadicStepAmplification.normalized_bound
109 #print axioms KomorebiPaperIX.DyadicStepAmplification.normalized_precision
110 #print axioms KomorebiPaperIX.DyadicStepAmplification.prime_power_step_bound
111 #print axioms KomorebiPaperIX.DyadicStepAmplification.unnormalized_factorial_bound
112 #print axioms KomorebiPaperIX.DyadicStepAmplification.unnormalized_factorial_precision
113 #print axioms KomorebiPaperIX.StepAmplification.binomial_step_precision
114 #print axioms KomorebiPaperIX.StepAmplification.difference_compose
115 #print axioms KomorebiPaperIX.StepAmplification.offset_displacement
116 #print axioms KomorebiPaperIX.StepAmplification.repeated_offset
117 #print axioms KomorebiPaperIX.StepAmplification.repeated_precision
118 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_first_difference
119 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_first_difference_valuation
120 #print axioms KomorebiPaperIX.StepAmplificationExamples.actual_second_coefficient
121 #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: 1b36f3b9acce73cfd05a44b5f65f3cee29b3c6facd2efe338a6fa5f889f04303

Original source on GitHub

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation