Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

bibkey: ralfstephan2026subspacetheorems authors: Ralf Stephan year: 2026 title: Subspace-Theorems doi: null url: https://github.com/rwst/Subspace-Theorems/tree/bfd830f481b296989fa5f0c1e48d9316f72270d8 claim: Formal Lean development of arithmetic heights, Roth approximation, and Thue equations over number fields. strata_touched:

  • D5/S3/Arith/AbsoluteValues/Heights/PseudoBasisMetrics
  • D5/S3/Arith/DiophantineApproximation/RothTheorem
  • D5/S3/Arith/DiophantineApproximation/ThueEquation license: Apache-2.0 triage: anchor

Subspace-Theorems

Ralf Stephan’s Lean source develops arithmetic heights and the approximation machinery leading to Roth’s theorem and finite fibers of Thue equations. The canonical projection uses the pinned source revision below; its adapted Lean files retain the upstream copyright and Apache-2.0 notices. The repository README describes its roadmaps as preliminary, so the source declarations and their exact hypotheses govern each formal claim.

Verified locator

  • Repository: https://github.com/rwst/Subspace-Theorems
  • Pinned source: https://github.com/rwst/Subspace-Theorems/tree/bfd830f481b296989fa5f0c1e48d9316f72270d8
  • Immutable revision: bfd830f481b296989fa5f0c1e48d9316f72270d8
  • Author at the pinned commit: Ralf Stephan.
  • License at the pinned revision: Apache-2.0. The upstream LICENSE and the downloaded source copy have the same SHA-256: b40930bbcf80744c86c46a12bc9da056641d722716c378f5659b9e555ef833e1.
  • Representative original author notice: DiophantineApproximation/ThueEquation.lean credits Ralf Stephan and says it is released under Apache 2.0.

The note identifies the source and license. It does not certify that a local canonical projection has compiled or that every donor statement is admissible as new mathematical content in this repository.