OAI/NumberTheory/EgyptianFractions/SampledDenominatorCertificate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.RandomProducts.eventually_sampled_denominator_certificate line 17

   Source documentation

   An unconditional arithmetic certificate in the actual sample coordinates. The prime pool and deterministic injective vector are chosen first. Every subsequent collection of the thousand Boolean sample blocks has one common auxiliary denominator with the required window and binary factor. Thus a Fourier-good realization can be used without resampling or identifying any repeated product values.

   theorem eventually_sampled_denominator_certificate :
       ∀ᶠ S : ℝ in atTop,
         S ^ 99 ≤ ((widePrimePool (S ^ 100)).card : ℝ) ∧
         (∀ q ∈ widePrimePool (S ^ 100),
           Nat.Prime q ∧ S ^ 100 < (q : ℝ) ∧ (q : ℝ) ≤ S ^ 101) ∧
         ∃ p : Fin (blockLength S) → ℕ,
           Function.Injective p ∧
           (∀ j, Nat.Prime (p j) ∧ S ^ 100 < (p j : ℝ) ∧ (p j : ℝ) ≤ S ^ 101) ∧
           Function.Injective (ResidueConstruction.subsetEntry p) ∧
           ∀ f : Fin 1000 → ((Fin (blockLength S) × Bool) → widePrimePool (S ^ 100)),
             ∃ M : ℕ, Real.exp S < (M : ℝ) ∧
               (M : ℝ) ≤ Real.exp (204204 * S) ∧
   …

   Mentions: OAI.Problem337.widePrimePool, OAI.Problem337.RandomProducts.blockLength, OAI.Problem337.ResidueConstruction.subsetEntry