Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 3 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Minimax approximation and Remez algorithms — Examples

1 · Prerequisites

2 · Summary

The examples compute the degree-one best uniform approximation to x squared on [-1,1], solve and certify a two-node degree-zero Remez system, and exhibit a defective type (1,1) rational minimizer with three rather than four alternating extrema.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A two-node degree-zero Remez certificate

Example

For $f (x) = ∣ x ∣$ on $[- 1, 1]$ , degree $n = 0$ , and initial nodes $x_{0} = 0, x_{1} = 1$ , the Remez linear system returns $p (x) = 1 / 2$ and signed level $λ = - 1 / 2$ . An exact global-extrema oracle returns error $1 / 2$ , so the current reference is an optimality certificate.

Verification

Given: $I = [- 1, 1]$ , $f (x) = ∣ x ∣$ , $n = 0$ , reference $X = (0, 1)$ , and an exact extrema oracle as in Finite-budget polynomial Remez exchange with an exact extrema oracle that returns maximum $(1 / 2, 0)$ on the first candidate $p = 1 / 2$ .

[F1] The Remez alternation linear system has a unique solution: at two distinct nodes the degree-zero alternation equations have a unique solution $(p, λ)$ .

[F2] Finite-budget polynomial Remez exchange with an exact extrema oracle: with equations $p (x_{i}) + (- 1)^{i} λ = f (x_{i})$ , a maximum $(E, y)$ response with $E = ∣ λ ∣ > 0$ returns certified $(p, E, X)$ using the current reference.

[F3] Exact polynomial equioscillation certifies best approximation: exact global equioscillation at $n + 2$ ordered nodes certifies best approximation.

1.1givenF1algebra

The equations at $x_{0} = 0, x_{1} = 1$ are $p + λ = 0$ and $p - λ = 1$ . Adding them gives $2 p = 1$ , so $p = 1 / 2$ and then $λ = - 1 / 2$ , in agreement with the unique solve [F1].

2.1F2F3step 1.1givenalgebra∎

For every $x \in [- 1, 1]$ , $∣ x ∣ \in [0, 1]$ , so $- ∣ 1 / 2 ∣ \leq ∣ x ∣ - 1 / 2 \leq 1 / 2$ and the absolute error is at most $1 / 2$ . It equals $1 / 2$ at $x = 0$ and at $x = 1$ (also at $x = - 1$ ), so the stipulated response maximum $(1 / 2, 0)$ is valid and has $E = 1 / 2 = ∣ λ ∣$ . The residuals at $(0, 1)$ are $- 1 / 2, 1 / 2$ , hence with this maximum response the procedure returns certified $(p, 1 / 2, X)$ by [F2], and [F3] makes $p$ best.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

The degree-one minimax approximation to x squared

Example

On $[- 1, 1]$ , the unique best degree-one uniform approximation to $f (x) = x^{2}$ is the constant polynomial $p (x) = 1 / 2$ , with error $1 / 2$ .

Verification

Given: $I = [- 1, 1]$ , $f (x) = x^{2}$ , $p (x) = 1 / 2 \in P_{1} (I)$ .

[F1] Best uniform polynomial error on a compact interval: $E_{1} (f; I)$ is the infimum of $∥ f - q ∥_{\infty, I}$ over real polynomials $q$ of degree at most $1$ .

[F2] Exact polynomial equioscillation certifies best approximation: a degree- $n$ candidate with exact uniform error $E > 0$ and $n + 2$ ordered alternating extrema is a best approximant.

[F3] The best uniform polynomial approximant is unique: the best degree- $n$ approximant exists and is unique for every continuous real target on a nondegenerate compact interval.

1.1givenalgebra

For $x \in [- 1, 1]$ , $0 \leq x^{2} \leq 1$ , so $- 1 / 2 \leq x^{2} - 1 / 2 \leq 1 / 2$ . Equality occurs at $x = 0$ and at $x = \pm 1$ , hence $∥ f - p ∥_{\infty, I} = 1 / 2$ .

2.1F1F2F3step 1.1algebra∎

The ordered points $- 1 < 0 < 1$ give residual values $1 / 2, - 1 / 2, 1 / 2$ . By [F2], $p$ is a best degree-one approximant; [F1] identifies its error with $E_{1} (f; I)$ , and [F3] makes it unique.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A defective rational minimizer can have fewer than m+n+2 extrema

Statement refuted

Every best real rational approximant of type $(m, n)$ with positive error has at least $m + n + 2$ distinct alternating global extrema.

Facts & Assumptions

Given: $I = [- 1, 1]$ , $f (x) = x^{2}$ , weight $w (x) = 1$ , type $(m, n) = (1, 1)$ , and $r (x) = 1 / 2$ .

[F1]

Weighted rational minimax families and defect: type $(m, n)$ candidates have degree bounds $(m, n)$ ; the defect of a nonzero reduced candidate is $d = \min (m - \deg p, n - \deg q)$ .

[F2]

Weighted rational minimizers satisfy the defect-sensitive alternation criterion: a candidate with positive error is best exactly when its error has $m + n + 2 - d$ ordered alternating global extrema.

Counterexample

1.1F1givenalgebra

The pair $p = 1 / 2, q = 1$ is reduced, has $q > 0$ , coefficient norm $1$ , degrees $(0, 0)$ , and error $f - r = x^{2} - 1 / 2$ . Since $x^{2} \in [0, 1]$ , this residual lies in $[- 1 / 2, 1 / 2]$ and its absolute value reaches $1 / 2$ exactly at $x = - 1, 0, 1$ . The extremal residual signs in order are $+, -, +$ .

2.1F1F2step 1.1algebra∎

Here $d = \min (1 - 0, 1 - 0) = 1$ , so the defect-sensitive count is $1 + 1 + 2 - 1 = 3$ . By [F2], the three alternating extrema make $r = 1 / 2$ a best type- $(1, 1)$ rational approximant. The extremal set is exactly ${- 1, 0, 1}$ , so there are not four distinct global extrema; the refuted $m + n + 2 = 4$ count fails.

Minimax approximation and Remez algorithms — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A two-node degree-zero Remez certificate

Example

Verification

The degree-one minimax approximation to x squared

Example

Verification

A defective rational minimizer can have fewer than m+n+2 extrema

Statement refuted

Facts & Assumptions

Counterexample

Sources