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

Peano's mixed-partial theorem from continuity of one mixed partial

Statement

Let ff have fxyf_{xy} in a neighbourhood of (a,b)(a,b), with fxyf_{xy} continuous at (a,b)(a,b), and let fyx(a,b)f_{yx}(a,b) exist. Then fxy(a,b)=fyx(a,b)f_{xy}(a,b)=f_{yx}(a,b).

Facts & Assumptions

Given: The hypotheses in the statement.

[L1]

When fxf_x and fxyf_{xy} exist on a neighbourhood of a rectangle, its rectangular second difference is the product of the side lengths and a value of fxyf_{xy} (A rectangular second difference equals a mixed partial times the side lengths).

Proof

technique · direct
1.1

For sufficiently small nonzero h,kh,k, apply [L1] to the rectangle with corners (a,b)(a,b) and (a+h,b+k)(a+h,b+k). After division by hkhk, continuity of fxyf_{xy} at (a,b)(a,b) makes the limit, as h,k→0h,k\to0, equal to fxy(a,b)f_{xy}(a,b).

L1givenalgebra
2.1

For fixed nonzero hh, first let k→0k\to0 in the same rectangle quotient; it becomes (fy(a+h,b)−fy(a,b))/h\bigl(f_y(a+h,b)-f_y(a,b)\bigr)/h. Letting h→0h\to0 gives the defining quotient for fyx(a,b)f_{yx}(a,b).

step 1.1givenalgebra
3.1

The two limits are equal, proving fxy(a,b)=fyx(a,b)f_{xy}(a,b)=f_{yx}(a,b).

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 12 results over 7 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources