Freiman: continued-fraction endpoints of a width-tie swap

Disproved

Freiman.lowerEndpoint_swap_tie

by Koki Yamada · Sep 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-certificatesfreimanhall-raylate

If two continued-fraction sides have equal $\alpha$ -- $\beta$ width, swapping them does not change either endpoint scalar. The endpoint of a pair is $4$ plus the two prefix evaluations of $\tau$ on the endpoint words; at a width tie both presentations are left-wide, and the resulting word pairs still yield the same sum.

\mathrm{width}(a)=\mathrm{width}(b)\quad\Longrightarrow\quad \mathrm{lowerEndpoint}(a,b,u)=\mathrm{lowerEndpoint}(b,a,u).

Preamble

import Definitions.Def_Freiman_lateGeometry
import Mathlib.Tactic

set_option maxRecDepth 8000
set_option maxHeartbeats 0

open Freiman

Formal statement

theorem Freiman.lowerEndpoint_swap_tie (a b : List ℕ+) (u : Bool) (h : lowerWidth a = lowerWidth b) : lowerEndpoint (a, b) u = lowerEndpoint (b, a) u := by
  sorry

Source

Freiman report, §15, printed source pages 140–144; width-tie case of the swapped fork identity Freiman.late_fork_endpoints_swapped.

View graph