Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated
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.

Translation of a Dirac mass

Example

Assume AC. Let d≥1 be an integer, T>0, and a,b∈Rd. The curve μt=δa+tb belongs to AC2([0,T];P2(Rd)), has constant metric speed ∣b∣, and the Borel field vt(x)=b solves the continuity equation. Its action is T∣b∣2, equal to the minimum action among fields solving that equation for this curve.

Facts & Assumptions

Given: AC, an integer d≥1, T>0, and a,b∈Rd.

[F1]

A coupling of two Dirac laws is forced to put all mass at the sole pair of support points, so the quadratic Wasserstein distance is W2(δx,δy)=∣x−y∣. The Euclidean quadratic Wasserstein space The Dirac set function at a point

[F2]

For a continuously differentiable scalar function, the total-derivative chain rule and fundamental theorem identify the integral of its derivative with its endpoint difference. The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a) The second fundamental theorem: if G is differentiable on [a,b] with G′=f and f is integrable, then ∫abf=G(b)−G(a)

[F3]

The minimum-velocity theorem says the least action of any admissible velocity for an AC2 curve is the integral of its squared metric speed. AC2 curves admit a unique minimum-action velocity field

Proof

1.1givenF1

For s,t∈[0,T], any coupling of δa+sb and δa+tb is concentrated at ((a+sb),(a+tb)), hence [F1] gives W2(μs,μt)=∣t−s∣∣b∣. For every bounded continuous f, f(a+tb) is continuous, so the curve is narrowly continuous. Thus it is AC2 with constant metric derivative ∣b∣ (the endpoint difference quotient is exactly ∣b∣ at every interior time).

2.1F2F3step 1.1∎

For φ∈Cc∞((0,T)×Rd), the chain rule gives ddtφ(t,a+tb)=∂tφ(t,a+tb)+∇xφ(t,a+tb)⋅b. The left side integrates to zero over [0,T] because the test vanishes near both time endpoints; this is exactly the weak continuity-equation identity for μt=δa+tb and vt=b. Its action is ∫0T∣b∣2dt=T∣b∣2. By [F3] and step 1.1, this equals ∫0T∣μ˙t∣2dt, the minimum action.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

58 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