LeanPool.FriezePatterns.Chapter2

Imported Lean Pool material for LeanPool.FriezePatterns.Chapter2.

structure flute (n : ℕ) : Type

An n-flute: a positive integer sequence a with a 0 = 1, periodic with period n - 1, and satisfying the divisibility relation a (k + 1) ∣ a k + a (k + 2).

• a : ℕ → ℕ

  The underlying sequence of the flute.

• pos (i : ℕ) : self.a i > 0

  Every entry of the flute is positive.

• hd : self.a 0 = 1

  The flute starts at 1.

• period (k : ℕ) : self.a k = self.a (k + (n - 1))

  The flute is periodic with period n - 1.

• div (k : ℕ) : self.a (k + 1) ∣ self.a k + self.a (k + 2)

  Each interior entry divides the sum of its neighbours.

@[reducible]

def csteFlute (n : ℕ) : Inhabited (flute n)

The constant flute (the sequence identically equal to 1).

Inhabited is preferred over Nonempty so that we can recover the explicit witness.

Equations

• csteFlute n = { default := { a := fun (x : ℕ) => 1, pos := ⋯, hd := csteFlute._proof_1, period := csteFlute._proof_2, div := csteFlute._proof_3 } }

def fluteSet (n : ℕ) : Set (flute n)

The set of all n-flutes.

Equations

• fluteSet n = Set.univ

@[irreducible]

def aOdd (k i : ℕ) : ℕ

The underlying sequence of the Fibonacci-maximal (2k+1)-flute.

Equations

• aOdd k i = if k = 0 then 1 else if i ≥ 2 * k then aOdd k (i - 2 * k) else if i < k then Nat.fib (2 * i + 2) else Nat.fib (1 + 4 * k - 2 * i)

def fibFluteOdd (k : ℕ) : flute (2 * k + 1)

The Fibonacci-maximal (2k+1)-flute, built from aOdd.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def aEven (k i : ℕ) : ℕ

The underlying sequence of the Fibonacci-maximal (2k+2)-flute.

Equations

• aEven k i = if i ≥ 2 * k + 1 then aEven k (i - 2 * k - 1) else if i < k + 1 then Nat.fib (2 * i + 2) else Nat.fib (3 + 4 * k - 2 * i)

def fibFluteEven (k : ℕ) : flute (2 * k + 2)

The Fibonacci-maximal (2k+2)-flute, built from aEven.

Equations

• fibFluteEven k = { a := aEven k, pos := ⋯, hd := ⋯, period := ⋯, div := ⋯ }

@[irreducible]

def a_1 (n : ℕ) (f : flute (n + 3)) (k : ℕ) : ℕ

Reduction of an (n+3)-flute (assuming f.a 1 = 1) to an (n+2)-flute (underlying sequence).

Equations

• a_1 n f k = if k ≥ n + 1 then a_1 n f (k - (n + 1)) else if k = 0 then f.a 0 else f.a (k + 1)

def aux_1 (n : ℕ) (f : flute (n + 3)) (h : f.a 1 = 1) : flute (n + 2)

Reduction of an (n+3)-flute with f.a 1 = 1 to an (n+2)-flute.

Equations

• aux_1 n f h = { a := a_1 n f, pos := ⋯, hd := ⋯, period := ⋯, div := ⋯ }

@[irreducible]

def a_2 (n : ℕ) (f : flute (n + 3)) (k : ℕ) : ℕ

Reduction of an (n+3)-flute (assuming f.a (n + 1) = 1) to an (n+2)-flute (underlying sequence).

Equations

• a_2 n f k = if k ≥ n + 1 then a_2 n f (k - (n + 1)) else f.a k

def aux_2 (n : ℕ) (f : flute (n + 3)) (h : f.a (n + 1) = 1) : flute (n + 2)

Reduction of an (n+3)-flute with f.a (n + 1) = 1 to an (n+2)-flute.

Equations

• aux_2 n f h = { a := a_2 n f, pos := ⋯, hd := ⋯, period := ⋯, div := ⋯ }

@[irreducible]

def a3 (n : ℕ) (f : flute (n + 3)) (i : ℕ) (hi : i ≤ n ∧ f.a (i + 1) = f.a i + f.a (i + 2)) (k : ℕ) : ℕ

Reduction of an (n+3)-flute admitting a reducible index i to an (n+2)-flute (underlying sequence).

Equations

• a3 n f i hi k = if k ≥ n + 1 then a3 n f i hi (k - (n + 1)) else if k ≤ i then f.a k else f.a (k + 1)

def aux3 (n : ℕ) (f : flute (n + 3)) (j : ℕ) (hj : j ≤ n ∧ f.a (j + 1) = f.a j + f.a (j + 2)) : flute (n + 2)

Reduction of an (n+3)-flute admitting a reducible index j to an (n+2)-flute.

Equations

• aux3 n f j hj = { a := a3 n f j hj, pos := ⋯, hd := ⋯, period := ⋯, div := ⋯ }

theorem fluteSetNonEmpty (n : ℕ) : Nonempty ↑(fluteSet n)

The set of n-flutes is nonempty.

theorem FluteReduction (n : ℕ) (f : flute n) : (f.a 1 = 1 ∨ f.a (n - 2) = 1) ∨ ∃ i ≤ n - 3, f.a (i + 1) = f.a i + f.a (i + 2)

Every n-flute either has f.a 1 = 1, has f.a (n-2) = 1, or admits a reducible index i where f.a (i+1) = f.a i + f.a (i+2).

theorem FluteBounded (n : ℕ) (hn : n > 0) (f : flute n) (i : ℕ) : i ≤ n - 1 → f.a i ≤ Nat.fib n