DyadicFourLeastPeriods.lean

1 module
2 public import NewtonDominance
3 public import DyadicFourPrefix
4 public import ExactPeriodClassification
5 public import NishibuchiCompletion
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 namespace KomorebiPaperIX.DyadicFourLeastPeriods
10 open Mahler Congruential GlobalEulerBoundary
11 
12 /-- The original coefficients include the address factorial in their exact gain. -/
13 def originalBonus (j : ℕ) : ℕ :=
14   DyadicFourPrefix.bonus j + padicValNat 2 j.factorial
15 
16 theorem originalBonus_values :
17     originalBonus 0 = 1 ∧ originalBonus 1 = 1 ∧
18     originalBonus 2 = 5 ∧ originalBonus 3 = 3 := by
19   have h2 : padicValNat 2 2 = 1 := by
20     simp
21   have h6 : padicValNat 2 6 = 1 := by
22     simpa using DyadicFourPrefix.valuation_two_power_odd 1 3 (by norm_num)
23   norm_num [originalBonus, DyadicFourPrefix.bonus, h2, h6]
24 
25 /-- Exact valuation for every positive displacement and every normalized packet row. -/
26 theorem normalized_exact_displacement (j n T : ℕ) (hj : j < 4) (hT : 0 < T) :
27     coeff 4 j (n + T) - coeff 4 j n ≠ 0 ∧
28     padicValRat 2 (coeff 4 j (n + T) - coeff 4 j n) =
29       (padicValNat 2 T : ℤ) + (DyadicFourPrefix.bonus j : ℤ) := by
30   exact NewtonDominance.exact_displacement (coeff 4 j) (DyadicFourPrefix.bonus j)
31     (DyadicFourPrefix.first_nonzero j hj) (DyadicFourPrefix.first_valuation j hj)
32     (DyadicFourPrefix.tail_precision j hj) n T hT
33 
34 /-- Original, unnormalized coefficients: the gain is exactly 1,1,5,3 by address. -/
35 theorem exact_displacement (j n T : ℕ) (hj : j < 4) (hT : 0 < T) :
36     unnormalized 4 j (n + T) - unnormalized 4 j n ≠ 0 ∧
37     padicValRat 2 (unnormalized 4 j (n + T) - unnormalized 4 j n) =
38       (padicValNat 2 T : ℤ) + (originalBonus j : ℤ) := by
39   have h := normalized_exact_displacement j n T hj hT
40   have hf : (j.factorial : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero j)
41   have he : unnormalized 4 j (n + T) - unnormalized 4 j n =
42       (j.factorial : ℚ) * (coeff 4 j (n + T) - coeff 4 j n) := by
43     simp only [unnormalized, mul_sub]
44   rw [he]
45   refine ⟨mul_ne_zero hf h.1, ?_⟩
46   rw [padicValRat.mul hf h.1, padicValRat.of_nat, h.2]
47   simp only [originalBonus, Nat.cast_add]
48   ring
49 
50 /-- Pointwise congruence has the same sharp displacement criterion at every row. -/
51 theorem precision_iff_dvd (j r n T : ℕ) (hj : j < 4) (hT : 0 < T) :
52     precision 2 (r : ℤ) (unnormalized 4 j (n + T) - unnormalized 4 j n) ↔
53       2 ^ (r - originalBonus j) ∣ T :=
54   ExactPeriodClassification.precision_iff_dvd 2 (unnormalized 4 j)
55     (originalBonus j) r n T hT (exact_displacement j n T hj hT)
56 
57 /-- All positive periods, not only power-of-two candidates, are classified. -/
58 theorem period_iff_dvd (j r T : ℕ) (hj : j < 4) :
59     ExactPeriodClassification.IsPeriod 2 (unnormalized 4 j) r T ↔
60       0 < T ∧ 2 ^ (r - originalBonus j) ∣ T :=
61   ExactPeriodClassification.isPeriod_iff_dvd 2 (unnormalized 4 j)
62     (originalBonus j) r T (fun n S hS => exact_displacement j n S hj hS)
63 
64 /-- The least positive packet period is valid uniformly from row zero. -/
65 theorem least_packet_period (j r : ℕ) (hj : j < 4) :
66     IsLeast {T : ℕ | ExactPeriodClassification.IsPeriod 2 (unnormalized 4 j) r T}
67       (2 ^ (r - originalBonus j)) :=
68   ExactPeriodClassification.least_period 2 (unnormalized 4 j)
69     (originalBonus j) r (fun n S hS => exact_displacement j n S hj hS)
70 
71 /-- Exact displacement in Nishibuchi's original degree-indexed convention. -/
72 theorem original_degree_exact_displacement (j n T : ℕ) (hj : j < 4) (hT : 0 < T) :
73     NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n + 4 * T) -
74       NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n) ≠ 0 ∧
75     padicValRat 2
76       (NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n + 4 * T) -
77        NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n)) =
78       (padicValNat 2 T : ℤ) + (originalBonus j : ℤ) := by
79   rw [← Nat.mul_add, NishibuchiCompletion.generalizedEuler_at_packet,
80     NishibuchiCompletion.generalizedEuler_at_packet]
81   exact exact_displacement j n T hj hT
82 
83 end KomorebiPaperIX.DyadicFourLeastPeriods

Back to source controls