BlockGeometry.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The shortest-gap argument for perfect blocks

The finite combinatorial lemma isolates a shortest gap across all prime coordinates. Every label has interval-shaped uses inside the intervening substring. The arithmetic lemmas below use exact integer displacement sums.

def OAI.TwoPointCorrelations.OccurrenceIntervals line 19
Source documentation
Interval-shaped occurrence sets on a half-open range of positions.
```
def OccurrenceIntervals {α : Type*} (P : α → ℕ → Prop) (a b : ℕ) : Prop :=
…
```
def OAI.TwoPointCorrelations.OccurrenceHole line 23
Source documentation
An occurrence gap has present endpoints and an absent interior position.
```
def OccurrenceHole {α : Type*} (P : α → ℕ → Prop) (n : ℕ) (p : α) (i j : ℕ) : Prop :=
…
```
lemma OAI.TwoPointCorrelations.not_occurrenceIntervals_iff line 26
theorem OAI.TwoPointCorrelations.exists_shortest_occurrence_hole line 42
Source documentation
A shortest gap has no appearances of its own label in its interior, and all labels have interval-shaped appearances before its returning endpoint.
```
theorem exists_shortest_occurrence_hole {α : Type*} (P : α → ℕ → Prop) (n : ℕ)
    (h : ¬OccurrenceIntervals P 0 n) :
    ∃ p i j, OccurrenceHole P n p i j ∧
      (∀ k, i < k → k < j → ¬P p k) ∧ OccurrenceIntervals P i j := by
…
```
Mentions: OAI.TwoPointCorrelations.OccurrenceIntervals, OAI.TwoPointCorrelations.OccurrenceHole
def OAI.TwoPointCorrelations.intervalDisplacement line 71
Source documentation
Displacement of the contiguous positions a, ..., b-1.
```
def intervalDisplacement (D : ℕ → ℤ) (a b : ℕ) : ℤ := ∑ i ∈ Ico a b, D i
```
lemma OAI.TwoPointCorrelations.intervalDisplacement_eq_sub line 73
lemma OAI.TwoPointCorrelations.intervalDisplacement_cons line 77
lemma OAI.TwoPointCorrelations.intervalDisplacement_singleton line 83
def OAI.TwoPointCorrelations.ProhibitedInterval line 88
Source documentation
A concrete local prohibition, including the complete occurrence pattern and an interior suffix divisibility relation.
```
def ProhibitedInterval {α : Type*} (P : α → ℕ → Prop) (D : ℕ → ℤ)
    (prime : α → ℕ) (a b : ℕ) : Prop :=
…
```

lemma OAI.TwoPointCorrelations.departure_difference_dvd line 96

Source documentation

Positivity at two departures supplies the divisibility of the intervening sum, with no assertion of independence between the sites.

lemma departure_difference_dvd {α : Type*} (P : α → ℕ → Prop) (D : ℕ → ℤ)
    (prime : α → ℕ) (x : ℤ) (n : ℕ)
    (hpositive : ∀ p i, i < n → P p i → (prime p : ℤ) ∣ x + ∑ a ∈ range i, D a)
    {p : α} {i j : ℕ} (hij : i ≤ j) (hj : j < n) (hi : P p i) (hjP : P p j) :
    (prime p : ℤ) ∣ intervalDisplacement D i j := by
…

Mentions: OAI.TwoPointCorrelations.intervalDisplacement

theorem OAI.TwoPointCorrelations.block_occurrence_intervals line 109

Source documentation

The shortest returning prime would give a prohibited subword. Thus a positive block avoiding those words has interval-shaped prime occurrences.

theorem block_occurrence_intervals {α : Type*} (P : α → ℕ → Prop) (D : ℕ → ℤ)
    (prime : α → ℕ) (x : ℤ) (n : ℕ)
    (hpositive : ∀ p i, i < n → P p i → (prime p : ℤ) ∣ x + ∑ a ∈ range i, D a)
    (hon : ∀ p i, i < n → P p i → (prime p : ℤ) ∣ D i)
    (hoff : ∀ p i, (∃ j, j < n ∧ P p j) → i < n → ¬P p i → ¬(prime p : ℤ) ∣ D i)
    (havoid : ∀ a b, b ≤ n → ¬ProhibitedInterval P D prime a b) :
    OccurrenceIntervals P 0 n := by
…

Mentions: OAI.TwoPointCorrelations.ProhibitedInterval, OAI.TwoPointCorrelations.OccurrenceIntervals

theorem OAI.TwoPointCorrelations.block_nonzero_subintervals line 139

Source documentation

Once occurrences are intervals, a directed change in the first two prime tuples supplies a prime absent from the final tuple. Any zero sum then gives the same prohibited suffix relation.

theorem block_nonzero_subintervals {α : Type*} (P : α → ℕ → Prop) (D : ℕ → ℤ)
    (prime : α → ℕ) (n : ℕ) (hinterval : OccurrenceIntervals P 0 n)
    (hon : ∀ p i, i < n → P p i → (prime p : ℤ) ∣ D i)
    (hoff : ∀ p i, (∃ j, j < n ∧ P p j) → i < n → ¬P p i → ¬(prime p : ℤ) ∣ D i)
    (hstep : ∀ i, i < n → D i ≠ 0)
    (hchange : ∀ i, i + 1 < n → ∃ p, P p i ∧ ¬P p (i + 1))
    (havoid : ∀ a b, b ≤ n → ¬ProhibitedInterval P D prime a b) :
    ∀ a b, a < b → b ≤ n → intervalDisplacement D a b ≠ 0 := by
…

Mentions: OAI.TwoPointCorrelations.OccurrenceIntervals, OAI.TwoPointCorrelations.ProhibitedInterval, OAI.TwoPointCorrelations.intervalDisplacement