Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

A bounded even window from an odd sign approximant

Statement

Let 0<η<1, 0<g≤t, and s>0 satisfy s+t≤1. Let S be an odd real polynomial such that ∣S(y)∣≤1 for y∈[−1,1] and ∣S(y)−sgn⁡(y)∣≤η/2 whenever y∈[−1,1] and ∣y∣≥g. Define R(x)=1−η2(S(x+t)+S(t−x))+η2,D(x)=1−S(x+t)+S(t−x)2 for x∈[−s,s]. Then R and D are even polynomials, each has degree at most deg⁡S, and 0≤R(x)≤1 for all x∈[−s,s]. On ∣x∣≤t−g, 1−η≤R(x)≤1 and ∣D(x)∣≤η/(2(1−η)). On ∣x∣≥t+g, 0≤R(x)≤η and ∣D(x)−1∣≤η/(2(1−η)). Globally, −η2(1−η)≤D(x)≤1+η2(1−η). The inner or outer interval may be empty, in which case its corresponding assertion is vacuous.

Facts & Assumptions

Given: η,g,t,s,S satisfy the hypotheses in the Statement; sgn⁡(y)=1 for y>0 and −1 for y<0.

[A1]

S is odd and ∣S(y)∣≤1 on [−1,1].

[A2]

For y∈[−1,1] with ∣y∣≥g, S(y) differs from sgn⁡(y) by at most η/2.

Proof

1.1givenA1algebra

Replacing x by −x interchanges the two summands in each definition, so R and D are even. Each summand is a translate of S and has degree at most deg⁡S; addition and scalar multiplication do not increase that bound.

1.2givenA1A2algebra

Put u=t+x and v=t−x. Since ∣x∣≤s and s+t≤1, each of u,v is at most t+s≤1 and at least t−s≥2t−1≥−1; also u+v=2t≥2g. If both u,v≥g, [A2] gives S(u)+S(v)≥2−η. Otherwise one of them, say u, is less than g, and then v=2t−u>2g−u>g; [A1]–[A2] give S(u)+S(v)≥−1+(1−η/2)=−η/2. In every case [A1] also gives S(u)+S(v)≤2. Thus −η/2≤S(u)+S(v)≤2, and substitution into the formula for R yields η(1+η)/4≤R(x)≤1−η/2, which implies 0≤R(x)≤1.

2.1givenA1A2step 1.2algebra

If ∣x∣≤t−g, both u=t+x and v=t−x are at least g. Their sign approximations lie in [1−η/2,1] by [A1]–[A2], so 2−η≤S(u)+S(v)≤2. Substituting gives 1−η+η2/2≤R(x)≤1−η/2, hence 1−η≤R(x)≤1. Since D(x)=(1−η/2−R(x))/(1−η), the interval R(x)∈[1−η,1] gives ∣D(x)∣≤η/(2(1−η)).

3.1givenA1A2step 1.1algebra

If x≥t+g, then u≥g and v≤−g. By [A1]–[A2], S(u)∈[1−η/2,1] and S(v)∈[−1,−1+η/2], so ∣S(u)+S(v)∣≤η. Evenness gives the same conclusion for x≤−(t+g). Substitution into R gives R(x)∈[η2/2,η−η2/2]⊆[0,η]. The identity for D in step 2.1 then gives ∣D(x)−1∣≤η/(2(1−η)).

4.1givenstep 1.2algebra∎

Step 1.2 gives R(x)∈[0,1]. Using D(x)=(1−η/2−R(x))/(1−η), its minimum over that interval is −η/(2(1−η)) and its maximum is 1+η/(2(1−η)). This proves the global bound.

Remarks

With a=1+t0, the OP1A expression 1+(S((x−t0)/a)−S((x+t0)/a))/2 is the D above after substituting x/a for the lemma variable and t0/a for t. The lemma domain uses s=1/a, so s+t=1, and g=δ/(4a) gives t=3g; its inner and outer thresholds are t−g=δ/(2a) and t+g=δ/a. For OP1A, take η=2v with its parameter v=e/(1000Pmax⁡); then the required approximation error is η/2=v. Subject to the OP1A SignPoly certificate proving that error and the bound ∣S∣≤1, all evaluations stay on [−1,1], where OP1A states those properties. It does not prove the separate Chebyshev interpolation, inverse approximation, Bernstein-refinement termination, or bit-cost obligations of OP1A. The displayed formula in Gilyén et al. Lemma 29 is not invoked here.

Used by

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources