Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-06
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.

Gradient flow for a Morse function on the flat torus

Example

On the flat torus with angular coordinates (θ,ϕ), take f(θ,ϕ)=cos⁡θ+cos⁡ϕ. Its critical points are (0,0) (maximum, index 2), (π,0) and (0,π) (saddles, index 1), and (π,π) (minimum, index 0). The negative-gradient equations are

θ˙=sin⁡θ,ϕ˙=sin⁡ϕ.

Verification

Given: The flat two-torus and f(θ,ϕ)=cos⁡θ+cos⁡ϕ.

1.1givenalgebra

Differentiating gives df=−sin⁡θ dθ−sin⁡ϕ dϕ, hence the displayed negative-gradient equations. Their zeros give exactly the four listed critical points, and the diagonal Hessian diag⁡(−cos⁡θ,−cos⁡ϕ) gives the stated indices.

2.1step 1.1algebra∎

The circles θ∈{0,π} and ϕ∈{0,π} are invariant and supply the coordinate-circle separatrices. On either component of S1∖{0,π}, each nonconstant coordinate trajectory has backward limit 0 and forward limit π (it increases on (0,π) and decreases on (π,2π) in the displayed coordinate). Thus the trajectories off those circles run from the maximum to the minimum in four arc-choice components. In each component, quotienting the two integration constants by common time translation leaves a one-parameter family.

Used by

Nothing in the library uses this result yet.

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources