Prove2Me

Finite truncated-log interpolation matrix is surjective at distinct centers

Disproved
OAI.PiExponent.FormalInterpolation.finite_truncated_log_matrix_surjective_of_distinct_centers

by Eyal1990 · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

For any column weight and truncation data, distinct center profiles make the finite truncated-log interpolation matrix surjective onto the row packet space.

Preamble
import Definitions.Def_OAI_PiExponent_TruncatedPolynomialJets

open OAI.PiExponent OAI.PiExponent.DeterminantContradiction OAI.PiExponent.FormalInterpolation
Formal statement
theorem OAI.PiExponent.FormalInterpolation.finite_truncated_log_matrix_surjective_of_distinct_centers
    {m : Nat} (K : Nat) (w0 v0 theta : Real) (w : Fin m → Real) (H : Real)
    (r : Fin m → Complex) (T : Fin m → Nat)
    (hcenters : Function.Injective
      (fun j : Fin K => fun i : Fin m => (j.val : Complex) * r i)) :
    Function.Surjective
      (InterpolationMatrix.truncatedLogMatrix K w0 v0 theta w H r T).mulVecLin := by sorry

View graph