Fix 1984 A6 (again)

This was disprovable because the value `g 0` breaks the period-4
pattern. More precisely, the period 4 arises because powers of 2
mod 10 have period 4 (2, 4, 8, 6, 2, 4, 8, 6, ...). However this
starts at 2^1 and the inital value 2^0 = 1 breaks the pattern.

The two obvious ways to fix the statement are:
 1. Change `P_def` to require periodicity only beyond 0.
 2. Change the characterisation of `g` so that `g 0` is free.
We have opted for the second choice.

This was previously "fixed" in 295b586
but unfortunately an error remained.

lean4/src/putnam_1984_a6.lean

@@ -15,10 +15,12 @@ Let $n$ be a positive integer, and let $f(n)$ denote the last nonzero digit in t
 theorem putnam_1984_a6
     (f : ℕ → ℕ)
     (hf : ∀ n, some (f n) = (Nat.digits 10 (n !)).find? (fun d ↦ d ≠ 0))
-    (P : (ℕ → ℕ) → ℕ → Prop)
-    (P_def : ∀ g p, P g p ↔
-      if p = 0 then (∀ q > 0, ¬ Periodic g q) else IsLeast {q | 0 < q ∧ Periodic g q} p) :
+    (IsPeriodicFrom : ℕ → (ℕ → ℕ) → ℕ → Prop)
+    (IsPeriodicFrom_def : ∀ x f p, IsPeriodicFrom x f p ↔ Periodic (f ∘ (· + x)) p)
+    (P : ℕ → (ℕ → ℕ) → ℕ → Prop)
+    (P_def : ∀ x g p, P x g p ↔ if p = 0 then (∀ q > 0, ¬ IsPeriodicFrom x g q) else
+        IsLeast {q | 0 < q ∧ IsPeriodicFrom x g q} p) :
     ∃ g : ℕ → ℕ,
       (∀ᵉ (k > 0) (a : Fin k → ℕ) (ha : Injective a), f (∑ i, 5 ^ (a i)) = g (∑ i, a i)) ∧
-      P g putnam_1984_a6_solution :=
+      P 1 g putnam_1984_a6_solution :=
   sorry