Metadata

slug: joshi-2025-sturmian-map-cumulative-bound
bibkey: joshi2025sturmian
doi: 10.21954/ou.ro.00106631
url: https://oro.open.ac.uk/106631/
triage: theorem
motivation_gids:
  - D5/S1/Words/SturmianMapCumulativeRefutation

A stronger cumulative Sturmian progression bound is false

Problem

Gandhar Joshi, Automatic sequences from algebraic, dynamical, and computational perspectives, Open University PhD thesis, §6.1, p. 118:

“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.”

The literal conjecture quantifies over irrational $0 < α < 1/2$ , positive $n$ , the convergent denominator $q_{n}$ , and $1 \leq d \leq q_{n}$ . Preregistration: https://github.com/the-omega-institute/trureturing/issues/17837.

Statement echo

Source clause	Formal counterpart	Fidelity
Definition 2.2.3: the letter at $n$ uses ${(n + 1) α}$ and intervals $[0, 1 - α)$ , $[1 - α, 1)$	`lowerMechanicalWord α α`; private `sturmian_letter_iff`	Same indexing and intercept; true is the second letter.
Definitions 2.6.1–2.6.2: all starts, either letter, positive finite lengths, infinity if unbounded	`mapLength`	Full nested supremum in $N \cup {\infty}$ .
Irrational slope in Chapter 4’s $0 < α < 1/2$	`claim` slope hypotheses	Literal domain.
Every positive $n$ , with $q_{0} = 1$ and $q_{1} = a_{1}$	`1 ≤ n`, `(GenContFract.of α).dens n`	Natural index and real denominator, identified with natural $q$ .
Every positive $d \leq q_{n}$ has $A (d) \leq A (q_{n})$	The final quantified implication of `claim`	No additional condition on $g (d)$ .
Refutation	`result : ¬ claim`	Witness $α = 2 - 3$ , $n = 1$ , $q = 3$ , $d = 2$ .

Motivation

The source already proves the retained-hypothesis version with $g (d) \leq α$ (Proposition 4.4.4). Its unrestricted version would order all shorter differences by a convergent denominator. The published Fibonacci special case does not assert this comparison for arbitrary slopes.

Gap

A long progression in a prefix alone cannot bound all starts. The required counterexample needs both a concrete longer progression at $d = 2$ and a uniform upper bound for difference $3$ , with the same slope, word and indexing.

Route

For $α = 2 - 3$ , exact square-root inequalities give $0 < α < 1/2$ and $1/ α = 2 + 3$ , hence $q_{1} = 3$ . Positions $1, 3, 5, 7, 9$ all have the first letter, so $A (2) \geq 5$ . At difference $3$ , the fractional orbit moves backwards by $g = 33 - 5$ . The proof uses the published FibonacciMapFirstStart.open_rotation_run to exclude wrapping inside either open symbol interval. Irrationality excludes both endpoints. Since $4 g > 1 - α$ and $2 g > α$ , every progression has length at most four. Thus the asserted comparison would imply $5 \leq 4$ .

Falsifier

An indexing or word-correspondence mismatch, or a five-term equal-letter run of difference $3$ at this slope, would invalidate this refutation. The formal statement quantifies every start, both letters and every positive length; its upper bound is independent of a prefix cutoff or numerical approximation.

Evidence

Formal module: D5/S1/Words/SturmianMapCumulativeRefutation.lean.
Settling declaration: D5.S1.Words.SturmianMapCumulativeRefutation.result.
Supporting private declarations: slope_range, slope_irrational, denominator_one, five_letters, mapLength_two_ge_five, mapLength_three_le_four; the latter bounds every start and both letters.
mapLength and claim retain the literal preregistered expressions. The word reuses the existing mechanical-word owner. The natural-valued, golden-specific goldenMAPMaximum does not supply the general-slope, extended-natural supremum.
The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.
The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).
Escape audit unfinished for the published owner D5.S1.Words.FibonacciMapFirstStart.open_rotation_run: https://github.com/the-omega-institute/trureturing/issues/19343. No Reg registration or declared_validated status is asserted.

Experiment

The pinned numerical check contains check.py, SHA-256 9c52d0b0f4b9daa6ca007ca6a960aba5d77b231f7728a9eb61bac714668a9d0c. Command from that directory: python3 check.py; rerun exit 0, ALL_OK. The computation checks exact integer certificates; scans $4000$ letters at $2 - 3$ ; compares circle calculations and brute force at five slopes for $1 \leq d \leq 40$ ; scans convergents with $q_{n} \leq 250$ ; and tests the periodic families below with $q_{n} \leq 700$ . These are computed readings, not uniform Lean conclusions.

