Paper IX · Lean source
InvalidPerturbationExtraPrecision.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_motion/controls/InvalidPerturbationExtraPrecision.lean11 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/polynomial_motion/controls/InvalidPerturbationExtraPrecision.lean1 module
2 public import PolynomialDeformationControls
3 @[expose] public section
4 open Komorebi.PolynomialDeformationControls MvPolynomial
5
6 -- Invalid: G=X−2 is an integral coefficient perturbation of F=X of precision one.
7 -- Its actual p-adic root has displacement two, which does not have precision two.
8 example : ∃ b : Fin 1 → ℤ_[2],
9 eval₂ (Int.castRingHom ℤ_[2]) b (Komorebi.PolynomialTowerControls.linearMinusTwo 0) = 0 ∧
10 (2 : ℤ_[2]) ^ 2 ∣ b 0 := by
11 exact linear_shift_no_extra_padic_precision
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: 4923d405f190856f3e193f2b76e4013f40f0c802502e5e6d998f737ab5790ab0
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation