ProhibitedWords.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

Positive words, reversal, and descent to a minimal prohibited word

A step keeps its whole tuple and padding divisor. Positivity is the exact integer divisibility q*d ∣ x at its departure. Since the displacement is ±h*q*d, this divisibility also holds at its arrival. Restriction and reversal therefore preserve positivity, as required in the witness descent.

structure OAI.TwoPointCorrelations.SignedStep line 18
def OAI.TwoPointCorrelations.SignedStep.flip line 26
lemma OAI.TwoPointCorrelations.SignedStep.flip_flip line 28
def OAI.TwoPointCorrelations.SignedStep.displacement line 32
def OAI.TwoPointCorrelations.SignedStep.divisor line 35
lemma OAI.TwoPointCorrelations.SignedStep.displacement_flip line 37
lemma OAI.TwoPointCorrelations.SignedStep.divisor_dvd_displacement line 42
lemma OAI.TwoPointCorrelations.SignedStep.divisor_flip line 47
lemma OAI.TwoPointCorrelations.SignedStep.divisor_dvd_arrival line 49
lemma OAI.TwoPointCorrelations.SignedStep.prime_not_dvd_displacement line 54
Source documentation
The exclusions on the common multiplier, padding, and tuple imply the exact absence of this prime from the integer displacement.
```
lemma prime_not_dvd_displacement (h p : ℕ) (hp : p.Prime) (a : SignedStep)
    (hh : ¬p ∣ h) (hq : ¬p ∣ a.padding) (hd : ¬p ∣ a.tuple) :
    ¬(p : ℤ) ∣ a.displacement h := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep
def OAI.TwoPointCorrelations.wordDisplacement line 65
Source documentation
Total displacement, with each visit counted in order.
```
def wordDisplacement (h : ℕ) (w : List SignedStep) : ℤ :=
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep
lemma OAI.TwoPointCorrelations.wordDisplacement_nil line 68
lemma OAI.TwoPointCorrelations.wordDisplacement_cons line 70
lemma OAI.TwoPointCorrelations.wordDisplacement_append line 73
def OAI.TwoPointCorrelations.reverseWord line 78
Source documentation
Reversing a word reverses its order and its signs.
```
def reverseWord (w : List SignedStep) : List SignedStep := w.reverse.map SignedStep.flip
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.SignedStep.flip
lemma OAI.TwoPointCorrelations.reverseWord_nil line 80
lemma OAI.TwoPointCorrelations.reverseWord_cons line 82
lemma OAI.TwoPointCorrelations.reverseWord_append line 85
lemma OAI.TwoPointCorrelations.reverseWord_length line 88
lemma OAI.TwoPointCorrelations.reverseWord_reverseWord line 91
lemma OAI.TwoPointCorrelations.wordDisplacement_reverseWord line 94
def OAI.TwoPointCorrelations.PositiveWord line 101
Source documentation
Exact positivity at every successive departure site.
```
def PositiveWord (h : ℕ) (x : ℤ) : List SignedStep → Prop
  | [] => True
  | a :: w => a.divisor ∣ x ∧ PositiveWord h (x + a.displacement h) w
```
Mentions: OAI.TwoPointCorrelations.SignedStep
lemma OAI.TwoPointCorrelations.positiveWord_nil line 105
lemma OAI.TwoPointCorrelations.positiveWord_cons line 107
lemma OAI.TwoPointCorrelations.positiveWord_append line 110
lemma OAI.TwoPointCorrelations.PositiveWord.reverse line 120
Source documentation
Positivity at arrivals makes reversed paths positive at their old endpoint.
```
lemma PositiveWord.reverse {h : ℕ} {x : ℤ} {w : List SignedStep} (hw : PositiveWord h x w) :
    PositiveWord h (x + wordDisplacement h w) (reverseWord w) := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.wordDisplacement, OAI.TwoPointCorrelations.reverseWord
def OAI.TwoPointCorrelations.WordVertex line 133
Source documentation
A main vertex is the endpoint of a prefix, including both extreme endpoints.
```
def WordVertex (h : ℕ) (x : ℤ) (w : List SignedStep) (y : ℤ) : Prop :=
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep
lemma OAI.TwoPointCorrelations.WordVertex.reverse line 136
lemma OAI.TwoPointCorrelations.PositiveWord.infix line 147
def OAI.TwoPointCorrelations.OrientedInfix line 159
Source documentation
A contiguous subword in either orientation.
```
def OrientedInfix (u w : List SignedStep) : Prop := u <:+: w ∨ u <:+: reverseWord w
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.reverseWord
lemma OAI.TwoPointCorrelations.OrientedInfix.refl line 161
lemma OAI.TwoPointCorrelations.reverseWord_infix line 163
lemma OAI.TwoPointCorrelations.OrientedInfix.trans line 166
lemma OAI.TwoPointCorrelations.OrientedInfix.length_le line 174
lemma OAI.TwoPointCorrelations.PositiveWord.orientedInfix line 180
def OAI.TwoPointCorrelations.MinimalWord line 190
Source documentation
Minimality refers to numerical words and permits reversing every shorter contiguous subword.
```
def MinimalWord (P : List SignedStep → Prop) (w : List SignedStep) : Prop :=
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep
theorem OAI.TwoPointCorrelations.exists_minimal_orientedInfix line 194
Source documentation
Strictly decreasing lengths give a minimal prohibited contiguous word.
```
theorem exists_minimal_orientedInfix (P : List SignedStep → Prop) (w : List SignedStep)
    (hw : P w) : ∃ u, OrientedInfix u w ∧ MinimalWord P u := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.OrientedInfix, OAI.TwoPointCorrelations.MinimalWord
def OAI.TwoPointCorrelations.TuplePrimeAt line 206
Source documentation
A tuple prime occurs when it divides the whole tuple at that position.
```
def TuplePrimeAt (w : List SignedStep) (p i : ℕ) : Prop :=
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep
def OAI.TwoPointCorrelations.TuplePrimeIntervals line 209
def OAI.TwoPointCorrelations.ForwardProhibited line 214
Source documentation
Exact numerical prohibition, with admissible tuple/padding pairs fixed.
```
def ForwardProhibited (h s : ℕ) (supply : ℕ → ℕ → Prop) (w : List SignedStep) : Prop :=
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep
def OAI.TwoPointCorrelations.ProhibitedWitness line 221
def OAI.TwoPointCorrelations.ProhibitedSite line 225
theorem OAI.TwoPointCorrelations.PositiveWord.prohibited_witness line 230
Source documentation
Every positive prohibited path contains a witness beginning at a main vertex. Reversing during descent may select either endpoint of a subword.
```
theorem PositiveWord.prohibited_witness {h s : ℕ} {supply : ℕ → ℕ → Prop}
    {x : ℤ} {w : List SignedStep} (hw : PositiveWord h x w)
    (hpro : ForwardProhibited h s supply w) :
    ∃ y, WordVertex h x w y ∧ ProhibitedSite h s supply y := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.ForwardProhibited, OAI.TwoPointCorrelations.WordVertex, OAI.TwoPointCorrelations.ProhibitedSite
theorem OAI.TwoPointCorrelations.PositiveWord.not_prohibited line 239
Source documentation
Surviving main vertices exclude every positive prohibited word.
```
theorem PositiveWord.not_prohibited {h s : ℕ} {supply : ℕ → ℕ → Prop}
    {x : ℤ} {w : List SignedStep} (hw : PositiveWord h x w)
    (hsurvive : ∀ y, WordVertex h x w y → ¬ProhibitedSite h s supply y) :
    ¬ForwardProhibited h s supply w := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.WordVertex, OAI.TwoPointCorrelations.ProhibitedSite, OAI.TwoPointCorrelations.ForwardProhibited
theorem OAI.TwoPointCorrelations.PositiveWord.not_prohibited_orientedInfix line 249
Source documentation
The same deletion excludes prohibited words contained in the path in either orientation, by composing the two stages of witness descent.
```
theorem PositiveWord.not_prohibited_orientedInfix {h s : ℕ} {supply : ℕ → ℕ → Prop}
    {x : ℤ} {u w : List SignedStep} (hw : PositiveWord h x w)
    (hsurvive : ∀ y, WordVertex h x w y → ¬ProhibitedSite h s supply y)
    (hu : OrientedInfix u w) : ¬ForwardProhibited h s supply u := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.WordVertex, OAI.TwoPointCorrelations.ProhibitedSite, OAI.TwoPointCorrelations.OrientedInfix, OAI.TwoPointCorrelations.ForwardProhibited