Fence tilings and bi-periodic Fibonacci numbers

DefinitionBi-periodic Fibonacci numbers squared#✓fully proved

For elements \(a\) and \(b\) of a field \(K\), the bi-periodic Fibonacci numbers squared \(q^2_n \in K\) (\(n \ge 0\)) are defined by \(q^2_0 = 0\), \(q^2_1 = 1\), \(q^2_2 = a^2\) and, for \(n \ge 3\),

\[ q^2_n = \frac{a}{b}(ab+1)\,q^2_{n-1} + (ab+1)\,q^2_{n-2} - \frac{a}{b}\,q^2_{n-3} \]

if \(n\) is even, and

\[ q^2_n = \frac{b}{a}(ab+1)\,q^2_{n-1} + (ab+1)\,q^2_{n-2} - \frac{b}{a}\,q^2_{n-3} \]

if \(n\) is odd.

Division by zero gives \(0\), so the sequence is defined for all \(a\) and \(b\).

def biPeriodicFibonacciSq {K : Type*} [Field K] (a b : K) : ℕ → K
  | 0 => 0
  | 1 => 1
  | 2 => a ^ 2
  | n + 3 =>
    if Even (n + 3) then
      a / b * (a * b + 1) * biPeriodicFibonacciSq a b (n + 2) +
        (a * b + 1) * biPeriodicFibonacciSq a b (n + 1) - a / b * biPeriodicFibonacciSq a b n
    else
      b / a * (a * b + 1) * biPeriodicFibonacciSq a b (n + 2) +
        (a * b + 1) * biPeriodicFibonacciSq a b (n + 1) - b / a * biPeriodicFibonacciSq a b n

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Definition 1.1.

Used by 5

Used byRecurrence for the bi-periodic Fibonacci numbers squared · First bi-periodic Fibonacci number squared · Second bi-periodic Fibonacci number squared · Zeroth bi-periodic Fibonacci number squared · Fence tilings and the bi-periodic Fibonacci numbers squared

TheoremZeroth bi-periodic Fibonacci number squared#✓fully proved

For elements \(a\) and \(b\) of a field \(K\), the bi-periodic Fibonacci number squared \(q^2_0\) equals \(0\).

@[simp]
theorem biPeriodicFibonacciSq_zero {K : Type*} [Field K] (a b : K) :
    biPeriodicFibonacciSq a b 0 = 0

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Definition 1.1.

Uses 1

Statement usesBi-periodic Fibonacci numbers squared

TheoremFirst bi-periodic Fibonacci number squared#✓fully proved

For elements \(a\) and \(b\) of a field \(K\), the bi-periodic Fibonacci number squared \(q^2_1\) equals \(1\).

@[simp]
theorem biPeriodicFibonacciSq_one {K : Type*} [Field K] (a b : K) :
    biPeriodicFibonacciSq a b 1 = 1

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Definition 1.1.

Uses 1

Statement usesBi-periodic Fibonacci numbers squared

TheoremSecond bi-periodic Fibonacci number squared#✓fully proved

For elements \(a\) and \(b\) of a field \(K\), the bi-periodic Fibonacci number squared \(q^2_2\) equals \(a^2\).

@[simp]
theorem biPeriodicFibonacciSq_two {K : Type*} [Field K] (a b : K) :
    biPeriodicFibonacciSq a b 2 = a ^ 2

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Definition 1.1.

Uses 1

Statement usesBi-periodic Fibonacci numbers squared

TheoremRecurrence for the bi-periodic Fibonacci numbers squared#✓fully proved

For elements \(a\) and \(b\) of a field \(K\) and every \(n \ge 0\), the bi-periodic Fibonacci numbers squared \(q^2_m\) satisfy

\[ q^2_{n+3} = \frac{a}{b}(ab+1)\,q^2_{n+2} + (ab+1)\,q^2_{n+1} - \frac{a}{b}\,q^2_n \]

if \(n + 3\) is even, and

