Mathematics · proofs · software

Paper IX · Lean source

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

polynomial_lifting/development/taylor/TaylorAudit.lean21 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/polynomial_lifting/development/taylor/TaylorAudit.lean

Skip source text

1 module
2 public import PolynomialTaylor
3 @[expose] public section
4 
5 #print axioms Komorebi.PolynomialTaylor.directional
6 #print axioms Komorebi.PolynomialTaylor.directional_C
7 #print axioms Komorebi.PolynomialTaylor.directional_add
8 #print axioms Komorebi.PolynomialTaylor.directional_mul
9 #print axioms Komorebi.PolynomialTaylor.directional_X
10 #print axioms Komorebi.PolynomialTaylor.taylor_dvd
11 #print axioms Komorebi.PolynomialTaylor.taylor_step_dvd
12 #print axioms Komorebi.PolynomialTaylor.eval_dvd_of_dvd
13 #print axioms Komorebi.PolynomialTaylor.pderiv_eval_dvd_of_dvd
14 
15 open MvPolynomial Komorebi.PolynomialTaylor in
16 example (d : ℕ) (P : MvPolynomial (Fin d) ℤ) (x t : Fin d → ℤ)
17     (q L : ℕ) (hL : 1 ≤ L) :
18     (q : ℤ) ^ (L + 1) ∣
19       eval (fun i => x i + (q : ℤ) ^ L * t i) P - eval x P -
20         (q : ℤ) ^ L * (∑ i, eval x (pderiv i P) * t i) :=
21   taylor_step_dvd P x t q L hL

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: 620f4fe2d674a88655147e94ae40a75f69dea90cde08a34e4725749855e895f7

Original source on GitHub

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