ExactPeriodStatementContract.lean

1 module
2 public import DyadicFourLeastPeriods
3 @[expose] public section
4 set_option autoImplicit false
5 open KomorebiPaperIX
6 
7 example (j n T : ℕ) (hj : j < 4) (hT : 0 < T) :
8     Congruential.unnormalized 4 j (n + T) - Congruential.unnormalized 4 j n ≠ 0 ∧
9     padicValRat 2 (Congruential.unnormalized 4 j (n + T) - Congruential.unnormalized 4 j n) =
10       (padicValNat 2 T : ℤ) + (DyadicFourLeastPeriods.originalBonus j : ℤ) :=
11   DyadicFourLeastPeriods.exact_displacement j n T hj hT
12 
13 example (j r T : ℕ) (hj : j < 4) :
14     (0 < T ∧ ∀ n, GlobalEulerBoundary.precision 2 (r : ℤ)
15       (Congruential.unnormalized 4 j (n + T) - Congruential.unnormalized 4 j n)) ↔
16     0 < T ∧ 2 ^ (r - DyadicFourLeastPeriods.originalBonus j) ∣ T :=
17   DyadicFourLeastPeriods.period_iff_dvd j r T hj
18 
19 example (j r : ℕ) (hj : j < 4) :
20     IsLeast {T : ℕ | 0 < T ∧ ∀ n, GlobalEulerBoundary.precision 2 (r : ℤ)
21       (Congruential.unnormalized 4 j (n + T) - Congruential.unnormalized 4 j n)}
22       (2 ^ (r - DyadicFourLeastPeriods.originalBonus j)) :=
23   DyadicFourLeastPeriods.least_packet_period j r hj
24 
25 example : DyadicFourLeastPeriods.originalBonus 0 = 1 ∧
26     DyadicFourLeastPeriods.originalBonus 1 = 1 ∧
27     DyadicFourLeastPeriods.originalBonus 2 = 5 ∧
28     DyadicFourLeastPeriods.originalBonus 3 = 3 :=
29   DyadicFourLeastPeriods.originalBonus_values

Back to source controls