LitBlockGeometry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Perfect blocks use only the lit divisibilities at their actual positions.

theorem OAI.TwoPointCorrelations.positiveWord_iff_departures line 12
theorem OAI.TwoPointCorrelations.positiveWord_slice_of_lit line 34
theorem OAI.TwoPointCorrelations.wordVertex_slice line 56

theorem OAI.TwoPointCorrelations.ColumnWordPattern.short_geometry_of_lit line 80

Source documentation

Every numerical perfect block has the geometric properties used by the universal code. Positivity is assumed only at the perfect positions; unlit positions elsewhere in the trace impose no condition here.

theorem short_geometry_of_lit (w : ColumnWordPattern α) (hn : 0 < w.length)
    (value : α → ℕ) (hvalue : Function.Injective value) (hprime : ∀ z, (value z).Prime)
    (hother : ∀ z t, t < w.length → ¬value z ∣ w.otherColumns t)
    {h s J : ℕ} {supply : ℕ → ℕ → Prop} {x : ℤ} (hh : 0 < h)
    (perfect : Finset (Fin w.length))
    (hlit : ∀ i ∈ perfect, (w.step value i.val).divisor ∣
      x + wordDisplacement h ((w.word value).take i.val))
    (heligible : ∀ a ∈ w.word value, supply a.tuple a.padding)
    (hq : ∀ a ∈ w.word value, 0 < a.padding)
    (hsq : ∀ a ∈ w.word value, Squarefree a.tuple)
    (hcard : ∀ a ∈ w.word value, a.tuple.primeFactors.card = J)
    (hchain : ∀ start len, start + len ≤ w.length → len ≤ s →
…

Mentions: OAI.TwoPointCorrelations.ColumnWordPattern, OAI.TwoPointCorrelations.wordDisplacement