ColumnWordGeometry.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Nonzero actual word intervals force nonzero quotient-run coefficients.

lemma OAI.TwoPointCorrelations.ColumnWordPattern.constant_run_coefficient_ne_zero line 18
Source documentation
The coefficient sum of a constant column run cannot vanish when its actual integer displacement does not vanish.
```
lemma constant_run_coefficient_ne_zero (w : ColumnWordPattern α) (h : ℕ)
    (value : α → ℕ) (a b : ℕ) (hab : a ≤ b) (hb : b ≤ w.length) (z : α)
    (hconst : ∀ t ∈ Ico a b, w.label t = z)
    (hnonzero : wordDisplacement h (wordSlice (w.word value) a b) ≠ 0) :
    (∑ t ∈ Ico a b, w.coefficient h t) ≠ 0 := by
…
```
Mentions: OAI.TwoPointCorrelations.ColumnWordPattern, OAI.TwoPointCorrelations.wordDisplacement, OAI.TwoPointCorrelations.wordSlice
lemma OAI.TwoPointCorrelations.ColumnWordPattern.constant_run_real_coefficient_ne_zero line 35

theorem OAI.TwoPointCorrelations.ColumnWordPattern.regular_segment_quotient_data line 45

Source documentation

The manuscript's nonzero-subinterval conclusion supplies every scalar non-reversal condition needed by the greedy regular-segment path.

theorem regular_segment_quotient_data [Fintype α]
    {ι : Type*} [DecidableEq ι]
    (w : ColumnWordPattern α) (h : ℕ) (value : α → ℕ)
    (D : Submodule ℝ (α → ℝ)) (anchor : ι → (α → ℝ) ⧸ D)
    (regularLabel : ι → α) (runLabel : ℕ → ι) (start len : ℕ)
    (hlen : 0 < len) (hend : start + len ≤ w.length)
    (hlabel : ∀ t ∈ Ico start (start + len), w.label t = regularLabel (runLabel t))
    (hline : ∀ t ∈ Ico start (start + len),
      ∃ c : ℝ, D.mkQ (formalDeparture w.label (fun j => (w.coefficient h j : ℝ)) t) =
        anchor (runLabel t) + c • D.mkQ (Pi.basisFun ℝ α (regularLabel (runLabel t))))
    (hnonzero : ∀ a b, start ≤ a → a < b → b ≤ start + len →
      wordDisplacement h (wordSlice (w.word value) a b) ≠ 0) :
…

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