Paper IX · Lean source
AllRowsControls.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/formalization/AllRowsControls.lean26 lines
Original source path
preserved/PRSC_IX_Consolidated_Manuscript/strengthening/formalization/AllRowsControls.leanSkip declarations and read code
1 module
2 public import DyadicFourAllRows
3 @[expose] public section
4 noncomputable section
5 set_option autoImplicit false
6 namespace KomorebiPaperIX.AllRowsControls
7 open Mahler DyadicFourCongruences
8
9 theorem zeroth_row_every_order (k : ℕ) :
10 (2:ℤ_[2])^k ∣ difference 1 k (normalizedLift 0 (by decide)) 0 :=
11 DyadicFourAllRows.base_step_bound 0 k 0 (by decide)
12
13 theorem zeroth_row_every_step (u k : ℕ) :
14 GlobalEulerBoundary.precision 2 (k:ℤ)
15 (difference u k (Congruential.unnormalized 4 3) 0) :=
16 DyadicFourAllRows.unnormalized_precision 3 u k 0 (by decide)
17
18 theorem zero_step_every_order (j k n : ℕ) (hj : j<4) :
19 GlobalEulerBoundary.precision 2 (k:ℤ)
20 (difference 0 k (Congruential.coeff 4 j) n) :=
21 DyadicFourAllRows.normalized_precision j 0 k n hj
22
23 #print axioms zeroth_row_every_order
24 #print axioms zeroth_row_every_step
25 #print axioms zero_step_every_order
26 end KomorebiPaperIX.AllRowsControls
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: 5c0b80c3b45af5cd396e18b76235aa069f5ce7aaf4fa638fd428636955fe2031
Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation