ExactPeriodClassification.lean

1 module
2 public import GlobalEulerBoundary
3 @[expose] public section
4 noncomputable section
5 set_option autoImplicit false
6 namespace KomorebiPaperIX.ExactPeriodClassification
7 open GlobalEulerBoundary
8 
9 variable (p : ℕ) [Fact p.Prime]
10 
11 /-- A positive packet shift that preserves every row modulo the stated prime power. -/
12 def IsPeriod (f : ℕ → ℚ) (r T : ℕ) : Prop :=
13   0 < T ∧ ∀ n, precision p (r : ℤ) (f (n + T) - f n)
14 
15 /-- Exact displacement valuations characterize every positive period by divisibility. -/
16 theorem precision_iff_dvd (f : ℕ → ℚ) (d r n T : ℕ) (hT : 0 < T)
17     (H : f (n + T) - f n ≠ 0 ∧
18       padicValRat p (f (n + T) - f n) = (padicValNat p T : ℤ) + (d : ℤ)) :
19     precision p (r : ℤ) (f (n + T) - f n) ↔ p ^ (r - d) ∣ T := by
20   obtain ⟨hnz, hv⟩ := H
21   rw [precision, or_iff_right hnz, hv, padicValNat_dvd_iff_le hT.ne']
22   omega
23 
24 theorem isPeriod_iff_dvd (f : ℕ → ℚ) (d r T : ℕ)
25     (H : ∀ n S, 0 < S → f (n + S) - f n ≠ 0 ∧
26       padicValRat p (f (n + S) - f n) = (padicValNat p S : ℤ) + (d : ℤ)) :
27     IsPeriod p f r T ↔ 0 < T ∧ p ^ (r - d) ∣ T := by
28   constructor
29   · rintro ⟨hT, hp⟩
30     exact ⟨hT, (precision_iff_dvd p f d r 0 T hT (H 0 T hT)).mp (hp 0)⟩
31   · rintro ⟨hT, hd⟩
32     refine ⟨hT, fun n => ?_⟩
33     exact (precision_iff_dvd p f d r n T hT (H n T hT)).mpr hd
34 
35 /-- Least means positive and valid at every row, not merely at a selected row. -/
36 theorem least_period (f : ℕ → ℚ) (d r : ℕ)
37     (H : ∀ n S, 0 < S → f (n + S) - f n ≠ 0 ∧
38       padicValRat p (f (n + S) - f n) = (padicValNat p S : ℤ) + (d : ℤ)) :
39     IsLeast {T : ℕ | IsPeriod p f r T} (p ^ (r - d)) := by
40   have hp : 0 < p ^ (r - d) := pow_pos (Fact.out : p.Prime).pos _
41   constructor
42   · exact (isPeriod_iff_dvd p f d r _ H).mpr ⟨hp, dvd_rfl⟩
43   · intro T hT
44     obtain ⟨hpos, hdiv⟩ := (isPeriod_iff_dvd p f d r T H).mp hT
45     exact Nat.le_of_dvd hpos hdiv
46 
47 end KomorebiPaperIX.ExactPeriodClassification

Back to source controls