Triage

What the settlement shows

Item	Status and evidence	Scope and boundary
Literal stronger cumulative conjecture	Kernel-checked: `result` refutes `claim`.	One counterexample settles the universal claim.
Concrete witness and necessary bounds	Kernel-checked: private `slope_range`, `slope_irrational`, `denominator_one`, `mapLength_two_ge_five`, `mapLength_three_le_four`.	$α = 2 - 3$ , $q_{1} = 3$ , $A (2) \geq 5$ , $A (3) \leq 4$ .
Wrong convergent indexing	Kernel-checked: `denominator_one`; transient fidelity checks apply `GenContFract.zeroth_den_eq_one` and `GenContFract.first_den_eq`.	$q_{0} = 1$ and $q_{1} = a_{1} = 3$ .
Wrong word intercept or index	Kernel-checked: private `sturmian_letter_iff`.	Source coordinate ${(n + 1) α}$ , intercept $α$ .
Prefix-only upper bound	Kernel-checked: private `mapLength_three_le_four`.	Every start, either Boolean letter, every admissible length.
Floating-point proof	Kernel-checked arithmetic in the named private lemmas.	Exact rational bounds and `Real.sqrt`; no floating-point premise.
Failure mechanism	Proved in prose: $g (2) = 1 - 2 α > α$ , since $α < 1/3$ and $2 α > 1/2$ .	This is precisely the regime omitted by the retained-hypothesis proposition. The two-cluster explanation does not assert a uniform formula.
Nearest surviving source statements	Literature reading: Proposition 4.4.4 retains $g (d) \leq α$ ; Joshi–Rust Corollary 4.17 gives the Fibonacci case.	Neither is refuted here; neither is on this module’s proof dependency path.
Exact maxima and first longest start	Computed by the pinned experiment: $A (1), A (2), A (3) = 3, 8, 4$ on $4000$ letters; first eight-term first-letter progression at difference $2$ starts at $12$ .	Exact global equalities are not proved in this module.
Level-1 failure interval	Computed on $1 0^{4}$ grid points in $(1/4, 1/3)$ : fraction $0.4286$ , largest violating point $0.285709$ .	The uniform interval $(1/4, 2/7)$ classification is open here.
Further failing levels	Computed for $q_{n} \leq 250$ : at $2 - 3$ , levels $1, 5$ ; at $(14 - 26) /34$ , levels $1, 3, 4, 7$ .	Infinite recurrence is open here. At level $5$ of the first slope: $q = 41$ , $d = 28$ , values $92 > 52$ .
Constant-factor repair	Computed for $B = 4, 6, 8, 12$ in $[0; 3, \overline{1, B, 1}]$ , $q_{n} \leq 700$ : observed largest ratios $3.0, 4.256, 5.559, 8.193$ .	No uniform unbounded-ratio theorem is proved; absence of every constant-factor repair is open here.
Typical slopes	Computed: $197$ of $400$ sampled slopes in $(0, 1/2)$ violate at a level with $q_{n} \leq 60$ .	An almost-everywhere or density statement is open.
Source formula comparison	Computed: $744$ mismatches in $7258$ sampled pairs; at $α = (83 - 6) /28$ , $d = 4$ , source formula $7$ , circle computation and $150000$ -letter brute-force scan $15$ .	The settlement uses neither Corollary 4.3.13 nor Theorem 4.3.9. General correction of those formulas is open.
Negative controls	Computed: no violation in the scan for ${5}$ or $(3 - 5) /2$ , or among tested $g (d) \leq α$ cases.	Finite checks alone do not prove their uniform versions.
Literature settlement screen	Literature reading: no prior settlement located in the recorded partial screen.	Completeness `ASSUMED-UNVERIFIED`.
Optional extensions	Open: full continued fraction, exact global maxima, density, interval-family classification, infinite levels and uniform ratio growth.	None is required for `result`.

The refutation removes the unrestricted conjecture as a possible general theorem. The source’s retained-hypothesis and Fibonacci statements retain their stated scope; no theorem depending on the unrestricted conjecture is established here.

ASSUMED-UNVERIFIED

Literature completeness is ASSUMED-UNVERIFIED. The recorded screen covers the thesis, Joshi–Rust arXiv:2501.05830v2 and later author papers 2506.13337v1, 2507.16956v2 and 2604.02404v2. Rate-limited citation searches, unindexed works and inaccessible citation coverage prevent an exhaustive absence claim. Finite computations do not establish any of the uniform extensions marked open.

Keyboard shortcuts

trureturing — Discovering truth