Mathematics · proofs · software

Paper IX · Lean source

AllRowsAxioms.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.

historical/development_audit_drivers/strengthening/AllRowsAxioms.lean46 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/historical/development_audit_drivers/strengthening/AllRowsAxioms.lean

Skip source text

1 module
2 public import ChargedDworkClosure
3 public import DyadicFourAllRows
4 @[expose] public section
5 #print axioms KomorebiPaperIX.ChargedDworkClosure.B
6 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_deriv
7 #print axioms KomorebiPaperIX.ChargedDworkClosure.iterate_B_deriv
8 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_mul
9 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_zero_one
10 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded
11 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat
12 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_zero
13 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_mono
14 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_succ
15 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_add
16 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_neg
17 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_sub
18 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_nat_mul
19 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_sum
20 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_deriv
21 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_middle
22 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_mul
23 #print axioms KomorebiPaperIX.ChargedDworkClosure.inverse_defect
24 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_inverse
25 #print axioms KomorebiPaperIX.ChargedDworkClosure.B_charge_shift
26 #print axioms KomorebiPaperIX.ChargedDworkClosure.bounded_charge_shift
27 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat_inverse
28 #print axioms KomorebiPaperIX.ChargedDworkClosure.flat_charge_shift
29 #print axioms KomorebiPaperIX.DyadicFourAllRows.B
30 #print axioms KomorebiPaperIX.DyadicFourAllRows.Flat
31 #print axioms KomorebiPaperIX.DyadicFourAllRows.CoeffFlat
32 #print axioms KomorebiPaperIX.DyadicFourAllRows.decode_B
33 #print axioms KomorebiPaperIX.DyadicFourAllRows.decode_B_iter
34 #print axioms KomorebiPaperIX.DyadicFourAllRows.difference_coe
35 #print axioms KomorebiPaperIX.DyadicFourAllRows.flat_encode_iff
36 #print axioms KomorebiPaperIX.DyadicFourAllRows.packed_difference_support
37 #print axioms KomorebiPaperIX.DyadicFourAllRows.packed_flat_of_kummer
38 #print axioms KomorebiPaperIX.DyadicFourAllRows.source_flat
39 #print axioms KomorebiPaperIX.DyadicFourAllRows.flat_reciprocal
40 #print axioms KomorebiPaperIX.DyadicFourAllRows.actual_packet_flat
41 #print axioms KomorebiPaperIX.DyadicFourAllRows.lifted_flat
42 #print axioms KomorebiPaperIX.DyadicFourAllRows.base_step_bound
43 #print axioms KomorebiPaperIX.DyadicFourAllRows.normalized_bound
44 #print axioms KomorebiPaperIX.DyadicFourAllRows.normalized_precision
45 #print axioms KomorebiPaperIX.DyadicFourAllRows.unnormalized_bound
46 #print axioms KomorebiPaperIX.DyadicFourAllRows.unnormalized_precision

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: b6bd477f90d3ebdbb4dda7983d6bfb4e8a1f7a9561e734b8453749a88239c49f

Original source on GitHub

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