BadCatalogCost.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The cost of the complete short-word catalog

Numerical primes are summed by reciprocal weight, rather than counted as additional symbols. This leaves only signs, equality classes, row records, and tuple/padding flags. The bound includes every length and every slot count up to the stated budgets, including invalid codes.

def OAI.TwoPointCorrelations.CrudeWordCode.badReciprocalCost line 25
Source documentation
The finite cost left after one nondegenerate prime relation is imposed.
```
noncomputable def badReciprocalCost (c : CrudeWordCode R N R) (VP VQ : ℝ) : ℝ :=
…
```
Mentions: OAI.TwoPointCorrelations.CrudeWordCode
lemma OAI.TwoPointCorrelations.CrudeWordCode.badReciprocalCost_nonneg line 30
lemma OAI.TwoPointCorrelations.CrudeWordCode.tuple_padding_class_count line 35
lemma OAI.TwoPointCorrelations.CrudeWordCode.class_count_le_slots line 42

lemma OAI.TwoPointCorrelations.CrudeWordCode.class_mass_le line 50

Source documentation

Tuple and padding classes together use at most one reciprocal mass per slot.

lemma class_mass_le (c : CrudeWordCode R N R) {VP VQ A : ℝ}
    (hP : 0 ≤ VP) (hQ : 0 ≤ VQ) (hPA : VP ≤ A) (hQA : VQ ≤ A)
    (hA : 1 ≤ A) :
    VP ^ Fintype.card c.tupleClasses *
      VQ ^ Fintype.card {z : c.usedClasses // z ∉ c.tupleClasses} ≤ A ^ N := by
…

Mentions: OAI.TwoPointCorrelations.CrudeWordCode

def OAI.TwoPointCorrelations.badCatalogCost line 67
Source documentation
All lengths, all actual slot counts, and all finite equality codes.
```
noncomputable def badCatalogCost (s T : ℕ) (VP VQ : ℝ) : ℝ :=
…
```
lemma OAI.TwoPointCorrelations.short_log_le_square line 71
lemma OAI.TwoPointCorrelations.short_polynomial_exp_bound line 77

lemma OAI.TwoPointCorrelations.short_crudeWordCode_bound line 91

Source documentation

Unlike the coarser pattern estimate, this bound does not need R ≤ N; empty or invalid codes may therefore be retained in the catalog.

lemma short_crudeWordCode_bound (R N s : ℕ) (L C : ℝ)
    (hlog : 1 ≤ Real.log L) (hR : R ≤ s)
    (hslots : (N : ℝ) ≤ C * s * Real.log L)
    (hN : (N : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hspoly : (s : ℝ) + 1 ≤ L ^ (2 : ℕ)) :
    (Fintype.card (CrudeWordCode R N R) : ℝ) ≤
      Real.exp ((1 + 5 * C) * s * (Real.log L) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.CrudeWordCode

lemma OAI.TwoPointCorrelations.short_badReciprocalCost_bound line 126

Source documentation

The reciprocal masses and the choice of one relation cost only an additional exp ((8 + 2 C) s log² L) for a fixed code.

lemma short_badReciprocalCost_bound {R N s : ℕ} (c : CrudeWordCode R N R)
    (VP VQ L C : ℝ) (hs : 1 ≤ s) (hL : 1 ≤ L) (hlog : 1 ≤ Real.log L)
    (hR : R ≤ s) (hslots : (N : ℝ) ≤ C * s * Real.log L)
    (hN : (N : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hspoly : (s : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hP : 0 ≤ VP) (hQ : 0 ≤ VQ)
    (hPupper : VP ≤ L ^ (2 : ℕ)) (hQupper : VQ ≤ L ^ (2 : ℕ)) :
    c.badReciprocalCost VP VQ ≤
      Real.exp ((8 + 2 * C) * s * (Real.log L) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.CrudeWordCode

lemma OAI.TwoPointCorrelations.short_badCode_sum_bound line 184

Source documentation

Sum over every code of one fixed length and slot count.

lemma short_badCode_sum_bound (R N s : ℕ) (VP VQ L C : ℝ)
    (hs : 1 ≤ s) (hL : 1 ≤ L) (hlog : 1 ≤ Real.log L)
    (hR : R ≤ s) (hslots : (N : ℝ) ≤ C * s * Real.log L)
    (hN : (N : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hspoly : (s : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hP : 0 ≤ VP) (hQ : 0 ≤ VQ)
    (hPupper : VP ≤ L ^ (2 : ℕ)) (hQupper : VQ ≤ L ^ (2 : ℕ)) :
    (∑ c : CrudeWordCode R N R, c.badReciprocalCost VP VQ) ≤
      Real.exp ((9 + 7 * C) * s * (Real.log L) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.CrudeWordCode

theorem OAI.TwoPointCorrelations.badCatalogCost_exp_bound line 210

Source documentation

The complete catalog, including both bounded integer parameters, has the required exp (O(s log² L)) reciprocal cost.

theorem badCatalogCost_exp_bound (s T : ℕ) (VP VQ L C : ℝ)
    (hs : 1 ≤ s) (hL : 1 ≤ L) (hlog : 1 ≤ Real.log L)
    (hslots : (T : ℝ) ≤ C * s * Real.log L)
    (hT : (T : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hspoly : (s : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hP : 0 ≤ VP) (hQ : 0 ≤ VQ)
    (hPupper : VP ≤ L ^ (2 : ℕ)) (hQupper : VQ ≤ L ^ (2 : ℕ)) :
    badCatalogCost s T VP VQ ≤
      Real.exp ((13 + 7 * C) * s * (Real.log L) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.badCatalogCost

theorem OAI.TwoPointCorrelations.eventually_badCatalogCost_exp_bound line 254

Source documentation

The polynomial side conditions in the finite estimate follow from the actual short-word and slot budgets once the scale is sufficiently large.

theorem eventually_badCatalogCost_exp_bound (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (s T : ℕ) (VP VQ : ℝ),
      1 ≤ s → (s : ℝ) ≤ L ^ (1 / 10 : ℝ) →
      (T : ℝ) ≤ C * s * Real.log L →
      0 ≤ VP → 0 ≤ VQ → VP ≤ L ^ (2 : ℕ) → VQ ≤ L ^ (2 : ℕ) →
      badCatalogCost s T VP VQ ≤
        Real.exp ((13 + 7 * C) * s * (Real.log L) ^ 2) := by
…

Mentions: OAI.TwoPointCorrelations.badCatalogCost

theorem OAI.TwoPointCorrelations.eventually_badCatalog_decay line 292

Source documentation

The full short-word enumeration is dominated by the single prime saving. This is the numerical end of the prohibited-site density estimate.

theorem eventually_badCatalog_decay (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (s T : ℕ) (VP VQ H B total : ℝ),
      1 ≤ s → (s : ℝ) ≤ L ^ (1 / 10 : ℝ) →
      (T : ℝ) ≤ C * s * Real.log L →
      0 ≤ VP → 0 ≤ VQ → VP ≤ L ^ (2 : ℕ) → VQ ≤ L ^ (2 : ℕ) →
      Real.exp (L ^ (199 / 200 : ℝ)) ≤ H → 1 ≤ B → B ≤ Real.exp L →
      total ≤ badCatalogCost s T VP VQ * (H⁻¹ + (1 + Real.log B) / H) →
      total ≤ Real.exp (-(1 / 2 : ℝ) * L ^ (199 / 200 : ℝ)) := by
…

Mentions: OAI.TwoPointCorrelations.badCatalogCost