Paper IX · Lean source
NegativeExactExtraDigit.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.
strengthening/controls/NegativeExactExtraDigit.lean11 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/strengthening/controls/NegativeExactExtraDigit.lean1 module
2 public import DyadicFourLeastPeriods
3 @[expose] public section
4 set_option autoImplicit false
5 open KomorebiPaperIX
6 example : padicValRat 2
7 (Congruential.unnormalized 4 2 (0 + 1) - Congruential.unnormalized 4 2 0) = 6 := by
8 have h := (DyadicFourLeastPeriods.exact_displacement 2 0 1 (by decide) (by decide)).2
9 rw [DyadicFourLeastPeriods.originalBonus_values.2.2.1] at h
10 norm_num at h
11 exact h
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: 807a762b41f8aa8d3e53d4e7c6c639d018dd4b8fc3be8206719038f970eee644
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation