Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27
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.

Indented real-axis contours compute principal values with half-residue corrections

Statement

Let R=p/q, where p,qC[z] are nonzero, be a rational function with degqdegp+2, and assume that its real poles a1<<as are simple. For T large enough to contain all these poles and for pairwise disjoint symmetric deletion radii εj>0, put

I(T,ε):=[T,T]j=1s(ajεj,aj+εj)R(x)dx,

where the integral is the sum over the remaining compact intervals. In this statement,

PV ⁣R(x)dx:=limTε1,,εs0I(T,ε).

When s=0, the deleted union is empty and only T remains. Indent every real pole above the real axis and close the contour in the upper half-plane. Then this principal value exists and

PV ⁣R(x)dx=2πia>0Res(R,a)+iπjRes(R,aj).

The correction term is the sum of the usual positive half-residues.

Facts & Assumptions

Given: A rational function R with a two-degree denominator gap and only simple real poles, all indented above the real axis.

[L1]

At a finite singularity, a principal value uses equal left and right deletions, while on the real line it uses the symmetric truncation [T,T]; neither assertion implies separate improper convergence (Cauchy principal values at a finite singularity and on the real line, This page keeps Cauchy principal values distinct from genuine improper convergence).

[L2]

For an admissible cycle, the residue theorem gives its contour integral as 2πi times the index-weighted sum of the enclosed residues (The residue theorem for a null-homologous cycle).

[L3]

If the large upper semicircle meets no pole and supz=T,z0zR(z)0, then its integral tends to 0 (A rational large-semicircle integral vanishes under the zR(z) to 0 condition).

[L4]

An upper indentation contributes iπRes(R,a) in the limit (An indented arc around a simple singularity contributes the expected residue fraction).

Proof

technique · direct
1.1

For large T and small pairwise disjoint indentation radii εj, form the contour specified in the statement. It is an admissible positively oriented cycle, avoids every real pole, and encloses precisely the nonreal poles in the upper half-plane, so [L2] applies.

givenL2
2.1

The contour pieces have their asserted limits as T and every εj0.

givenstep 1.1L1L3L4algebra

Indeed, the straight pieces sum to I(T,ε) from the statement. The degree gap gives R(z)=O(z2), so the large semicircle eventually meets no pole and satisfies the hypothesis of [L3]. Thus its integral tends to 0. Finally, [L4] makes the jth upper indentation tend to iπRes(R,aj). [given, step 1.1, L1, L3, L4, algebra]

3.1

The residue theorem and step 2.1 give PV ⁣R(x)dxiπjRes(R,aj)=2πia>0Res(R,a). Hence the joint limit exists, and moving the indentation term to the right proves the formula.

step 1.1step 2.1L2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources