OAI/NumberTheory/TwoPoint/Walks/ReversedSegments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.tuplePrimeAt_reverseWord line 9
2. lemma OAI.TwoPointCorrelations.TuplePrimeIntervals.slice line 15
3. lemma OAI.TwoPointCorrelations.TuplePrimeIntervals.reverse line 27
4. lemma OAI.TwoPointCorrelations.reverseWord_drop line 37
5. lemma OAI.TwoPointCorrelations.reverseWord_slice_drop line 41
6. lemma OAI.TwoPointCorrelations.reverseWord_chain line 49
7. lemma OAI.TwoPointCorrelations.reversed_interval_forwardProhibited line 63

   Source documentation

   The reversed interval is genuinely forward-prohibited. The divisible suffix has length c-a, while its preceding part has positive length.

   lemma reversed_interval_forwardProhibited (h s : ℕ) (supply : ℕ → ℕ → Prop)
       (w : List SignedStep) (hlen : w.length ≤ s)
       (hsupply : ∀ t ∈ w, supply t.tuple t.padding)
       (hchain : w.IsChain (fun a b => a.tuple ≠ b.tuple))
       (hinterval : TuplePrimeIntervals w) {a b c p : ℕ}
       (hac : a + 1 < c) (hcb : c < b) (hb : b ≤ w.length)
       (hp : TuplePrimeAt w p (b - 1)) (hnot : ¬TuplePrimeAt w p a)
       (hdiv : (p : ℤ) ∣ intervalDisplacement (wordStepDisplacement h w) a c) :
       ForwardProhibited h s supply (reverseWord (wordSlice w a b)) := by
   …

   Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.TuplePrimeIntervals, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.intervalDisplacement, OAI.TwoPointCorrelations.wordStepDisplacement, OAI.TwoPointCorrelations.ForwardProhibited, OAI.TwoPointCorrelations.reverseWord, OAI.TwoPointCorrelations.wordSlice