The rational-function eigenvector of the backward shifts

Nonzero edge triples give nonzero degree-at-most-two polynomials. Their images in RatFunc k are invertible. Reciprocal prefix products produce a genuine (non-finitely-supported) eigenvector on the full function space.

noncomputable def KoetheCounterexample.ShiftWitness.edgePolynomial {k : Type u} [Field k] (z : Triple k) : Polynomial k

A triple encoded as a polynomial of degree at most two.

Equations

• KoetheCounterexample.ShiftWitness.edgePolynomial z = Polynomial.C (z 0) + Polynomial.X * Polynomial.C (z 1) + Polynomial.X ^ 2 * Polynomial.C (z 2)

theorem KoetheCounterexample.ShiftWitness.edgePolynomial_ne_zero {k : Type u} [Field k] (z : Triple k) (hz : z ≠ 0) : edgePolynomial z ≠ 0

noncomputable def KoetheCounterexample.ShiftWitness.edge {k : Type u} [Field k] (z : Triple k) : RatFunc k

The polynomial edge weight embedded faithfully in the rational-function field.

Equations

• KoetheCounterexample.ShiftWitness.edge z = (algebraMap (Polynomial k) (RatFunc k)) (KoetheCounterexample.ShiftWitness.edgePolynomial z)

theorem KoetheCounterexample.ShiftWitness.edge_eq {k : Type u} [Field k] (z : Triple k) : edge z = (algebraMap k (RatFunc k)) (z 0) + RatFunc.X * (algebraMap k (RatFunc k)) (z 1) + RatFunc.X ^ 2 * (algebraMap k (RatFunc k)) (z 2)

theorem KoetheCounterexample.ShiftWitness.edge_ne_zero {k : Type u} [Field k] (z : Triple k) (hz : z ≠ 0) : edge z ≠ 0

noncomputable def KoetheCounterexample.ShiftWitness.eigenvector {k : Type u} [Field k] (v : ℕ → Triple k) : Space (RatFunc k)

Reciprocal prefix products, defined on the full sequence module.

Equations

• KoetheCounterexample.ShiftWitness.eigenvector v n = (∏ i ∈ Finset.range n, KoetheCounterexample.ShiftWitness.edge (v i))⁻¹

@[simp]

theorem KoetheCounterexample.ShiftWitness.eigenvector_zero {k : Type u} [Field k] (v : ℕ → Triple k) : eigenvector v 0 = 1

theorem KoetheCounterexample.ShiftWitness.eigenvector_ne_zero {k : Type u} [Field k] (v : ℕ → Triple k) : eigenvector v ≠ 0

theorem KoetheCounterexample.ShiftWitness.edge_mul_eigenvector_succ {k : Type u} [Field k] (v : ℕ → Triple k) (hv : ∀ (n : ℕ), v n ≠ 0) (n : ℕ) : edge (v n) * eigenvector v (n + 1) = eigenvector v n

theorem KoetheCounterexample.ShiftWitness.combined_shift_eigenvector {k : Type u} [Field k] (v : ℕ → Triple k) (hv : ∀ (n : ℕ), v n ≠ 0) : (backShift v 0 + RatFunc.X • backShift v 1 + RatFunc.X ^ 2 • backShift v 2) (eigenvector v) = eigenvector v

The combined shift with transcendental scalar coefficients fixes a nonzero vector. This is not a scalar combination over the ground field k.