Paper IX · Lean source
InvalidMotionExtraErrorDigit.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/InvalidMotionExtraErrorDigit.lean10 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/polynomial_prescribed/controls/InvalidMotionExtraErrorDigit.lean1 module
2 public import PolynomialMotionControls
3 @[expose] public section
4 open Komorebi.PolynomialMotionControls
5
6 -- Invalid: for F=X+X^2, H=1, p=2, s=0, M=1, the root exists in 2 Z_2,
7 -- and its first-order error b+2 has exactly depth two, not depth three.
8 example : ∀ b : ℤ_[2], b + b ^ 2 + 2 = 0 → (2 : ℤ_[2]) ∣ b →
9 (2 : ℤ_[2]) ^ 3 ∣ b + 2 := by
10 exact no_uniform_extra_error_digit
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: af20412a408a23d2328574f49816535d4091102ba3b5fdcaee6953a7f898c491
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation