ActiveLabels.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Active numerical labels in minimal prohibited witnesses.

def OAI.TwoPointCorrelations.wordPrimeContribution line 11
def OAI.TwoPointCorrelations.ActivePrime line 16
Source documentation
A contiguous relation with a nonzero contribution from this label.
```
def ActivePrime (h : ℕ) (w : List SignedStep) (p : ℕ) : Prop :=
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep
lemma OAI.TwoPointCorrelations.wordPrimeContribution_eq_interval line 21
lemma OAI.TwoPointCorrelations.wordPrimeContribution_eq_singleton line 30

lemma OAI.TwoPointCorrelations.ForwardProhibited.last_new_active line 45

Source documentation

A label first entering at the last step is active in the original prohibited suffix, because its contribution is exactly that last step.

lemma ForwardProhibited.last_new_active {h s : ℕ} {supply : ℕ → ℕ → Prop}
    {w : List SignedStep} (hw : ForwardProhibited h s supply w) {z : ℕ}
    (hz : TuplePrimeAt w z (w.length - 1))
    (hearlier : ∀ i, i < w.length - 1 → ¬TuplePrimeAt w z i)
    (hoff : ∀ p i, (∃ j, TuplePrimeAt w p j) → i < w.length →
      ¬TuplePrimeAt w p i → ¬(p : ℤ) ∣ wordStepDisplacement h w i) :
    ActivePrime h w z := by
…

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

lemma OAI.TwoPointCorrelations.prime_dvd_wordPrimeContribution line 66
lemma OAI.TwoPointCorrelations.ActivePrime.distinct_controller line 76
lemma OAI.TwoPointCorrelations.TuplePrimeIntervals.prefix_occurrences line 89
Source documentation
Intersecting an interval-shaped occurrence set with a prefix gives an explicit nonempty interval of indices.
```
lemma TuplePrimeIntervals.prefix_occurrences {w : List SignedStep}
    (hw : TuplePrimeIntervals w) (p n : ℕ) (hn : n ≤ w.length)
    (hp : ∃ j, j < n ∧ TuplePrimeAt w p j) :
    ∃ a b, a < b ∧ b ≤ n ∧ ∀ i, i < n →
      (TuplePrimeAt w p i ↔ a ≤ i ∧ i < b) := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.TuplePrimeIntervals, OAI.TwoPointCorrelations.TuplePrimeAt
lemma OAI.TwoPointCorrelations.wordPrimeContribution_restrict line 120
lemma OAI.TwoPointCorrelations.MinimalWord.no_reversed_divisible_interval line 143
Source documentation
Minimality forbids a reversed suffix starting at a strictly positive index, when an internal initial segment is divisible by its final prime.
```
lemma MinimalWord.no_reversed_divisible_interval {h s : ℕ} {supply : ℕ → ℕ → Prop}
    {w : List SignedStep} (hw : MinimalWord (ForwardProhibited h s supply) w)
    {a c p : ℕ} (ha : 0 < a) (hac : a + 1 < c) (hc : c < w.length)
    (hp : TuplePrimeAt w p (w.length - 1)) (hnot : ¬TuplePrimeAt w p a) :
    ¬(p : ℤ) ∣ intervalDisplacement (wordStepDisplacement h w) a c := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.MinimalWord, OAI.TwoPointCorrelations.ForwardProhibited, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.intervalDisplacement, OAI.TwoPointCorrelations.wordStepDisplacement

theorem OAI.TwoPointCorrelations.MinimalWord.active_dichotomy line 158

Source documentation

Every label of a minimal prohibited word is active or has a nonzero prefix contribution modulo an active label used at that departure.

theorem MinimalWord.active_dichotomy {h s : ℕ} {supply : ℕ → ℕ → Prop}
    {w : List SignedStep} (hw : MinimalWord (ForwardProhibited h s supply) w)
    (hnew : ∀ i, i + 1 < w.length →
      ∃ p, TuplePrimeAt w p (i + 1) ∧ ¬TuplePrimeAt w p i)
    (hoff : ∀ p i, (∃ j, TuplePrimeAt w p j) → i < w.length →
      ¬TuplePrimeAt w p i → ¬(p : ℤ) ∣ wordStepDisplacement h w i)
    (y : ℕ) (hy : ∃ j, TuplePrimeAt w y j) :
    ActivePrime h w y ∨ ∃ z i, ActivePrime h w z ∧ TuplePrimeAt w z i ∧
      ¬(z : ℤ) ∣ wordPrimeContribution h w y 0 i := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.MinimalWord, OAI.TwoPointCorrelations.ForwardProhibited, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.wordStepDisplacement, OAI.TwoPointCorrelations.ActivePrime, OAI.TwoPointCorrelations.wordPrimeContribution

lemma OAI.TwoPointCorrelations.adjacent_tuple_new_prime line 240

Source documentation

Equal-size squarefree tuples that change must also acquire a new prime.

lemma adjacent_tuple_new_prime (w : List SignedStep) (J : ℕ)
    (hsq : ∀ a ∈ w, Squarefree a.tuple)
    (hcard : ∀ a ∈ w, a.tuple.primeFactors.card = J)
    (hchain : w.IsChain (fun a b => a.tuple ≠ b.tuple)) :
    ∀ i, i + 1 < w.length → ∃ p, TuplePrimeAt w p (i + 1) ∧ ¬TuplePrimeAt w p i := by
…

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

theorem OAI.TwoPointCorrelations.MinimalWord.active_dichotomy_of_squarefree line 271

Source documentation

The active-label dichotomy with the manuscript's concrete arithmetic hypotheses: squarefree whole tuples of fixed prime-factor count, and prime exclusion from the common multiplier and all padding factors.

theorem MinimalWord.active_dichotomy_of_squarefree {h s J : ℕ}
    {supply : ℕ → ℕ → Prop} {w : List SignedStep}
    (hw : MinimalWord (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)
    (y : ℕ) (hy : ∃ j, TuplePrimeAt w y j) :
    ActivePrime h w y ∨ ∃ z i, ActivePrime h w z ∧ TuplePrimeAt w z i ∧
      ¬(z : ℤ) ∣ wordPrimeContribution h w y 0 i := by
…

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