OAI/NumberTheory/TwoPoint/Walks/WordSegments.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.wordStepDisplacement line 11
2. lemma OAI.TwoPointCorrelations.wordStepDisplacement_nil line 14
3. lemma OAI.TwoPointCorrelations.wordStepDisplacement_cons_zero line 17
4. lemma OAI.TwoPointCorrelations.wordStepDisplacement_cons_succ line 20
5. lemma OAI.TwoPointCorrelations.wordDisplacement_take line 23
6. def OAI.TwoPointCorrelations.wordSlice line 35
7. lemma OAI.TwoPointCorrelations.wordSlice_length line 37
8. lemma OAI.TwoPointCorrelations.wordSlice_split line 42
9. lemma OAI.TwoPointCorrelations.wordSlice_infix line 47
10. lemma OAI.TwoPointCorrelations.wordSlice_displacement line 52
11. lemma OAI.TwoPointCorrelations.wordSlice_drop line 59
12. lemma OAI.TwoPointCorrelations.tuplePrimeAt_slice line 65
13. lemma OAI.TwoPointCorrelations.TuplePrimeAt.index_lt line 70
14. lemma OAI.TwoPointCorrelations.prohibitedInterval_forward_wordSlice line 77

    Source documentation

    The purely local interval prohibition is exactly a forward-prohibited list segment when eligibility and unequal consecutive tuples are retained.

    lemma prohibitedInterval_forward_wordSlice (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)) {a b : ℕ}
        (hb : b ≤ w.length)
        (hpro : ProhibitedInterval (TuplePrimeAt w) (wordStepDisplacement h w) id a b) :
        ForwardProhibited h s supply (wordSlice w a b) := by
    …

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.ProhibitedInterval, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.wordStepDisplacement, OAI.TwoPointCorrelations.ForwardProhibited, OAI.TwoPointCorrelations.wordSlice

15. theorem OAI.TwoPointCorrelations.PositiveWord.avoids_prohibitedIntervals line 109

    Source documentation

    The local prohibition hypothesis used by block geometry is discharged from survival of the actual main vertices, via concrete witness descent.

    theorem PositiveWord.avoids_prohibitedIntervals {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)
        (hlen : w.length ≤ s) (hsupply : ∀ t ∈ w, supply t.tuple t.padding)
        (hchain : w.IsChain (fun a b => a.tuple ≠ b.tuple)) :
        ∀ a b, b ≤ w.length → ¬ProhibitedInterval (TuplePrimeAt w) (wordStepDisplacement h w) id a b := by
    …

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.WordVertex, OAI.TwoPointCorrelations.ProhibitedSite, OAI.TwoPointCorrelations.ProhibitedInterval, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.wordStepDisplacement