BinaryAmplification.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Binary charge amplification and integer rounding

An integer within a constant factor of exp D has binary length linear in D. Rational Taylor sums compute this scale with explicit positive-integer charge rounding bounds.

def OAI.ContinuumCoulomb.binaryAmplification line 20
theorem OAI.ContinuumCoulomb.binaryAmplification_pos line 22
theorem OAI.ContinuumCoulomb.binaryAmplification_ge_scale line 25
theorem OAI.ContinuumCoulomb.binaryAmplification_bounds line 28
theorem OAI.ContinuumCoulomb.binaryAmplification_bit_length line 34
Source documentation
Exponentially large charges still have only linearly many binary digits.
```
theorem binaryAmplification_bit_length (D : ℕ) :
    Nat.size (binaryAmplification D) ≤ 2 * D + 2 := by
…
```
Mentions: OAI.ContinuumCoulomb.binaryAmplification
def OAI.ContinuumCoulomb.rationalRoundedScaledCharge line 55
Source documentation
Rational rounding used by the charge-output algorithm.
```
def rationalRoundedScaledCharge (Z : ℕ) (q : ℚ) : ℕ := (round ((Z : ℚ) * q)).toNat
```
def OAI.ContinuumCoulomb.roundedScaledCharge line 57
theorem OAI.ContinuumCoulomb.rationalRoundedScaledCharge_eq line 60
theorem OAI.ContinuumCoulomb.roundedScaledCharge_pos line 65
theorem OAI.ContinuumCoulomb.roundedScaledCharge_error line 74
Source documentation
Rounding the physical charge first incurs only inverse-amplification error in the dilated one-particle potential.
```
theorem roundedScaledCharge_error {Z : ℕ} (hZ : 0 < Z) {q : ℝ}
    (hscale : 1 ≤ (Z : ℝ) * q) :
    |(roundedScaledCharge Z q : ℝ) / (Z : ℝ) - q| ≤ 1 / (2 * (Z : ℝ)) := by
…
```
Mentions: OAI.ContinuumCoulomb.roundedScaledCharge