Paper IX · Lean source
InvalidWeightedExtraPrecision.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_prescribed/controls/InvalidWeightedExtraPrecision.lean9 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/polynomial_prescribed/controls/InvalidWeightedExtraPrecision.lean1 module
2 public import PolynomialWeightedControls
3 @[expose] public section
4 open Komorebi.PolynomialWeightedControls
5
6 -- Invalid: the exact shifted root of 2X + 8 is -4, with depth two.
7 -- The weighted estimate r-s = 3-1 = 2 cannot uniformly gain another digit.
8 example : (2 : ℤ_[2]) ^ (3 - 1 + 1) ∣ -(2 : ℤ_[2]) ^ (3 - 1) := by
9 exact (linear_displacement_sharp 2 1 3).2
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: 803ca08f93df86615be8448a64eab3a99fa9580f707cd69363b026d4893ce458
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation