ColumnBlockGeometry.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The perfect-block geometry for the actual labels of a fixed prime column.

theorem OAI.TwoPointCorrelations.ColumnWordPattern.label_intervals_of_prime_intervals line 15

Source documentation

Disjoint column supplies turn numerical prime intervals into intervals of the abstract labels used by the decoder.

theorem label_intervals_of_prime_intervals (w : ColumnWordPattern α) (value : α → ℕ)
    (hvalue : Function.Injective value) (hprime : ∀ z, (value z).Prime)
    (hother : ∀ z t, t < w.length → ¬value z ∣ w.otherColumns t)
    (hinterval : TuplePrimeIntervals (w.word value)) :
    ∀ i j k : Fin w.length, i ≤ j → j ≤ k → w.label i = w.label k → w.label j = w.label i := by
…

Mentions: OAI.TwoPointCorrelations.ColumnWordPattern, OAI.TwoPointCorrelations.TuplePrimeIntervals

theorem OAI.TwoPointCorrelations.ColumnWordPattern.positive_block_geometry line 38

Source documentation

All block geometry needed for coding follows from the genuine surviving positive-word lemma, with only the disjoint prime-supply data added.

theorem positive_block_geometry (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 : ℤ}
    (hw : PositiveWord h x (w.word value)) (hh : 0 < h)
    (hlen : w.length ≤ s)
    (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 : (w.word value).IsChain (fun a b => a.tuple ≠ b.tuple))
    (hsupport : ∀ p j, TuplePrimeAt (w.word value) p j →
…

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