PrimeChoice.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Choosing the prime after the finite parameters

The field size is chosen after the dimension, direction count, and encoding cost. Infinitude of primes permits all these bounds to be imposed simultaneously, without any upper bound on the prime.

theorem OAI.MetricEntropyDuality.exists_prime_gt_real line 20
Source documentation
A natural prime exceeds every prescribed real bound.
```
theorem exists_prime_gt_real (bound : ℝ) :
    ∃ p : ℕ, p.Prime ∧ bound < (p : ℝ) := by
…
```

theorem OAI.MetricEntropyDuality.exists_prime_after_parameters line 27

Source documentation

All parameters, including the encoding cost, precede the choice of prime.

theorem exists_prime_after_parameters (h u D : ℕ) (C B bound : ℝ) :
    ∃ p : ℕ, p.Prime ∧ bound < (p : ℝ) ∧ h < p ∧
      h ^ 2 * u ^ (2 * h) < p ∧ Real.exp (B * C / (D : ℝ)) < (p : ℝ) := by
…

theorem OAI.MetricEntropyDuality.prime_log_pos line 38

theorem OAI.MetricEntropyDuality.prime_choice_entropy_lt line 44

Source documentation

The exponential lower bound on the prime absorbs the fixed encoding cost.

theorem prime_choice_entropy_lt {p D : ℕ} (hD : 0 < D)
    {B C : ℝ} (hchoice : Real.exp (B * C / (D : ℝ)) < (p : ℝ)) :
    B * C < (D : ℝ) * Real.log (p : ℝ) := by
…

theorem OAI.MetricEntropyDuality.prime_choice_encoding_ratio_lt line 53

Source documentation

Positivity of the encoding cost is not needed for this comparison.

theorem prime_choice_encoding_ratio_lt {p D : ℕ} (hp : p.Prime) (hD : 0 < D)
    {B C : ℝ} (hB : 0 < B)
    (hchoice : Real.exp (B * C / (D : ℝ)) < (p : ℝ)) :
    2 * C / ((D : ℝ) * Real.log (p : ℝ)) < 2 / B := by
…

theorem OAI.MetricEntropyDuality.exists_prime_with_entropy_budget line 66

Source documentation

A single prime satisfies the finite construction and entropy bounds.

theorem exists_prime_with_entropy_budget (h u D : ℕ) (C B bound : ℝ)
    (hD : 0 < D) (hB : 0 < B) :
    ∃ p : ℕ, p.Prime ∧ bound < (p : ℝ) ∧ h < p ∧
      h ^ 2 * u ^ (2 * h) < p ∧ Real.exp (B * C / (D : ℝ)) < (p : ℝ) ∧
      0 < Real.log (p : ℝ) ∧ B * C < (D : ℝ) * Real.log (p : ℝ) ∧
      2 * C / ((D : ℝ) * Real.log (p : ℝ)) < 2 / B := by
…

theorem OAI.MetricEntropyDuality.exists_prime_for_rank line 79
Source documentation
The finite parameters are all fixed before the prime. The caller may impose any additional real lower bound on the prime.
```
theorem exists_prime_for_rank {a : ℝ} (ha : 1 ≤ a) {r : ℕ} (hr : 0 < r)
    (B bound : ℝ) (hB : 0 < B) :
    let h := compressionRadius a
…
```
Mentions: OAI.MetricEntropyDuality.compressionRadius