\[ q^2_{n+3} = \frac{b}{a}(ab+1)\,q^2_{n+2} + (ab+1)\,q^2_{n+1} - \frac{b}{a}\,q^2_n \]

if \(n + 3\) is odd.

Division by zero gives \(0\), so this holds for all \(a\) and \(b\).

theorem biPeriodicFibonacciSq_add_three {K : Type*} [Field K] (a b : K) (n : ℕ) :
    biPeriodicFibonacciSq a b (n + 3) =
      if Even (n + 3) then
        a / b * (a * b + 1) * biPeriodicFibonacciSq a b (n + 2) +
          (a * b + 1) * biPeriodicFibonacciSq a b (n + 1) - a / b * biPeriodicFibonacciSq a b n
      else
        b / a * (a * b + 1) * biPeriodicFibonacciSq a b (n + 2) +
          (a * b + 1) * biPeriodicFibonacciSq a b (n + 1) - b / a * biPeriodicFibonacciSq a b n

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Definition 1.1, (1.1).

Uses 1

Statement usesBi-periodic Fibonacci numbers squared

DefinitionFence tilings of a board#✓fully proved

Number the half-cells of an \(n\)-board \(0, \dots, 2n - 1\). The tilings of the \(n\)-board by half-squares and \((1/2, 1/2)\)-fences are encoded as the sets \(F\) of fence positions \(k < 2n - 2\) (the fence at \(k\) has posts on half-cells \(k\) and \(k + 2\)) whose posts are pairwise disjoint, that is, \(k + 2 \notin F\) for every \(k \in F\).

def fenceTilings (n : ℕ) : Finset (Finset ℕ) :=
  (range (2 * n - 2)).powerset.filter fun F => ∀ k ∈ F, k + 2 ∉ F

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Section 2.

Used by 8

Used byWeighted count of fence tilings · Weighted fence tilings of the one-cell board · Weighted fence tilings of the empty board · Weighted count of bifence-free fence tilings · Tilings of the empty board with no bifence · Weighted tilings with no free bifence · Tilings of the one-cell board with no free bifence · Tilings of the empty board with no free bifence

DefinitionWeight of a fence tiling#✓fully proved

Let \(a\), \(b\) be elements of a commutative semiring, let \(n \ge 0\), and let \(F\) be a finite set of natural numbers (fence positions; the fence at \(k\) has posts on half-cells \(k\) and \(k + 2\)). The weight of \(F\) on the \(n\)-board is the product, over the half-cells \(h \in \{0, \dots, 2n - 1\}\) that neither lie in \(F\) nor equal \(k + 2\) for some \(k \in F\), of \(a\) if \(\lfloor h/2 \rfloor\) is even (a half-square in the odd cell \(\lfloor h/2 \rfloor + 1\)) and of \(b\) otherwise (a half-square in an even cell).

def fenceTilingWeight {R : Type*} [CommSemiring R] (a b : R) (n : ℕ) (F : Finset ℕ) : R :=
  ∏ h ∈ range (2 * n) \ (F ∪ F.image (· + 2)), if h / 2 % 2 = 0 then a else b

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Section 2.

Used by 8

Used byWeighted count of fence tilings · Weighted fence tilings of the one-cell board · Weighted fence tilings of the empty board · Weighted count of bifence-free fence tilings · Tilings of the empty board with no bifence · Weighted tilings with no free bifence · Tilings of the one-cell board with no free bifence · Tilings of the empty board with no free bifence

DefinitionWeighted count of fence tilings#✓fully proved

Let \(a\), \(b\) be elements of a commutative semiring and \(n \ge 0\). The weighted number \(S_n\) of tilings of an \(n\)-board by half-squares and \((1/2, 1/2)\)-fences is the sum, over all fence tilings \(F\) of the \(n\)-board, of the weight of \(F\), in which a half-square weighs \(a\) in an odd cell and \(b\) in an even cell and fences weigh \(1\).

def fenceTilingSum {R : Type*} [CommSemiring R] (a b : R) (n : ℕ) : R :=
  ∑ F ∈ fenceTilings n, fenceTilingWeight a b n F

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Section 2 (before Lemma 2.1).

Uses 2 · Used by 5

Statement usesWeight of a fence tiling · Fence tilings of a board

Used byFence tilings and the bi-periodic Fibonacci numbers squared · Recurrence for weighted fence tilings of even boards · Recurrence for weighted fence tilings of odd boards · Weighted fence tilings of the one-cell board · Weighted fence tilings of the empty board

TheoremWeighted fence tilings of the empty board#✓fully proved

For elements \(a\) and \(b\) of a commutative semiring \(R\), the weighted number \(S_0\) of tilings of the \(0\)-board by half-squares and \((1/2, 1/2)\)-fences equals \(1\): the only tiling is the empty one.

@[simp]
theorem fenceTilingSum_zero {R : Type*} [CommSemiring R] (a b : R) : fenceTilingSum a b 0 = 1

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, proof of Lemma 2.1.

Uses 3

Statement usesWeighted count of fence tilings

Proof usesWeight of a fence tiling · Fence tilings of a board

TheoremWeighted fence tilings of the one-cell board#✓fully proved

For elements \(a\) and \(b\) of a commutative semiring \(R\), the weighted number \(S_1\) of tilings of a \(1\)-board by half-squares and \((1/2, 1/2)\)-fences, a half-square weighing \(a\) in an odd cell and \(b\) in an even cell, equals \(a^2\): the only tiling has two half-squares in cell \(1\).

@[simp]
theorem fenceTilingSum_one {R : Type*} [CommSemiring R] (a b : R) : fenceTilingSum a b 1 = a ^ 2

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, proof of Theorem 2.2.

Uses 3

Statement usesWeighted count of fence tilings

Proof usesWeight of a fence tiling · Fence tilings of a board

DefinitionWeighted count of bifence-free fence tilings#✓fully proved

Let \(a\), \(b\) be elements of a commutative semiring and \(n \ge 0\). Two fences at positions \(k\) and \(k + 1\) form a bifence. The weighted number \(C_n\) of tilings with no bifence is the sum of the weights, with half-square weights \(a\) and \(b\), of the fence tilings \(F\) of the \(n\)-board with no bifence, that is, with \(k + 1 \notin F\) for every \(k \in F\).

def noBifenceTilingSum {R : Type*} [CommSemiring R] (a b : R) (n : ℕ) : R :=
  ∑ F ∈ (fenceTilings n).filter (fun F => ∀ k ∈ F, k + 1 ∉ F), fenceTilingWeight a b n F

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Lemma 3.15.

Uses 2 · Used by 2

Statement usesWeight of a fence tiling · Fence tilings of a board

Used byClosed formula for bifence-free fence tilings · Tilings of the empty board with no bifence

TheoremTilings of the empty board with no bifence#✓fully proved

For all elements \(a\), \(b\) of a commutative semiring, the weighted number \(C_0\) of tilings of the \(0\)-board with no bifence, with half-square weights \(a\) and \(b\), equals \(1\).

@[simp]
theorem noBifenceTilingSum_zero {R : Type*} [CommSemiring R] (a b : R) :
    noBifenceTilingSum a b 0 = 1

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Lemma 3.15.

Uses 3

Statement usesWeighted count of bifence-free fence tilings

Proof usesWeight of a fence tiling · Fence tilings of a board

DefinitionWeighted tilings with no free bifence#✓fully proved

For elements \(a\), \(b\) of a commutative semiring and \(n \ge 0\), number the cells of an \(n\)-board \(1, \dots, n\) and its \(2n\) half-cells \(0, \dots, 2n - 1\), half-cell \(h\) lying in cell \(\lfloor h/2 \rfloor + 1\). A \((1/2, 1/2)\)-fence at position \(k\) has its posts on half-cells \(k\) and \(k + 2\). Then \(R_n\) is the sum of the weights of the tilings of the board by half-squares and such fences that contain no free bifence, that is, no two fences at positions \(k\) and \(k + 1\) with \(k\) even. The weight of a tiling is the product over its half-squares of \(a\) for a half-square in an odd cell and \(b\) for one in an even cell.

def noFreeBifenceTilingSum {R : Type*} [CommSemiring R] (a b : R) (n : ℕ) : R :=
  ∑ F ∈ (fenceTilings n).filter (fun F => ∀ k ∈ F, Even k → k + 1 ∉ F), fenceTilingWeight a b n F

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Lemma 3.13.

Uses 2 · Used by 3

Statement usesWeight of a fence tiling · Fence tilings of a board

Used byTilings of the one-cell board with no free bifence · Recurrence for weighted tilings with no free bifence · Tilings of the empty board with no free bifence

TheoremTilings of the empty board with no free bifence#✓fully proved

For all elements \(a\), \(b\) of a commutative semiring, the weighted number \(R_0\) of tilings of the \(0\)-board by half-squares and \((1/2, 1/2)\)-fences with no free bifence, with half-squares weighted by \(a\) and \(b\), equals \(1\).

@[simp]
theorem noFreeBifenceTilingSum_zero {R : Type*} [CommSemiring R] (a b : R) :
    noFreeBifenceTilingSum a b 0 = 1

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Lemma 3.13.

Uses 3

Statement usesWeighted tilings with no free bifence

Proof usesWeight of a fence tiling · Fence tilings of a board

TheoremTilings of the one-cell board with no free bifence#✓fully proved

For all elements \(a\), \(b\) of a commutative semiring, the weighted number \(R_1\) of tilings of the \(1\)-board with no free bifence, with half-square weights \(a\) and \(b\), equals \(a^2\).

@[simp]
theorem noFreeBifenceTilingSum_one {R : Type*} [CommSemiring R] (a b : R) :
    noFreeBifenceTilingSum a b 1 = a ^ 2

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Lemma 3.13.

Uses 3

Statement usesWeighted tilings with no free bifence

Proof usesWeight of a fence tiling · Fence tilings of a board

TheoremRecurrence for weighted fence tilings of even boards#●ready to prove

Let \(a\) and \(b\) be elements of a commutative semiring \(R\), and let \(S_m\) be the weighted number of tilings of an \(m\)-board, with cells numbered \(1, \dots, m\), by half-squares and \((1/2, 1/2)\)-fences, a half-square weighing \(a\) in an odd cell and \(b\) in an even cell. Then for every even \(n \ge 2\),

\[ S_n = b^2 S_{n-1} + (2ab+1) S_{n-2} + 2ab \sum_{j=2}^{n/2} S_{n-2j} + 2b^2 \sum_{j=1}^{n/2-1} S_{n-2j-1}. \]

public theorem_wanted fenceTilingSum_even {R : Type*} [CommSemiring R] (a b : R) {n : ℕ}
    (hn : 2 ≤ n) (he : Even n) :
    fenceTilingSum a b n =
      b ^ 2 * fenceTilingSum a b (n - 1) + (2 * a * b + 1) * fenceTilingSum a b (n - 2) +
        2 * a * b * ∑ j ∈ Icc 2 (n / 2), fenceTilingSum a b (n - 2 * j) +
        2 * b ^ 2 * ∑ j ∈ Icc 1 (n / 2 - 1), fenceTilingSum a b (n - 2 * j - 1)

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Lemma 2.1, (2.1).

Uses 1

Statement usesWeighted count of fence tilings

TheoremRecurrence for weighted fence tilings of odd boards#●ready to prove

Let \(a\) and \(b\) be elements of a commutative semiring \(R\), and let \(S_m\) be the weighted number of tilings of an \(m\)-board, with cells numbered \(1, \dots, m\), by half-squares and \((1/2, 1/2)\)-fences, a half-square weighing \(a\) in an odd cell and \(b\) in an even cell. Then for every odd \(n \ge 3\),

\[ S_n = a^2 S_{n-1} + (2ab+1) S_{n-2} + 2ab \sum_{j=2}^{(n-1)/2} S_{n-2j} + 2a^2 \sum_{j=1}^{(n-1)/2} S_{n-2j-1}. \]

public theorem_wanted fenceTilingSum_odd {R : Type*} [CommSemiring R] (a b : R) {n : ℕ}
    (hn : 2 ≤ n) (ho : Odd n) :
    fenceTilingSum a b n =
      a ^ 2 * fenceTilingSum a b (n - 1) + (2 * a * b + 1) * fenceTilingSum a b (n - 2) +
        2 * a * b * ∑ j ∈ Icc 2 ((n - 1) / 2), fenceTilingSum a b (n - 2 * j) +
        2 * a ^ 2 * ∑ j ∈ Icc 1 ((n - 1) / 2), fenceTilingSum a b (n - 2 * j - 1)

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Lemma 2.1, (2.1).

Uses 1

Statement usesWeighted count of fence tilings

TheoremFence tilings and the bi-periodic Fibonacci numbers squared#●ready to prove

Let \(a\) and \(b\) be nonzero elements of a field \(K\). For every \(n \ge 0\), let \(S_n\) be the weighted number of tilings of an \(n\)-board, with cells numbered \(1, \dots, n\), by half-squares and \((1/2, 1/2)\)-fences, a half-square weighing \(a\) in an odd cell and \(b\) in an even cell. Then \(S_n\) equals the bi-periodic Fibonacci number squared \(q^2_{n+1}\).

public theorem_wanted fenceTilingSum_eq_biPeriodicFibonacciSq {K : Type*} [Field K] {a b : K}
    (ha : a ≠ 0) (hb : b ≠ 0) (n : ℕ) :
    fenceTilingSum a b n = biPeriodicFibonacciSq a b (n + 1)

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Theorem 2.2.

Uses 2

Statement usesBi-periodic Fibonacci numbers squared · Weighted count of fence tilings

TheoremSquared Fibonacci numbers as a double binomial sum#●ready to prove

Let \(F_k\) denote the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\)). For every natural number \(n\),

\[ F_{n+1}^2 = \sum_{i=0}^{\lfloor 2n/3 \rfloor} \sum_{j=0}^{i} \binom{i}{j} \binom{2n-3i}{j} 2^j. \]

public theorem_wanted fib_succ_sq_eq_sum_choose_mul_choose (n : ℕ) :
    Nat.fib (n + 1) ^ 2 =
      ∑ i ∈ range (2 * n / 3 + 1), ∑ j ∈ range (i + 1),
        i.choose j * (2 * n - 3 * i).choose j * 2 ^ j

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Corollary 3.3.

TheoremSum of squared Fibonacci numbers from three consecutive squares#●ready to prove

Let \(F_j\) denote the \(j\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\). For every integer \(n \ge 3\),

\[2 \sum_{j=1}^{n-2} F_j^2 = F_n^2 - F_{n-1}^2 - F_{n-2}^2.\]

public theorem_wanted two_mul_sum_fib_sq {n : ℕ} (hn : 3 ≤ n) :
    2 * ∑ j ∈ Icc 1 (n - 2), (Nat.fib j : ℤ) ^ 2 =
      (Nat.fib n : ℤ) ^ 2 - (Nat.fib (n - 1) : ℤ) ^ 2 - (Nat.fib (n - 2) : ℤ) ^ 2

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Corollary 3.5.

TheoremSquared Fibonacci numbers as weighted sums of squares#●ready to prove

Let \(F_k\) denote the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\)) and let \(\xi(m) = m \bmod 2\). For every natural number \(n \ge 1\),

\[ F_{n+1}^2 - \xi(n+1) = \sum_{k=1}^{n} (n-k+1) F_k^2 = \sum_{k=1}^{n} k F_{n-k+1}^2. \]

public theorem_wanted fib_succ_sq_sub_parity_eq_sum {n : ℕ} (hn : 1 ≤ n) :
    (Nat.fib (n + 1) : ℤ) ^ 2 - ((n + 1) % 2 : ℕ) =
        ∑ k ∈ Icc 1 n, ((n - k + 1 : ℕ) : ℤ) * (Nat.fib k : ℤ) ^ 2 ∧
      (Nat.fib (n + 1) : ℤ) ^ 2 - ((n + 1) % 2 : ℕ) =
        ∑ k ∈ Icc 1 n, (k : ℤ) * (Nat.fib (n - k + 1) : ℤ) ^ 2

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Corollary 3.10.

TheoremAddition formula for squared Fibonacci numbers#●ready to prove

Let \(F_k\) denote the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\)). For all natural numbers \(m \ge 1\) and \(n \ge 2\),

\[ F_{m+n}^2 = F_{m+1}^2 F_n^2 + F_m^2 F_{n-1}^2 + 2 \left(\sum_{i=1}^{m} F_i^2\right) \left(\sum_{j=1}^{n-1} F_j^2\right). \]

public theorem_wanted fib_add_sq_eq {m n : ℕ} (hm : 1 ≤ m) (hn : 2 ≤ n) :
    Nat.fib (m + n) ^ 2 =
      Nat.fib (m + 1) ^ 2 * Nat.fib n ^ 2 + Nat.fib m ^ 2 * Nat.fib (n - 1) ^ 2 +
        2 * (∑ i ∈ Icc 1 m, Nat.fib i ^ 2) * ∑ j ∈ Icc 1 (n - 1), Nat.fib j ^ 2

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Corollary 3.12.

TheoremRecurrence for weighted tilings with no free bifence#●ready to prove

Let \(a\) and \(b\) be nonzero elements of a field, and let \(R_n\) be the weighted number of tilings of an \(n\)-board by half-squares and \((1/2, 1/2)\)-fences with no free bifence, where a half-square has weight \(a\) in an odd cell and \(b\) in an even cell (cells numbered \(1, \dots, n\)). For every \(n \ge 2\),

\[R_n = \frac{b}{a}(ab + 1) R_{n-1} + ab\, R_{n-2}\]

if \(n\) is even, and

\[R_n = \frac{a}{b}(ab + 1) R_{n-1} + ab\, R_{n-2}\]

if \(n\) is odd.

The initial values are \(R_0 = 1\) and \(R_1 = a^2\).

public theorem_wanted noFreeBifenceTilingSum_rec {K : Type*} [Field K] {a b : K} (ha : a ≠ 0)
    (hb : b ≠ 0) {n : ℕ} (hn : 2 ≤ n) :
    noFreeBifenceTilingSum a b n =
      (if Even n then b / a else a / b) * (a * b + 1) * noFreeBifenceTilingSum a b (n - 1) +
        a * b * noFreeBifenceTilingSum a b (n - 2)

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Lemma 3.13.

Uses 1

Statement usesWeighted tilings with no free bifence

TheoremClosed formula for bifence-free fence tilings#●ready to prove

Let \(a\), \(b\) be nonzero elements of a field and let \(\xi(n) = n \bmod 2\). For every natural number \(n\), the weighted number \(C_n\) of tilings of the \(n\)-board by half-squares and \((1/2, 1/2)\)-fences with no bifence, with half-square weights \(a\) and \(b\), is

\[ C_n = \left(\frac{a}{b}\right)^{\xi(n)} \sum_{i=0}^{\lfloor 2n/3 \rfloor} \binom{2n-2i}{i} (ab)^{n-i}. \]

public theorem_wanted noBifenceTilingSum_eq_sum_choose {K : Type*} [Field K] {a b : K}
    (ha : a ≠ 0) (hb : b ≠ 0) (n : ℕ) :
    noBifenceTilingSum a b n =
      (a / b) ^ (n % 2) *
        ∑ i ∈ range (2 * n / 3 + 1), ((2 * n - 2 * i).choose i : K) * (a * b) ^ (n - i)

Sources

• Nassima Belaggoun and Hacène Belbachir, Combinatorial Identities for the Bi-Periodic Fibonacci Numbers Squared, The Fibonacci Quarterly 62 (2024), Article belaggoun01132024, Lemma 3.15.

Uses 1

Statement usesWeighted count of bifence-free fence tilings

15 fully proved9 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.