Definition and Theorems of the Generalised Kaminski Equation

kaminski.lean

import data.nat.basic
import data.nat.prime
import data.fintype.basic
import tactic

theorem kaminski (f : bool → bool) (x : bool) : f (f (f x)) = f x :=
by cases x; cases h₁ : f tt; cases h₂ : f ff; simp only [h₁, h₂]

/-- the general case -/

def gk (n a b : ℕ) := ∀ f (x : fin n), (f^[a] x) = (f^[b] x)

example : gk 2 3 1 :=
begin
  intros f x,
  cases @exists_eq' _ (f 0) with y hy,
  cases @exists_eq' _ (f 1) with z hz,
  fin_cases x; fin_cases y; fin_cases z;
  simp [hy, hz],
end

/-- trivial identities -/

theorem gk.refl {n a : ℕ} : gk n a a :=
  λ f x, rfl

theorem gk.symm {n a b : ℕ} : gk n a b → gk n b a :=
  λ h f x, eq.symm (h f x)

theorem gk.zero {a b : ℕ} : gk 0 a b :=
  λ f x, by cc

theorem gk.one {a b : ℕ} : gk 1 a b :=
  λ f x, by cc

/-- additive properties -/

theorem gk.add {n a b c d : ℕ} : gk n a b → gk n c d → gk n (a + c) (b + d) :=
  λ h₁ h₂ f x, by rw [function.iterate_add_apply, h₁, h₂, function.iterate_add_apply]

theorem gk.trail {n a b c : ℕ} : gk n a b → gk n (a + c) (b + c) :=
  λ h, gk.add h (gk.refl)

lemma gk.extra_lap {n a b : ℕ} : gk n a (a + b) → gk n a (a + b + b) :=
  λ h f x, by rw [h, function.iterate_add_apply, h, ←function.iterate_add_apply]

lemma gk.extra_lap' {n a b : ℕ} : gk n a b → gk n a (b + (b - a)) :=
begin
  intros h f x, by_cases hc : b < a,
  { rw [nat.sub_eq_zero_of_le (le_of_lt hc), nat.add_zero], exact (h f x) },

  have h' := @gk.extra_lap n a (b - a),
  rw [←nat.add_sub_assoc (not_lt.mp hc), add_tsub_cancel_left] at h',
  exact (h' h _ _),
end

theorem gk.shift_right {n a b m : ℕ} : gk n a b → gk n a (b + (b - a) * m) :=
begin
  intros h f x,
  induction m with m ih,
  { rw [nat.mul_zero, nat.add_zero], apply h, },
  { have h' := gk.extra_lap' h f x,
    rw [nat.add_comm, function.iterate_add_apply] at h',
    rw [nat.mul_succ, ←nat.add_assoc, nat.add_comm,
      function.iterate_add_apply, ←ih, h, ←h', h],
  },
end

theorem gk.shift_left {n a b m : ℕ} : gk n a b → gk n (a + (a - b) * m) b :=
  λ h, gk.symm $ gk.shift_right $ gk.symm h

/-- non-trivial solutions -/

theorem gk.non_triv_exists {n : ℕ} : ∃ a b, a ≠ b ∧ gk n a b :=
begin
  have h : ¬function.injective (λ k (f : fin n → fin n), f^[k]),
  apply not_injective_infinite_fintype,
  unfold function.injective at h,
  push_neg at h,
  simp_rw function.funext_iff at h,
  rcases h with ⟨a, b, h₁, h₂⟩,
  exact ⟨a, b, h₂, λ f x, h₁ f x⟩,
end

def a (n : ℕ) := n - 1
def b (n : ℕ) := list.foldr nat.lcm 1 (list.iota n) + n - 1

theorem gk.non_triv_exact {n : ℕ} : gk n (a n) (b n) :=
begin
  sorry
end