Paper IX · Lean source
PolynomialTaylorContract.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/contracts/PolynomialTaylorContract.lean18 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/polynomial_lifting/contracts/PolynomialTaylorContract.leanSkip declarations and read code
1 module
2 public import PolynomialTaylor
3
4 @[expose] public section
5 set_option autoImplicit false
6
7 namespace Komorebi.PolynomialTaylorContract
8
9 /-- The source polynomial, actual partial derivatives, all integer shifts,
10 and a divisible quadratic remainder appear explicitly in the contract. -/
11 theorem explicit_integral_taylor_contract (d : ℕ)
12 (P : MvPolynomial (Fin d) ℤ) (x t : Fin d → ℤ) (a : ℤ) :
13 a ^ 2 ∣ MvPolynomial.eval (fun i => x i + a * t i) P -
14 MvPolynomial.eval x P -
15 a * ∑ i, MvPolynomial.eval x (MvPolynomial.pderiv i P) * t i :=
16 PolynomialTaylor.taylor_dvd P x t a
17
18 end Komorebi.PolynomialTaylorContract
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: d6bba92070ef41f5fe3da87b040eb0caf78f73120cfb322302981d158ce1fc69
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation