Two integer frieze patterns whose middle rows are strictly ordered

A Conway–Coxeter frieze pattern of width w is determined by its quiddity a = (a₀, …, a_{n-1}), n = w + 3: the entry of row k starting at position i is the continuant K(a_i, a_{i+1}, …, a_{i+k-1}) (indices modulo n), row 0 is all ones, and the pattern closes with a row of ones (row w + 1) followed by a row of zeros (row w + 2). It is an integer Conway–Coxeter frieze when, in addition, rows 1, …, w are positive.

S. Tabachnikov (A four-vertex theorem for frieze patterns?, Math. Intelligencer 40 (2018), 14–18, Problem 1) asks for which rows the cyclic sequence of differences of two such friezes of the same width must change sign at least four times; a rational counterexample (width 5, middle row) is due to M. Cuntz, and the question is left open for friezes of positive integers.

We record two integer Conway–Coxeter friezes of width 11 (n = 14) whose middle rows (row 6, the row of the diameters of the 14-gon) are strictly ordered at all 14 positions, so the difference has no sign change at all. The verification is a finite computation checked by the kernel (decide +kernel; the only axiom used is propext). An exhaustive search found 672 such ordered pairs (24 dihedral orbits) with strictly ordered rows at width 11, and none with strictly ordered rows, in any row, at smaller widths. The middle row is row ⌈w/2⌉; the printed range 1 ≤ k ≤ [w/2] of the question would exclude it, but the question's own rational example (width 5, row 3) is a middle row too.

def Frieze.continuant (l : List ℤ) : ℤ

The continuant K(x₁, …, x_j): K() = 1, K(x₁) = x₁, and K(x₁, …, x_j) = x_j K(x₁, …, x_{j-1}) - K(x₁, …, x_{j-2}).

Equations

• Frieze.continuant l = (List.foldl (fun (p : ℤ × ℤ) (x : ℤ) => (p.snd, x * p.snd - p.fst)) (0, 1) l).snd

def Frieze.entry (a : List ℤ) (k i : ℕ) : ℤ

The entry of row k at position i of the frieze pattern with quiddity a: the continuant of a_i, …, a_{i+k-1}, indices modulo the length of a.

Equations

• Frieze.entry a k i = Frieze.continuant (List.map (fun (t : ℕ) => a.getD ((i + t) % a.length) 0) (List.range k))

def Frieze.IsQuiddity (a : List ℤ) : Prop

a is the quiddity of an integer Conway–Coxeter frieze of width a.length - 3: rows 1, …, a.length - 3 are positive, row a.length - 2 is all ones and row a.length - 1 is all zeros.

Equations

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

@[instance_reducible]

instance Frieze.instDecidableIsQuiddity (a : List ℤ) : Decidable (IsQuiddity a)

Equations

• Frieze.instDecidableIsQuiddity a = id inferInstance

def Frieze.lower : List ℤ

The fan of the 14-gon from vertex 13 with its diameter (13, 6) flipped to (5, 7).

Equations

• Frieze.lower = [1, 2, 2, 2, 2, 3, 1, 3, 2, 2, 2, 2, 1, 11]

def Frieze.upper : List ℤ

A triangulation of the 14-gon without diameters.

Equations

• Frieze.upper = [1, 5, 2, 3, 1, 2, 5, 4, 1, 2, 2, 4, 2, 2]

theorem Frieze.isQuiddity_lower : IsQuiddity lower

theorem Frieze.isQuiddity_upper : IsQuiddity upper

theorem Frieze.entry_six_lower_lt_upper (i : ℕ) : i < 14 → entry lower 6 i < entry upper 6 i

The middle rows: (2, 6, 6, 6, 6, 6, 6) and (3, 7, 7, 8, 7, 7, 7), each repeated twice.

theorem Frieze.exists_strictly_ordered_middle_rows : ∃ (a : List ℤ), ∃ (b : List ℤ), IsQuiddity a ∧ IsQuiddity b ∧ a.length = 14 ∧ b.length = 14 ∧ ∀ (i : ℕ), i < 14 → entry a 6 i < entry b 6 i

Two integer Conway–Coxeter friezes of the same width 11 whose row 6 differences entry upper 6 i - entry lower 6 i are positive at every position: no sign change.