OAI/NumberTheory/TwoPoint/Walks/ProhibitedCatalogEncoding.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.decodeStep_injective line 12
2. lemma OAI.TwoPointCorrelations.decodeStepWord_injective line 20
3. lemma OAI.TwoPointCorrelations.prohibitedCatalog_decode_injective line 34
4. theorem OAI.TwoPointCorrelations.prohibitedCatalog_has_encoding line 41

   Source documentation

   The supplied finite pair family discharges every side condition used by the nondegenerate last-prime relation, including the global padding exclusion.

   theorem prohibitedCatalog_has_encoding (pairs : Finset (ℕ × ℕ)) (P Q : Finset ℕ)
       (h s J M : ℕ)
       (ht : ∀ dq ∈ pairs, Squarefree dq.1) (hq : ∀ dq ∈ pairs, Squarefree dq.2)
       (hJ : ∀ dq ∈ pairs, dq.1.primeFactors.card = J)
       (hM : ∀ dq ∈ pairs, dq.2.primeFactors.card ≤ M)
       (hP : ∀ dq ∈ pairs, dq.1.primeFactors ⊆ P)
       (hQ : ∀ dq ∈ pairs, dq.2.primeFactors ⊆ Q)
       (hd : Disjoint P Q) (hh : ∀ p ∈ P, ¬p ∣ h)
       (c : ProhibitedCatalog pairs h s) :
       ∃ e : PrimeWordEncoding c.val.1.val (s * (J + M)) P Q,
         e.Prohibited h s J (fun d q => (d, q) ∈ pairs) ∧
         e.decode = decodeStepWord c.val ∧
   …

   Mentions: OAI.TwoPointCorrelations.ProhibitedCatalog, OAI.TwoPointCorrelations.PrimeWordEncoding, OAI.TwoPointCorrelations.decodeStepWord

5. theorem OAI.TwoPointCorrelations.prohibitedCatalog_reciprocal_sum_le_encodings line 81

   Source documentation

   The actual catalog sum is bounded by the finite code sum, with each numerical prime still carrying exactly one reciprocal.

   theorem prohibitedCatalog_reciprocal_sum_le_encodings
       (pairs : Finset (ℕ × ℕ)) (P Q : Finset ℕ) (h s J M : ℕ)
       (ht : ∀ dq ∈ pairs, Squarefree dq.1) (hq : ∀ dq ∈ pairs, Squarefree dq.2)
       (hJ : ∀ dq ∈ pairs, dq.1.primeFactors.card = J)
       (hM : ∀ dq ∈ pairs, dq.2.primeFactors.card ≤ M)
       (hP : ∀ dq ∈ pairs, dq.1.primeFactors ⊆ P)
       (hQ : ∀ dq ∈ pairs, dq.2.primeFactors ⊆ Q)
       (hd : Disjoint P Q) (hh : ∀ p ∈ P, ¬p ∣ h) :
       (∑ c : ProhibitedCatalog pairs h s,
         ∏ p ∈ wordDivisorPrimeSupport (decodeStepWord c.val), (p : ℝ)⁻¹) ≤
         ∑ R : Fin (s + 1), ∑ e : PrimeWordEncoding R.val (s * (J + M)) P Q,
           if e.Prohibited h s J (fun d q => (d, q) ∈ pairs) then e.weight else 0 := by
   …

   Mentions: OAI.TwoPointCorrelations.ProhibitedCatalog, OAI.TwoPointCorrelations.wordDivisorPrimeSupport, OAI.TwoPointCorrelations.decodeStepWord, OAI.TwoPointCorrelations.PrimeWordEncoding

6. theorem OAI.TwoPointCorrelations.prohibitedCatalog_reciprocal_bound line 121

   Source documentation

   Full reciprocal estimate for the manuscript's minimal prohibited words.

   theorem prohibitedCatalog_reciprocal_bound
       (pairs : Finset (ℕ × ℕ)) (P Q : Finset ℕ) (h s J M : ℕ)
       (ht : ∀ dq ∈ pairs, Squarefree dq.1) (hq : ∀ dq ∈ pairs, Squarefree dq.2)
       (hJ : ∀ dq ∈ pairs, dq.1.primeFactors.card = J)
       (hM : ∀ dq ∈ pairs, dq.2.primeFactors.card ≤ M)
       (hP : ∀ dq ∈ pairs, dq.1.primeFactors ⊆ P)
       (hQ : ∀ dq ∈ pairs, dq.2.primeFactors ⊆ Q)
       (hd : Disjoint P Q) (hh : ∀ p ∈ P, ¬p ∣ h)
       (hprime : ∀ p ∈ P, p.Prime) (hVP : 1 ≤ primeHarmonicMass P)
       (H B : ℕ) (hH : 0 < H) (hB : 1 ≤ B)
       (hlo : ∀ p ∈ P, H ≤ p) (hhi : ∀ p ∈ P, p ≤ B) :
       (∑ c : ProhibitedCatalog pairs h s,
   …

   Mentions: OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.ProhibitedCatalog