Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)
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.

Christoffel symbols in polar coordinates

Example

For the Euclidean plane in a polar chart (r,θ) with r>0, the metric is dr2+r2dθ2. Its only nonzero Levi–Civita symbols are Γrθθ=r and Γθrθ=Γθθr=1/r.

Facts & Assumptions

Given: A polar chart with angular interval small enough that (r,θ)(rcosθ,rsinθ) is injective, and r>0.

[F1]

Γkij=12gk(igj+jgigij) (Christoffel formula for the levi civita connection).

Verification

1.1

Differentiating the coordinate map gives vectors (cosθ,sinθ) and (rsinθ,rcosθ), whose inner products are 1,0,r2. Thus G=diag(1,r2), G1=diag(1,r2), and the only nonzero metric derivative is rgθθ=2r. Formula [F1] gives Γrθθ=(2r)/2=r and Γθrθ=Γθθr=(2r)/(2r2)=1/r.

F1given
2.1

The remaining entries are Γrrr=Γrrθ=Γrθr=Γθrr=Γθθθ=0. For the first and fourth, every metric derivative is zero. In the middle two the only potentially nonzero term rgθθ is multiplied by grθ=0; in the last, the term rgθθ is multiplied by gθr=0. At r=1 the three displayed nonzero entries are 1,1,1. None of these formulas applies at r=0: there the angular coordinate vector vanishes and the coordinate map is not a chart. There is therefore no singularity of the Euclidean metric asserted at the origin.

F1step 1.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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