Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16
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.

The integral of complex conjugation from -1 to 1 differs along a semicircle and a polygonal path

Example

Let γ(t)=ei(π−t) for 0≤t≤π, the upper semicircle from −1 to 1, and let η be the polygonal path −1→2i→1. Then ∫γz‾ dz=−πi,∫ηz‾ dz=−4i.

Facts & Assumptions

Given: The two oriented paths from −1 to 1.

[L1]

Piecewise-C1 contour integrals agree with the parametric formula (For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals).

[L2]

Complex line integrals add under concatenation and change sign under reversal (Complex line integrals change sign under reversal and add under concatenation).

Verification

technique · direct
1.1L1algebra

Along γ, γ(t)‾γ′(t)=e−i(π−t)(−i)ei(π−t)=−i, so [L1] integrated from 0 to π gives −πi.

1.2L1algebra

On a segment z(t)=z0+td with 0≤t≤1, direct integration gives ∫z‾ dz=z0‾d+∣d∣2/2. For −1→2i we have z0=−1 and d=1+2i, so ∣d∣2=5 and the value is (−1)(1+2i)+5/2=3/2−2i; for 2i→1 we have z0=2i and d=1−2i, so ∣d∣2=5 and the value is (−2i)(1−2i)+5/2=−3/2−2i.

2.1step 1.1step 1.2L2∎

Add the two segment values by [L2]: (3/2−2i)+(−3/2−2i)=−4i. Since −πi≠−4i, the unequal results prove path dependence.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

14 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