FirstTransfer.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem346.firstPolynomial_zero_of_chain line 19

Source documentation

Cancel the first transfer sequence from its zero endpoint. The homogeneous and derivative identities are kept separate from this zero-reflection argument.

theorem firstPolynomial_zero_of_chain {r m : ℕ}
    (T : SymmetricMultilinearForm (r+1) (r+m) V) (e : κ → V)
    (ht : ∀ k < m, PolynomialWeights.IsBlockHomogeneous (some none)
      (firstPolynomial T e k) (r+m-k))
    (hy : ∀ (k : ℕ) (hk : k < m), PolynomialWeights.IsBlockHomogeneous
      (some (some (⟨k,hk⟩ : Fin m))) (firstPolynomial T e k) r)
    (hD : ∀ (k : ℕ) (hk : k < m),
      PolynomialShift.shift (some none) (some (some (⟨k,hk⟩ : Fin m)))
        (firstPolynomial T e k) = ((r+m-k : ℕ) : ℂ) • firstPolynomial T e (k+1))
    (hm : firstPolynomial T e m = 0) : firstPolynomial T e 0 = 0 := by
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.PolynomialWeights.IsBlockHomogeneous, OAI.Problem346.firstPolynomial, OAI.Problem346.PolynomialShift.shift

theorem OAI.Problem346.firstPolynomial_zero_of_final line 39
Source documentation
Every terminal-zero polynomial in the concrete first-transfer family is zero at the initial stage. All degree counts and derivative identities are discharged.
```
theorem firstPolynomial_zero_of_final {r m : ℕ}
    (T : SymmetricMultilinearForm (r+1) (r+m) V) (e : κ → V)
    (hm : firstPolynomial T e m = 0) : firstPolynomial T e 0 = 0 := by
…
```
Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.firstPolynomial

theorem OAI.Problem346.first_transfer line 59

Source documentation

The first transfer in the stabilization argument: the common product can be removed from the distinguished argument, while the other arguments remain fixed. No outer symmetry or positive-degree assumptions are needed for this step.

theorem first_transfer [FiniteDimensional ℂ V] {r m : ℕ}
    (T : SymmetricMultilinearForm (r+1) (r+m) V)
    (h : ∀ (x t : V) (y : Fin m → V),
      T (Fin.cons (symPowMul r m (symMonomial r V (fun _ => t)) (symMonomial m V y))
        (fun _ => symPowMul r m (symMonomial r V (fun _ => x)) (symMonomial m V y))) = 0) :
    ∀ (x t : V) (y : Fin m → V),
      T (Fin.cons (symMonomial (r+m) V (fun _ => t))
        (fun _ => symPowMul r m (symMonomial r V (fun _ => x)) (symMonomial m V y))) = 0 := by
…

Mentions: OAI.Problem346.SymmetricMultilinearForm, OAI.Problem346.symPowMul, OAI.Problem346.symMonomial