ExactPeriodControls.lean

1 module
2 public import DyadicFourLeastPeriods
3 @[expose] public section
4 set_option autoImplicit false
5 namespace KomorebiPaperIX.ExactPeriodControls
6 open Congruential GlobalEulerBoundary DyadicFourLeastPeriods
7 
8 /-- The second higher address is constant modulo32 at every row. -/
9 theorem address_two_mod32 (n : ℕ) :
10     precision 2 5 (unnormalized 4 2 (n + 1) - unnormalized 4 2 n) := by
11   apply (precision_iff_dvd 2 5 n 1 (by decide) (by decide)).mpr
12   rw [originalBonus_values.2.2.1]
13   norm_num
14 
15 /-- At the next precision the least packet period is exactly two. -/
16 theorem address_two_mod64_least :
17     IsLeast {T : ℕ | ExactPeriodClassification.IsPeriod 2 (unnormalized 4 2) 6 T} 2 := by
18   have h := least_packet_period 2 6 (by decide)
19   rw [originalBonus_values.2.2.1] at h
20   norm_num at h
21   exact h
22 
23 /-- Constancy modulo32 does not extend to constancy modulo64. -/
24 theorem address_two_period_one_fails_mod64 :
25     ¬ ExactPeriodClassification.IsPeriod 2 (unnormalized 4 2) 6 1 := by
26   rw [period_iff_dvd 2 6 1 (by decide), originalBonus_values.2.2.1]
27   norm_num
28 
29 /-- The other higher address has least period128 modulo1024. -/
30 theorem address_three_mod1024_least :
31     IsLeast {T : ℕ | ExactPeriodClassification.IsPeriod 2 (unnormalized 4 3) 10 T} 128 := by
32   have h := least_packet_period 3 10 (by decide)
33   rw [originalBonus_values.2.2.2] at h
34   norm_num at h
35   exact h
36 
37 /-- Odd multiples of the least period are covered by the complete classification. -/
38 theorem address_two_mod1024_period96 :
39     ExactPeriodClassification.IsPeriod 2 (unnormalized 4 2) 10 96 := by
40   apply (period_iff_dvd 2 10 96 (by decide)).mpr
41   rw [originalBonus_values.2.2.1]
42   norm_num
43 
44 /-- A positive shift never makes these original rational coefficient values equal. -/
45 theorem positive_shift_nonzero (j n T : ℕ) (hj : j < 4) (hT : 0 < T) :
46     unnormalized 4 j (n + T) ≠ unnormalized 4 j n := by
47   exact sub_ne_zero.mp (exact_displacement j n T hj hT).1
48 
49 end KomorebiPaperIX.ExactPeriodControls

Back to source controls