Mathematics · proofs · software

Paper IX · Lean source

NewtonDominanceAudit.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/least_periods/NewtonDominanceAudit.lean14 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/historical/development_audit_drivers/least_periods/NewtonDominanceAudit.lean

Skip source text

1 module
2 public import NewtonDominance
3 
4 #print axioms KomorebiPaperIX.NewtonDominance.precision_mono
5 #print axioms KomorebiPaperIX.NewtonDominance.precision_add
6 #print axioms KomorebiPaperIX.NewtonDominance.precision_sum
7 #print axioms KomorebiPaperIX.NewtonDominance.precision_mul
8 #print axioms KomorebiPaperIX.NewtonDominance.precision_mul_nat
9 #print axioms KomorebiPaperIX.NewtonDominance.strict_dominance
10 #print axioms KomorebiPaperIX.NewtonDominance.translated_tail
11 #print axioms KomorebiPaperIX.NewtonDominance.first_difference_tail
12 #print axioms KomorebiPaperIX.NewtonDominance.choose_precision
13 #print axioms KomorebiPaperIX.NewtonDominance.displacement_expansion
14 #print axioms KomorebiPaperIX.NewtonDominance.exact_displacement

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: 8dd2bd227135a0874ff75098cad36e839802247b199d575e3ee1c0a5303e9d59

Original source on GitHub

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