ColumnWordSlices.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual contiguous column blocks retain their signed word and coefficient geometry.

def OAI.TwoPointCorrelations.ColumnWordPattern.slice line 13
theorem OAI.TwoPointCorrelations.ColumnWordPattern.slice_word line 20
theorem OAI.TwoPointCorrelations.ColumnWordPattern.slice_coefficient line 30

theorem OAI.TwoPointCorrelations.ColumnWordPattern.block_geometry_of_slice line 36

Source documentation

Use positivity only on the actual perfect block; other positions in the full trace word may be unlit. All global admissibility properties are restricted to that block, and every scalar sum uses its original indices.

theorem block_geometry_of_slice (w : ColumnWordPattern α) (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 : ℤ} (start len : ℕ)
    (hend : start + len ≤ w.length) (hshort : len ≤ s)
    (hw : PositiveWord h x (wordSlice (w.word value) start (start + len))) (hh : 0 < h)
    (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 : (wordSlice (w.word value) start (start + len)).IsChain
      (fun a b => a.tuple ≠ b.tuple))
…

Mentions: OAI.TwoPointCorrelations.ColumnWordPattern, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.wordSlice