RawDensityExistence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.eventually_common_residue_lists line 23

Source documentation

The deterministic and sampled lists can use exactly the same Boolean sample space. The deterministic list is chosen before the random realization, and every realization is accommodated by a common bounded denominator. This is an unconditional arithmetic statement, including the prime pool.

theorem eventually_common_residue_lists :
    ∀ᶠ S : ℝ in atTop,
      S ^ 99 ≤ ((widePrimePool (S ^ 100)).card : ℝ) ∧
      (∀ q ∈ widePrimePool (S ^ 100),
        Nat.Prime q ∧ S ^ 100 < (q : ℝ) ∧ (q : ℝ) ≤ S ^ 101) ∧
      ∃ t₀ : (Fin (ResidueLevels.scale S) → Bool) → ℕ,
        Function.Injective t₀ ∧
        ∀ f : Fin 1000 →
            ((Fin (ResidueLevels.scale S) × Bool) → widePrimePool (S ^ 100)),
          ∃ M : ℕ, Real.exp S < (M : ℝ) ∧
            (M : ℝ) ≤ Real.exp (RawDensityParameters.DM * S) ∧
            2 ^ TerminalDepth.binaryExponent RawDensityParameters.D₀ S ∣ M ∧
…

Mentions: OAI.Problem337.widePrimePool, OAI.Problem337.ResidueLevels.scale, OAI.Problem337.RawDensityParameters.DM, OAI.Problem337.TerminalDepth.binaryExponent, OAI.Problem337.RawDensityParameters.D₀

theorem OAI.Problem337.eventually_geometric_high_residue_lists line 54

Source documentation

Actual deterministic residue supply simultaneously on the canonical high levels, with the same Boolean sample type as the random construction.

theorem eventually_geometric_high_residue_lists :
    ∀ᶠ S : ℝ in atTop, ∀ C : ℕ,
      Real.exp (4 * (DM + 2) * S) ≤ (C : ℝ) →
      (C : ℝ) ≤ Real.exp (2 * (4 * (DM + 2)) * S) →
      ∀ t : (Fin (ResidueLevels.scale S) → Bool) → ℕ,
        Function.Injective t →
        (∀ I, (t I : ℝ) ≤ Real.exp (101 * S)) →
        ∃ E : ℕ → Finset ℕ, ∀ j < depth DM η S,
          Real.exp S < cutoff DM η S j →
          ((E j).card : ℝ) ≤ cutoff DM η S j *
              Real.exp (-c * ResidueLevels.scale S) ∧
          ∀ u ∈ Finset.Icc 1 ⌊cutoff DM η S j⌋₊, u ∉ E j →
…

Mentions: OAI.Problem337.ResidueLevels.scale

theorem OAI.Problem337.reindexed_boolean_residue_count line 131

Source documentation

Reindex the sampled count without losing repeated data.

theorem reindexed_boolean_residue_count {m : ℕ}
    (t : (Fin m → Bool) → ℕ) (ρ : ℝ) (u : ℕ)
    (h : ρ / 2 * (2 : ℝ) ^ m ≤
      ((Finset.univ.filter (fun a : Fin m → Bool =>
        Int.fract (-(t a : ℝ) / u) < ρ)).card : ℝ)) :
    ρ * ((residueIndices (Fin m → Bool)).card : ℝ) / 2 ≤
      (((residueIndices (Fin m → Bool)).filter (fun i =>
        Int.fract (-((residueEntry t i : ℕ) : ℝ) / u) < ρ)).card : ℝ) := by
…

Mentions: OAI.Problem337.residueIndices, OAI.Problem337.residueEntry

theorem OAI.Problem337.eventually_raw_density_supply line 149
Source documentation
Unconditional arithmetic construction of the raw density supply. The prime-product and sampled lists share one bounded denominator, and the actual high and middle residue estimates are joined before the density descent.
```
theorem eventually_raw_density_supply :
    ∀ᶠ S : ℝ in atTop, ∀ C : ℕ,
      Real.exp (4 * (DM + 2) * S) ≤ (C : ℝ) →
      (C : ℝ) ≤ Real.exp (2 * (4 * (DM + 2)) * S) →
      RawDensitySupply DM L c K r S C := by
…
```
Mentions: OAI.Problem337.RawDensitySupply

theorem OAI.Problem337.exists_raw_density_supply line 260

Source documentation

The complete quantitative raw-supply family, with no arithmetic or analytic hypotheses left over.

theorem exists_raw_density_supply :
    ∃ DM L c K r : ℝ, 1 < DM ∧ 0 < L ∧ 0 < c ∧ 0 ≤ K ∧
      2 ≤ r ∧ 8 * K ≤ r ∧
      ∀ᶠ S : ℝ in atTop, ∀ C : ℕ,
        Real.exp (4 * (DM + 2) * S) ≤ (C : ℝ) →
        (C : ℝ) ≤ Real.exp (2 * (4 * (DM + 2)) * S) →
        RawDensitySupply DM L c K r S C := by
…

Mentions: OAI.Problem337.RawDensitySupply