A Sturmian Cumulative Bound Fails

Abstract

Refute the cumulative Sturmian bound at slope two minus square root three.

Definition 1.1 (The maximum progression length).

$$\forall (\alpha :\mathbb{R}),\forall (d:\mathbb{N}),mapLength\left(\alpha ,d\right)=({\mathrm{iSup}}_{i:\mathbb{N}}{\mathrm{iSup}}_{a:Bool}{\mathrm{iSup}}_{\ell :\mathbb{N}}{\mathrm{iSup}}_{(0<\ell \wedge (\forall (k:\mathbb{N}),(k<\ell )\Rightarrow (lowerMechanicalWord\left(\alpha ,\alpha ,i+k\cdot d\right)=a)))}(\ell :\mathrm{WithTop}\left(\mathbb{N}\right)))$$

Formalization. D5/S1/Words/SturmianMapCumulativeRefutation.mapLength (✓ std3).

Citation. Gandhar Joshi (2025). Automatic sequences from algebraic, dynamical, and computational perspectives. DOI: 10.21954/ou.ro.00106631. URL: https://oro.open.ac.uk/106631/.

Commentary.

Joshi, Definitions 2.6.1–2.6.2, pp. 27–28: “When a symbol a in a sequence x repeats ℓ times with a difference d, we call it a monochromatic arithmetic progression of difference d and length ℓ. That is, for some i ≥ 0, x_i = x_{i+d} = ⋯ = x_{i+(ℓ−1)d} = a.” “A_x(d) = max{ℓ | there is a MAP of difference d and length ℓ in x}” “Here, we have A_x(d) = ∞ if no finite maximum exists.” The displayed nested iSup ranges over natural starts i, Boolean letters a, natural lengths ℓ, and the proposition that the length is positive and every sample has letter a. Its value is in ℕ∞, so unbounded lengths have value infinity.

Definition 2.2.3, p. 12: “Let α ∈ [0, 1) be an irrational number. Let the interval [0, 1) be partitioned into I_a := [0, 1 − α) and I_b := [1 − α, 1). The n-th term of a Sturmian sequence s = (sₙ)ₙ≥0 is defined by sₙ = a if ⟨(n + 1)α⟩ ∈ I_a, b if ⟨(n + 1)α⟩ ∈ I_b.” The existing lowerMechanicalWord has slope and intercept α. True represents b, false represents a, and the first word index is zero. The fractional coordinate is Int.fract ((n+1)α).

Definition 1.2 (The stronger cumulative comparison).

$$claim=(\forall (\alpha :\mathbb{R}),(Irrational\left(\alpha \right))\Rightarrow ((0<\alpha )\Rightarrow ((\alpha <\frac{1}{2})\Rightarrow (\forall (n:\mathbb{N}),(1\le n)\Rightarrow (\forall (q:\mathbb{N}),((q:\mathbb{R})=(\mathrm{GenContFract}.\mathrm{of}\left(\alpha \right)).\mathrm{dens}\left(n\right))\Rightarrow (\forall (d:\mathbb{N}),(1\le d)\Rightarrow ((d\le q)\Rightarrow (mapLength\left(\alpha ,d\right)\le mapLength\left(\alpha ,q\right)))))))))$$

Formalization. D5/S1/Words/SturmianMapCumulativeRefutation.claim (✓ std3).

Citation. Gandhar Joshi (2025). Automatic sequences from algebraic, dynamical, and computational perspectives. DOI: 10.21954/ou.ro.00106631. URL: https://oro.open.ac.uk/106631/.

Commentary.

Joshi, §6.1, p. 118, “Stronger cumulative bound on A(d).” “The data generated by the A(d) formulae in Corollary 4.3.13 heuristically directs to a conjecture that for every n ∈ N, d ≤ qₙ ⟹ A(d) ≤ A(qₙ) (Proposition 4.4.4) could be true for all g(d). As done for the specific case in [32, Corollary 4.17], this possibility for all Sturmians will be assessed in the author’s future work.” Chapter 4 takes irrational 0 < α < 1/2. The positive integers n and d are encoded by natural numbers at least one. The natural q equals the real-valued convergent denominator (GenContFract.of α).dens n; dens 0 = 1 and dens 1 = a₁. The comparison ranges over all positive differences d at most q.

Theorem 1.3 (Refutation at the first convergent).

$$\neg (\forall (\alpha :\mathbb{R}),(Irrational\left(\alpha \right))\Rightarrow ((0<\alpha )\Rightarrow ((\alpha <\frac{1}{2})\Rightarrow (\forall (n:\mathbb{N}),(1\le n)\Rightarrow (\forall (q:\mathbb{N}),((q:\mathbb{R})=(\mathrm{GenContFract}.\mathrm{of}\left(\alpha \right)).\mathrm{dens}\left(n\right))\Rightarrow (\forall (d:\mathbb{N}),(1\le d)\Rightarrow ((d\le q)\Rightarrow (mapLength\left(\alpha ,d\right)\le mapLength\left(\alpha ,q\right)))))))))$$

Proof. Machine-checked in Lean as D5/S1/Words/SturmianMapCumulativeRefutation.result (✓ std3). ∎

Resolves. Problems/joshi-2025-sturmian-map-cumulative-bound (refuted) by D5/S1/Words/SturmianMapCumulativeRefutation.result.

Source. Repository-derived.

Acknowledgement. Gandhar Joshi (2025). Automatic sequences from algebraic, dynamical, and computational perspectives. DOI: 10.21954/ou.ro.00106631. URL: https://oro.open.ac.uk/106631/.

Commentary.

Take α = 2 − √3, n = 1, q = 3 and d = 2. The slope is irrational and lies in (0,1/2); its inverse is 2 + √3 and its first convergent denominator is 3. The letters at positions 1,3,5,7,9 are false, so mapLength α 2 is at least 5. For difference 3, the fractional orbit moves backwards by g = 3√3 − 5. An equal-letter run cannot wrap across the other letter’s interval. Four steps exceed the false-letter interval, and two exceed the true-letter interval. Thus every start, either letter, and every admissible length contribute at most 4 to mapLength α 3. The asserted comparison would imply 5 ≤ 4.

Proposition 4.4.4 retains the hypothesis g(d) ≤ α, where g(d) = min{⟨dα⟩, 1 − ⟨dα⟩}; this stronger assertion removes that restriction. The refutation does not assert exact maxima, an interval family, or any change to the Fibonacci special case.

References

• Truth anchor: D5/S1/Words/SturmianMapCumulativeRefutation.claim
• Truth anchor: D5/S1/Words/SturmianMapCumulativeRefutation.mapLength
• Truth anchor: D5/S1/Words/SturmianMapCumulativeRefutation.result
• Dependency: D5/S1/Words/FibonacciMapFirstStart
• Dependency: D5/S1/Words/Mechanical/MechanicalBalance