BadWordRelations.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

One actual nondegenerate relation for each forward prohibited word.

theorem OAI.TwoPointCorrelations.ForwardProhibited.exists_active line 16

Source documentation

The last transition of a prohibited word acquires a new prime. Its contribution to the prohibited suffix is exactly the last step.

theorem ForwardProhibited.exists_active {h s J : ℕ} {supply : ℕ → ℕ → Prop}
    {w : List SignedStep} (hw : ForwardProhibited h s supply w)
    (hsq : ∀ a ∈ w, Squarefree a.tuple)
    (hcard : ∀ a ∈ w, a.tuple.primeFactors.card = J)
    (hsupport : ∀ p j, TuplePrimeAt w p j → ¬p ∣ h ∧ ∀ a ∈ w, ¬p ∣ a.padding) :
    ∃ z, ActivePrime h w z := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.ForwardProhibited, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.ActivePrime

abbrev OAI.TwoPointCorrelations.BadRelationCode line 38
def OAI.TwoPointCorrelations.BadRelationCode.Holds line 44
def OAI.TwoPointCorrelations.BadRelationCode.toSystem line 47
lemma OAI.TwoPointCorrelations.BadRelationCode.toSystem_size line 57
def OAI.TwoPointCorrelations.ResampledProhibitedEvent line 67
Source documentation
The numerical event retains every arithmetic assumption used to get the last-step coefficient. The reciprocal sum may subsequently enlarge to coincident numerical assignments.
```
def ResampledProhibitedEvent {ι : Type*} [DecidableEq ι]
    (w : LabeledPrimeWord ι) (h s J : ℕ) (supply : ℕ → ℕ → Prop)
    (value : ι → ℕ) : Prop :=
…
```
Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord
theorem OAI.TwoPointCorrelations.resampled_prohibited_relation line 77
theorem OAI.TwoPointCorrelations.bad_relation_reciprocal_bound line 104

theorem OAI.TwoPointCorrelations.resampled_prohibited_reciprocal_bound line 163

Source documentation

The numerical prohibited event enters the fixed metadata union. The ambient prime assignment may be enlarged after this inclusion is proved.

theorem resampled_prohibited_reciprocal_bound {ι : Type*} [Fintype ι] [DecidableEq ι]
    {s J : ℕ} {supply : ℕ → ℕ → Prop}
    (N h : ℕ) (w : LabeledPrimeWord ι) (hN : w.word.length ≤ N)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (hV : 1 ≤ primeHarmonicMass P)
    (H B : ℕ) (hH : 0 < H) (hB : 1 ≤ B)
    (hlo : ∀ p ∈ P, H ≤ p) (hhi : ∀ p ∈ P, p ≤ B) :
    (∑ x : ι → P, if ResampledProhibitedEvent w h s J supply (fun i => (x i).val)
      then ∏ i, ((x i).val : ℝ)⁻¹ else 0) ≤
      (Fintype.card ι ^ 2 * (N + 1) ^ 2 : ℕ) * primeHarmonicMass P ^ Fintype.card ι *
        ((H : ℝ)⁻¹ + (1 + Real.log B) / H) := by
…

Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.ResampledProhibitedEvent