NuclearCoordinates.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit rational rounding and distinctness

Rounding on a common rational grid controls the approximation error and preserves pairwise distinctness of separated nuclear positions.

def OAI.ContinuumCoulomb.roundCoordinate line 16
def OAI.ContinuumCoulomb.roundPosition line 19
theorem OAI.ContinuumCoulomb.roundCoordinate_error line 23
Source documentation
A common denominator bounds each coordinate error, also for negative data.
```
theorem roundCoordinate_error {denominator : ℕ} (hdenom : 0 < denominator) (x : ℝ) :
    |(roundCoordinate denominator x : ℝ) - x| ≤ 1 / (denominator : ℝ) := by
…
```
Mentions: OAI.ContinuumCoulomb.roundCoordinate
theorem OAI.ContinuumCoulomb.roundPosition_error line 39
Source documentation
A deliberately coarse Euclidean bound suffices for the rounding budget.
```
theorem roundPosition_error {denominator : ℕ} (hdenom : 0 < denominator) (x : Position) :
    ‖realPosition (roundPosition denominator x) - x‖ ≤ 3 / (denominator : ℝ) := by
…
```
Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.realPosition, OAI.ContinuumCoulomb.roundPosition

theorem OAI.ContinuumCoulomb.roundPosition_injective line 61

Source documentation

Rounding preserves distinct nuclei when the common grid is finer than one sixth of every original pair separation.

theorem roundPosition_injective {m denominator : ℕ} (hdenom : 0 < denominator)
    (position : Fin m → Position)
    (hsep : ∀ i j, i ≠ j → 6 / (denominator : ℝ) < ‖position i - position j‖) :
    Function.Injective (fun i => roundPosition denominator (position i)) := by
…

Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.roundPosition