OAI/NumberTheory/EgyptianFractions/ResidueDenominatorCertificate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.ResidueConstruction.eventually_residue_denominator_certificate line 16

   Source documentation

   Uniform arithmetic certificate for the common residue denominator. The deterministic prime vector is chosen before the random blocks. Every realization with the stated factor bounds has a suitable common denominator; there is no prime-density, floor-scale, or logarithmic-size premise left.

   theorem eventually_residue_denominator_certificate :
       ∀ᶠ S : ℝ in atTop,
         ∃ p : Fin (ResidueLevels.scale S) → ℕ,
           Function.Injective p ∧
           (∀ j, Nat.Prime (p j) ∧ S ^ 100 < (p j : ℝ) ∧ (p j : ℝ) ≤ S ^ 101) ∧
           Function.Injective (subsetEntry p) ∧
           ∀ q : Fin 1000 → Fin (ResidueLevels.scale S) → Fin 2 → ℕ,
             (∀ i j e, 0 < q i j e) →
             (∀ i j e, (q i j e : ℝ) ≤ S ^ 101) →
             ∃ M : ℕ, Real.exp S < (M : ℝ) ∧
               (M : ℝ) ≤ Real.exp (204204 * S) ∧
               2 ^ ⌈100000 * Real.log S / Real.log 2⌉₊ ∣ M ∧
   …

   Mentions: OAI.Problem337.ResidueLevels.scale, OAI.Problem337.ResidueConstruction.subsetEntry