ShiftSequence.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.blockShift_eq_zero_of_pos_weight line 17

Source documentation

Positive-weight injectivity for the shared blockShift derivation API.

theorem blockShift_eq_zero_of_pos_weight (src dst : B) (hsd : src ≠ dst)
    {f : MvPolynomial (B × I) ℂ} {p q : ℕ} (hpq : q < p)
    (hp : IsBlockHomogeneous src f p) (hq : IsBlockHomogeneous dst f q)
    (hDf : blockShift ℂ src dst f = 0) : f = 0 := by
…

Mentions: OAI.Problem346.blockShift

theorem OAI.Problem346.blockShift_pow_eq_zero_of_degree_bound line 41
Source documentation
A chain of repeated shifts can be cancelled as long as its least intermediate source-minus-destination weight is positive. The convenient sufficient bound q + 2*n ≤ p is exactly what is used for each block in the quadratic argument.
```
theorem blockShift_pow_eq_zero_of_degree_bound (src dst : B) (hsd : src ≠ dst)
    {f : MvPolynomial (B × I) ℂ} {p q : ℕ}
    (hp : IsBlockHomogeneous src f p) (hq : IsBlockHomogeneous dst f q)
    (n : ℕ) : q + 2 * n ≤ p →
    (((blockShift ℂ src dst).toLinearMap ^ n) f = 0) → f = 0 := by
…
```
Mentions: OAI.Problem346.blockShift