Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized

Corollary 3.3

Fix a positive integer \(n\). The set Frieze\((n)\) is non-empty.

LaTeX Lean

Corollary 1.4

Let \(f\) be a nowhere-zero \(F\)-valued pattern of height \(n\). Then, \({\rm Im}(f) := \{ f (i,m) : i \in \{ 1,\ldots , n\} , m \in \mathbb {Z}\} \) is a finite set.

LaTeX Lean

Definition 3.1

A \(\mathbb {Q}\)-valued pattern of height \(n\) is said to be an arithmetic frieze pattern if it takes values in \(\mathbb {Z}_{{\gt}0}\). We denote by Frieze\((n)\) the set of arithmetic frieze patterns of height \(n\).

LaTeX Lean

Definition 2.1

A sequence \((a_k)\), indexed by \(\mathbb {N}^*\) and consisting of positive integers is called pandean if \(a_1 = 1\) and if, for every \(k {\gt} 1\), we have

\[ a_k \mid a_{k-1} + a_{k+1}. \]

Given a pandean sequence \((a_k)\), if there exists a positive integer \(n\) such that \(a_k = a_{k+n-1}\) for all \(k\in \mathbb {N}\), the tuple \((a_1, \ldots , a_n)\) is called a Pan flute, or simply a flute, of height \(n\). The set of all flutes of a given height \(n\) is denoted Flute\((n)\).

LaTeX Lean

Definition 1.1

Fix \(n \in \mathbb {N}^*\). A map \(f : \{ 0,1,\ldots , n,n+1\} \times \mathbb {Z} \longrightarrow F\) is called an \(F\)-valued pattern of height n if,

1) for all \(m \in \mathbb {Z}\), \( f(0,m) = f (n+1,m) = 0\),

2) for all \(m \in \mathbb {Z}\), \( f(1,m) = f (n,m) = 1\), and

3) for all \((i,m) \in \{ 1,2,\ldots , n\} \times \mathbb {Z}\), we have

\begin{equation} \label{eq:diamond} f(i,m) f(i,m+1) = 1 + f(i+1,m) f(i-1, m+1). \end{equation}

LaTeX Lean

Lemma 2.3

1) If \(n\) is odd, the \(n\)-tuple

\[ (F_2,F_4, F_6, \ldots , F_{n-1}, F_{n}, F_{n-2}, F_{n-4}, \ldots , F_5, F_3, F_1), \]

is a Pan flute of height \(n\).

2) If \(n\) is even, the \(n\)-tuple

\[ (F_2, F_4, F_6, \ldots , F_{n-2}, F_{n}, F_{n-1}, F_{n-3}, \ldots , F_5, F_3,F_1), \]

is a Pan flute of height \(n\).

LaTeX

Lean

fib_flute_even
fib_flute_odd

Lemma 2.2

For any positive integer \(n\), the set Flute\((n)\) is non-empty.

LaTeX

Lean

fluteSetNonEmpty
csteFlute

Lemma 1.2

Let \(f\) be a nowhere-zero \(F\)-valued pattern of height \(n\). For all \(m\), we have

\begin{align*} f(i+2,m) & = f(2,m+i) f(i+1,m) - f(i,m), \qquad i \in \{ 0, \ldots , n-1\} \\ f (i,m) & = f (n-1,m) f (i+1,m-1) - f(i+2,m-2), \qquad i \in \{ 0,n-1\} . \end{align*}

LaTeX

Lean

pattern_nContinuant1
pattern_nContinuant2

Lemma 2.4

In a flute \((a_1, \ldots , a_n)\), one of the following two statements holds.

1) \(a_2 = 1\) or \(a_{n-1} =1\).

2) There exists an index \(i \in \{ 2,\ldots , n-1\} \) such that \(a_i = a_{i-1} + a_{i+1}\).

LaTeX Lean

Theorem 3.4

For all \(n \geq 1\), we have

\[ u_n = F_{n}. \]

LaTeX

Lean

main1
main2
main3

Proposition 2.5

Fix a positive integer \(n\), and let \((a_1, \ldots , a_n) \in {\rm Flute}(n)\). For any \(i \in \{ 1,\ldots , n\} \), we have \(a_i \leq F_n\).

LaTeX Lean

Proposition 3.2

1) Let \(f\) be an arithmetic frieze pattern of height \(n\). For all \(m \in \mathbb {Z}\), the \(n\)-tuple

\[ (f (1,m), f (2,m), \ldots , f (n,m)) \]

is a flute of height \(n\).

2) Given a flute \((a_1, \ldots , a_n)\), there exists a arithmetic frieze pattern \(f\) of height \(n\) such that

\[ (f (1,0), \ldots , f (n,0)) = (a_1, \ldots , a_n). \]

LaTeX

Lean

friezeToFlute
frieze_f
fluteToFrieze

Proposition 1.3

Let \(f\) be a nowhere-zero \(F\)-valued pattern of height \(n\). Then, for all \(m \in \mathbb {Z}\) and all \(i \in \{ 0,\ldots , n+1\} \), we have

\[ f(i,m) = f(i,m+n+1). \]

LaTeX Lean