Two integer frieze patterns of width 12 whose rows 6 differ with exactly two sign changes

Continuation of Formalizations.Combinatorics.Frieze.IntegerDominance (same conventions: entry a k i is the continuant of a_i, …, a_{i+k-1}, indices modulo n = a.length). For width w = 12 (n = 15), row 6 = ⌊w/2⌋ lies inside the printed range 1 ≤ k ≤ [w/2] of Problem 1 of S. Tabachnikov (A four-vertex theorem for frieze patterns?, Math. Intelligencer 40 (2018)). We record two integer Conway–Coxeter friezes of width 12 whose row-6 differences have no zero and exactly two cyclic sign changes, so the answer to the question is negative for integer friezes within the printed range too. An exhaustive search found 480 such pairs at width 12 and none, in any row k ≤ ⌊w/2⌋, at smaller widths. The verification is a finite computation checked by the kernel (decide +kernel).

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

The difference of row k of the friezes with quiddities b and a, at position i.

Equations

• Frieze.rowDiff a b k i = Frieze.entry b k i - Frieze.entry a k i

def Frieze.signChanges (a b : List ℤ) (k : ℕ) : ℕ

The number of cyclic positions i < a.length where the row-k difference changes sign strictly.

Equations

• Frieze.signChanges a b k = (List.filter (fun (i : ℕ) => decide (Frieze.rowDiff a b k i * Frieze.rowDiff a b k ((i + 1) % a.length) < 0)) (List.range a.length)).length

def Frieze.lower12 : List ℤ

First quiddity of width 12.

Equations

• Frieze.lower12 = [1, 2, 2, 2, 2, 3, 1, 4, 2, 1, 4, 2, 2, 1, 10]

def Frieze.upper12 : List ℤ

Second quiddity of width 12.

Equations

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

theorem Frieze.isQuiddity_lower12 : IsQuiddity lower12

theorem Frieze.isQuiddity_upper12 : IsQuiddity upper12

theorem Frieze.rowDiff_six_ne_zero (i : ℕ) : i < 15 → rowDiff lower12 upper12 6 i ≠ 0

The row-6 differences are (1, 1, 2, 7, 1, 1, 1, 1, 9, -8, -9, 3, 7, 3, 2): no zero.

theorem Frieze.signChanges_six : signChanges lower12 upper12 6 = 2

theorem Frieze.signChanges_five : signChanges lower12 upper12 5 = 5

Control: the counter is not degenerate; row 5 of the same pair has five sign changes.

theorem Frieze.exists_two_sign_changes_width_twelve : ∃ (a : List ℤ), ∃ (b : List ℤ), IsQuiddity a ∧ IsQuiddity b ∧ a.length = 15 ∧ b.length = 15 ∧ (∀ (i : ℕ), i < 15 → rowDiff a b 6 i ≠ 0) ∧ signChanges a b 6 = 2

Two integer Conway–Coxeter friezes of width 12 whose rows 6 = ⌊12/2⌋ differ with no zero and exactly two cyclic sign changes.