ColumnRankRelations.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Integral coefficient rows of the lit-consistency equations.

def OAI.TwoPointCorrelations.integerColumnDeparture line 18
Source documentation
Each step has one label in the selected column; its coefficient contains only its sign, padding, fixed shift and the primes in other columns.
```
noncomputable def integerColumnDeparture (label : ℕ → α) (t : ℕ → ℤ) (n : ℕ) (z : α) : ℤ :=
…
```
lemma OAI.TwoPointCorrelations.integerColumnDeparture_cast line 21
lemma OAI.TwoPointCorrelations.integerColumnDeparture_eval line 27
def OAI.TwoPointCorrelations.columnDifference line 37
lemma OAI.TwoPointCorrelations.columnDifference_cast line 42
lemma OAI.TwoPointCorrelations.columnDifference_eval line 51

theorem OAI.TwoPointCorrelations.column_congruence_of_departure_divisibilities line 61

Source documentation

Only the selected lit departures are needed; unlit steps need not be positive in the mixed-difference expansion.

theorem column_congruence_of_departure_divisibilities (h : ℕ) (word : List SignedStep)
    (base : ℤ) (label : ℕ → α) (t : ℕ → ℤ) (value : α → ℕ)
    (hstep : ∀ a < word.length, wordStepDisplacement h word a = t a * (value (label a) : ℤ))
    (left right : ρ → ℕ) (control : ρ → α)
    (hleft : ∀ i, left i ≤ word.length) (hright : ∀ i, right i ≤ word.length)
    (hlit : ∀ i, (value (control i) : ℤ) ∣ base + wordDisplacement h (word.take (left i)))
    (hrit : ∀ i, (value (control i) : ℤ) ∣ base + wordDisplacement h (word.take (right i)))
    (i : ρ) :
    (value (control i) : ℤ) ∣ ∑ z, columnDifference label t left right i z * (value z : ℤ) := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordStepDisplacement, OAI.TwoPointCorrelations.wordDisplacement, OAI.TwoPointCorrelations.columnDifference

theorem OAI.TwoPointCorrelations.positiveWord_column_congruence line 81

Source documentation

Positivity of the whole word is a convenient sufficient condition for selected lit consistency.

theorem positiveWord_column_congruence (h : ℕ) (word : List SignedStep) (base : ℤ)
    (hw : PositiveWord h base word) (label : ℕ → α) (t : ℕ → ℤ) (value : α → ℕ)
    (hstep : ∀ a < word.length, wordStepDisplacement h word a = t a * (value (label a) : ℤ))
    (left right : ρ → ℕ) (control : ρ → α)
    (hleft : ∀ i, TuplePrimeAt word (value (control i)) (left i))
    (hright : ∀ i, TuplePrimeAt word (value (control i)) (right i)) (i : ρ) :
    (value (control i) : ℤ) ∣ ∑ z, columnDifference label t left right i z * (value z : ℤ) := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.wordStepDisplacement, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.columnDifference

theorem OAI.TwoPointCorrelations.columnDifference_disjoint_minor line 94

Source documentation

Joint independence in the manuscript's formal departures gives the actual nonzero integral minor with disjoint controlling coordinates.

theorem columnDifference_disjoint_minor (label : ℕ → α) (t : ℕ → ℤ)
    (left right : ρ → ℕ) (control : ρ → α)
    (hind : LinearIndependent ℝ (Sum.elim
      (fun i => formalDeparture label (fun a => (t a : ℝ)) (left i) -
        formalDeparture label (fun a => (t a : ℝ)) (right i))
      (fun i => Pi.basisFun ℝ α (control i)))) :
    Function.Injective control ∧ ∃ pivot : ρ → α, Function.Injective pivot ∧
      (∀ i j, pivot i ≠ control j) ∧
      (Matrix.of fun i j => columnDifference label t left right i (pivot j)).det ≠ 0 := by
…

Mentions: OAI.TwoPointCorrelations.formalDeparture, OAI.TwoPointCorrelations.columnDifference