Books·books:BugeaudDistributionModuloOne/Problem10_61
Bugeaud Collection of Conjectures and Open Questions: Pisot orbits on the Cantor set
Machine-checked by Palomar.
Fidelity F2: The correspondence is declared through a Comparator challenge, an alignment table and written divergences.
AI activity
How grades workNo AI contribution recorded against this statement.
Does the formal statement say what was claimed?
F2 declared The correspondence is declared through a Comparator challenge, an alignment table and written divergences.
Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.
Checks
1-
verified Palomar
Registered by Palomar at d61132ff: Comparator confirmed 17 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel
Declared by the projects
1Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict it.
Lean formalization toward Bugeaud Problem 10.61
- 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
Follow and discuss
All discussionGet an email when this problem moves
A new claim, a check, a bounty or a discussion. One link to confirm, one click to stop.
Discussion and bounties for this problem load here.
Formal material
Formal statements · 1
Cited proofs · 4
- rwst/Pisot-Cantor-61/blob/a464f1cd3c8d14229a2f1d7881773987446d0df0/BB61/Criterion.lean#L230
- rwst/Pisot-Cantor-61/blob/a464f1cd3c8d14229a2f1d7881773987446d0df0/BB61/GapSqrtThree.lean#L298
- rwst/Pisot-Cantor-61/blob/a464f1cd3c8d14229a2f1d7881773987446d0df0/BB61/RouteA.lean#L163
- rwst/Pisot-Cantor-61/blob/a464f1cd3c8d14229a2f1d7881773987446d0df0/BB61/RouteANormalForm.lean#L283
Also known as · 2
- https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_61.lean
- FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_61.lean