NumericalColumnCover.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A surviving numerical trace word belongs to the universal column code set.

theorem OAI.TwoPointCorrelations.ColumnWordPattern.numerical_column_in_universe line 19

Source documentation

The complete column-covering implication. Only the two halves are assumed nonbacktracking. All positivity premises are actual divisibilities at the original perfect positions; one midpoint reference is charged to the imperfect budget. The finite code universe is independent of value, the signs, the padding, and the fixed other-column coefficients.

theorem numerical_column_in_universe (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 r : ℕ} {supply : ℕ → ℕ → Prop} {x : ℤ} (hh : 0 < h) (hs : 0 < s)
    (perfect : Finset (Fin w.length)) (cut : 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)
    (hleft : ((w.word value).take cut.val).IsChain (fun a b => a.tuple ≠ b.tuple))
…

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