WordBlockGeometry.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Geometry of actual surviving positive words, including the prime-support checks.

lemma OAI.TwoPointCorrelations.tuplePrimeAt_iff_getElem line 12
lemma OAI.TwoPointCorrelations.wordStepDisplacement_getElem line 16
lemma OAI.TwoPointCorrelations.tuplePrime_dvd_step line 20
lemma OAI.TwoPointCorrelations.PositiveWord.tuplePrime_departure line 29
Source documentation
Positivity supplies each tuple-prime divisibility at the exact prefix sum.
```
lemma PositiveWord.tuplePrime_departure {h p i : ℕ} {x : ℤ} {w : List SignedStep}
    (hw : PositiveWord h x w) (hp : TuplePrimeAt w p i) :
    (p : ℤ) ∣ x + wordDisplacement h (w.take i) := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.wordDisplacement
lemma OAI.TwoPointCorrelations.PositiveWord.tuplePrime_departure_sum line 46

lemma OAI.TwoPointCorrelations.adjacent_tuple_prime_change line 55

Source documentation

Equal-size squarefree whole tuples cannot change by merely adding primes: a changed tuple loses at least one prime from the preceding tuple.

lemma adjacent_tuple_prime_change (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 ∧ ¬TuplePrimeAt w p (i + 1) := by
…

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

lemma OAI.TwoPointCorrelations.word_prime_support line 85
Source documentation
Every tuple prime is coprime to the common multiplier and every padding. Consequently an absent tuple prime cannot divide a step's displacement.
```
lemma word_prime_support {h : ℕ} {w : List SignedStep}
    (hsupport : ∀ p j, TuplePrimeAt w p j → ¬p ∣ h ∧ ∀ a ∈ w, ¬p ∣ a.padding) :
    ∀ p i, (∃ j, j < w.length ∧ TuplePrimeAt w p j) → i < w.length →
      ¬TuplePrimeAt w p i → ¬(p : ℤ) ∣ wordStepDisplacement h w i := by
…
```
Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.wordStepDisplacement
lemma OAI.TwoPointCorrelations.word_step_nonzero line 100

theorem OAI.TwoPointCorrelations.PositiveWord.block_geometry line 115

Source documentation

The block-interval lemma for actual signed words. All hypotheses concern admissibility, positivity, survival, or the explicit prime supports. Neither interval-shaped occurrences nor nonzero subintervals is assumed.

theorem PositiveWord.block_geometry {h s J : ℕ} {supply : ℕ → ℕ → Prop}
    {x : ℤ} {w : List SignedStep} (hw : PositiveWord h x w) (hh : 0 < h)
    (hlen : w.length ≤ s) (heligible : ∀ a ∈ w, supply a.tuple a.padding)
    (hq : ∀ a ∈ w, 0 < a.padding) (hsq : ∀ a ∈ w, Squarefree a.tuple)
    (hcard : ∀ a ∈ w, a.tuple.primeFactors.card = J)
    (hchain : w.IsChain (fun a b => a.tuple ≠ b.tuple))
    (hsupport : ∀ p j, TuplePrimeAt w p j → ¬p ∣ h ∧ ∀ a ∈ w, ¬p ∣ a.padding)
    (hsurvive : ∀ y, WordVertex h x w y → ¬ProhibitedSite h s supply y) :
    TuplePrimeIntervals w ∧
      ∀ a b, a < b → b ≤ w.length → wordDisplacement h (wordSlice w a b) ≠ 0 := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.WordVertex, OAI.TwoPointCorrelations.ProhibitedSite, OAI.TwoPointCorrelations.TuplePrimeIntervals, OAI.TwoPointCorrelations.wordDisplacement, OAI.TwoPointCorrelations.wordSlice