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.

Clairaut--Schwarz theorem for continuous second partial derivatives

Statement

If ff is C2C^2 on an open subset of Rm\mathbb R^m, then ∂i∂jf=∂j∂if\partial_i\partial_j f=\partial_j\partial_i f for every pair of coordinate indices.

Facts & Assumptions

Given: A C2C^2 scalar field and coordinate indices i,j<mi,j<m.

[L1]

If fxyf_{xy} exists on a neighbourhood of a point and is continuous at that point, while fyxf_{yx} exists there, then the two values are equal (Peano's mixed-partial theorem from continuity of one mixed partial).

[L2]

The C2C^2 condition supplies every ordered partial derivative of length at most two, continuously on the open set (CkC^k maps and multi-index derivative notation in Euclidean space).

Proof

technique · direct
1.1

At an arbitrary point, [L2] supplies ∂i∂jf\partial_i\partial_jf on a neighbourhood and continuously there, as well as the reversed partial ∂j∂if\partial_j\partial_if at the point.

L2given
2.1

Apply [L1] at an arbitrary point to obtain ∂i∂jf=∂j∂if\partial_i\partial_j f=\partial_j\partial_i f.

step 1.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 43 results over 14 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