Bugeaud Collection of Conjectures and Open Questions: Pisot orbits on the Cantor set

Read formalization.yaml

authors

Ralf Stephan

method

agent — claude-fable-5, claude-opus-5

review

unchecked

axioms

Classical.choice, Quot.sound, propext

sorry

0 unproved goals declared

results

17 main results named, checked with Comparator, with an alignment table

sources

Machine-written notes on Bugeaud Problem 61 — other, authors participated; Distribution Modulo One and Diophantine Approximation — background, authors not-contacted; Nombres normaux. Applications aux fonctions pseudo-aléatoires — background, authors n/a; Dimension, entropy and Lyapunov exponents — background, authors n/a

divergences

Theorem A(i) is compared in the unbundled form, with Measure.map and an explicit IsProbabilityMeasure hypothesis, rather than through the bundled ProbabilityMeasure statement of the development: the bundled type mentions a measurability proof and would drag some fifteen further proofs into the compared closure. The Σ₁ wrapper that the notes put around Corollary 3.2 is prose; what is compared is the pressure bracket it runs on. The most material divergence concerns degree. The notes state Theorem C(i) for a Pisot number of degree d ≥ 2, and state Theorem C(iii) as "an explicit infinite family in every degree on which 10.61 holds in the strong form". The Lean form of C(i), BB61.QuadSetup.not_equidistributed_of_routeAExponent_lt_one, is quantified over a BB61.QuadSetup and so covers degree two only, and C(iii) is formalized as three ingredients — the Pisot property, the conjugate bound, and a conditional numerical inequality giving A < 1 — with no formalized step from them to non-equidistribution above degree two. The registry account follows the development, not the notes. At degree two the family's members are quadratic setups and the development does package the conclusion, as BB61

checked by

Palomar