Roth Moving Chain

Abstract

A long moving chain of sufficiently strong approximants is impossible.

Theorem 1.1 (Roth Moving Chain).

Lean statement: D5/S3/Arith/DiophantineApproximation/RothMovingChain.roth_no_moving_chain_aux

Proof. Machine-checked in Lean as D5/S3/Arith/DiophantineApproximation/RothMovingChain.roth_no_moving_chain_aux (✓ std3). ∎

Citation. Ralf Stephan (2026). Subspace-Theorems. URL: https://github.com/rwst/Subspace-Theorems/tree/bfd830f481b296989fa5f0c1e48d9316f72270d8.

Commentary.

A long moving chain of sufficiently strong approximants is impossible.

References

• Truth anchor: D5/S3/Arith/DiophantineApproximation/RothMovingChain.roth_no_moving_chain_aux
• Dependency: D5/S3/Arith/AbsoluteValues/Heights/AbsoluteScalarHeight
• Dependency: D5/S3/Arith/DiophantineApproximation/PlacesOverFinite
• Dependency: D5/S3/Arith/DiophantineApproximation/PlacesOverInfinite
• Dependency: D5/S3/Arith/DiophantineApproximation/RothAuxiliary
• Dependency: D5/S3/Arith/DiophantineApproximation/RothKeyInequality