NumericalWork.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Concrete numerical representation and arithmetic work

These are integer bit-length and exact rational-operation bounds for the finite optimizer. They are not a RAM theorem: the costed evaluator below counts rational arithmetic operations, while bit-operation costs also require the charged evaluation model used by the surrounding algorithm.

def OAI.EditApproximation.rationalEncodingBits line 19
Source documentation
Signed numerator plus positive denominator encoding length.
```
def rationalEncodingBits (r : ℚ) : ℕ := Nat.size r.num.natAbs + Nat.size r.den + 1
```
theorem OAI.EditApproximation.natural_product_bit_length line 21
theorem OAI.EditApproximation.natural_sum_bit_length line 30
theorem OAI.EditApproximation.natural_power_bit_length line 40
theorem OAI.EditApproximation.natural_finite_product_bit_length line 49
theorem OAI.EditApproximation.rational_finite_sum_denominator line 61
Source documentation
Denominator of a finite rational sum divides the product of the individual denominators.
```
theorem rational_finite_sum_denominator {ι : Type*} (s : Finset ι) (values : ι → ℚ) :
    (∑ i ∈ s, values i).den ∣ ∏ i ∈ s, (values i).den := by
…
```
theorem OAI.EditApproximation.logarithm_parameter_denominator line 72
Source documentation
The symmetric logarithm parameter has a denominator bounded by the input's numerator/denominator height.
```
theorem logarithm_parameter_denominator (r : ℚ) :
    ((r - 1) / (r + 1)).den ≤ r.num.natAbs + r.den := by
…
```
theorem OAI.EditApproximation.logarithm_parameter_bit_length line 93
def OAI.EditApproximation.logarithmDenominatorBudget line 98
theorem OAI.EditApproximation.sum_odd_logarithm_exponents line 101
theorem OAI.EditApproximation.rationalLogApproximation_denominator line 109
Source documentation
A concrete unreduced denominator for every finite logarithm sum. The exponent K² is deliberately loose and keeps the proof elementary.
```
theorem rationalLogApproximation_denominator (r : ℚ) (K : ℕ) :
    (rationalLogApproximation r K).den ∣ logarithmDenominatorBudget r K := by
…
```
Mentions: OAI.EditApproximation.rationalLogApproximation, OAI.EditApproximation.logarithmDenominatorBudget
theorem OAI.EditApproximation.logarithmDenominatorBudget_positive line 132
theorem OAI.EditApproximation.rationalLogApproximation_denominator_bit_length line 139
Source documentation
Polynomial bit length of the actual logarithm denominator in the input encoding length and truncation count.
```
theorem rationalLogApproximation_denominator_bit_length (r : ℚ) (K : ℕ) :
    Nat.size (rationalLogApproximation r K).den ≤
      K * K * rationalEncodingBits r + K * Nat.size (2 * K + 1) + 2 := by
…
```
Mentions: OAI.EditApproximation.rationalLogApproximation, OAI.EditApproximation.rationalEncodingBits
def OAI.EditApproximation.rationalPowerWithWork line 160
Source documentation
Costed repeated multiplication, counting one rational multiplication at each successor.
```
def rationalPowerWithWork (r : ℚ) : ℕ → ℚ × ℕ
  | 0 => (1, 0)
  | n + 1 => let previous := rationalPowerWithWork r n
…
```
theorem OAI.EditApproximation.rationalPowerWithWork_spec line 165
def OAI.EditApproximation.rationalLogPartialWithWork line 173
Source documentation
The direct finite logarithm summation, with every power, division and addition counted.
```
def rationalLogPartialWithWork (b : ℚ) : ℕ → ℚ × ℕ
  | 0 => (0, 0)
  | K + 1 =>
    let previous := rationalLogPartialWithWork b K
…
```
theorem OAI.EditApproximation.rationalLogPartialWithWork_spec line 180
def OAI.EditApproximation.rationalLogApproximationWithWork line 192
Source documentation
Three operations form the logarithm parameter, and one final multiplication doubles the partial sum.
```
def rationalLogApproximationWithWork (r : ℚ) (K : ℕ) : ℚ × ℕ :=
…
```
theorem OAI.EditApproximation.rationalLogApproximationWithWork_spec line 198
Source documentation
The actual logarithm evaluator uses exactly a quadratic number of rational arithmetic operations and returns the already verified value.
```
theorem rationalLogApproximationWithWork_spec (r : ℚ) (K : ℕ) :
    rationalLogApproximationWithWork r K =
      (rationalLogApproximation r K, K * K + 2 * K + 4) := by
…
```
Mentions: OAI.EditApproximation.rationalLogApproximationWithWork, OAI.EditApproximation.rationalLogApproximation
theorem OAI.EditApproximation.rationalLogApproximation_abs_bound line 205
Source documentation
Every logarithm series term is bounded on nonnegative inputs; this controls the returned numerator without transcendental arithmetic.
```
theorem rationalLogApproximation_abs_bound (r : ℚ) (K : ℕ) (hr : 0 ≤ r) :
    |rationalLogApproximation r K| ≤ 2 * K := by
…
```
Mentions: OAI.EditApproximation.rationalLogApproximation
theorem OAI.EditApproximation.rational_numerator_bound line 233
theorem OAI.EditApproximation.rationalLogApproximation_encoding_bit_length line 246
Source documentation
Polynomial bit-length bound for both numerator and denominator of all actually returned logarithm approximations.
```
theorem rationalLogApproximation_encoding_bit_length (r : ℚ) (K : ℕ) (hr : 0 ≤ r) :
    rationalEncodingBits (rationalLogApproximation r K) ≤
      2 * (K * K * rationalEncodingBits r + K * Nat.size (2 * K + 1) + 2) +
        Nat.size (2 * K) + 1 := by
…
```
Mentions: OAI.EditApproximation.rationalEncodingBits, OAI.EditApproximation.rationalLogApproximation
theorem OAI.EditApproximation.optimizerMixtureWeight_denominator line 261
Source documentation
Stored mixture coefficients use a denominator dividing K(K+1); there is no growth with the number of earlier optimizer updates.
```
theorem optimizerMixtureWeight_denominator (K j : ℕ) (hK : 0 < K) :
    (optimizerMixtureWeight K j).den ∣ K * (K + 1) := by
…
```
Mentions: OAI.EditApproximation.optimizerMixtureWeight
theorem OAI.EditApproximation.optimizerMixtureWeight_bit_length line 273

theorem OAI.EditApproximation.rationalOptimizerIterate_denominator_bit_length line 284

Source documentation

Every actual rational iterate has a polynomial denominator bit length in its trace length and the listed vertices' input bit bound.

theorem rationalOptimizerIterate_denominator_bit_length {ι : Type*}
    (initial : ι → ℚ) (selected : ℕ → ι → ℚ) (K B : ℕ) (hK : 0 < K) (i : ι)
    (hinput : ∀ j ∈ range K, Nat.size (selected j i).den ≤ B) :
    Nat.size (rationalOptimizerIterate initial selected K i).den ≤
      K * (2 * Nat.size K + 2 + B) + 1 := by
…

Mentions: OAI.EditApproximation.rationalOptimizerIterate