Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)
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.

A periodic C1 characteristic map is an orientation-preserving diffeomorphism

Statement

Under the hypotheses of A periodic C1 velocity has a global characteristic flow on a finite horizon, fix s,t∈[0,T] and let Φt,s(x):=X(t;s,x) on the periodic lift Rd. Then Φt,s is a C1 diffeomorphism with inverse Φs,t, and det⁡DxΦt,s(x)>0(x∈Rd).

Facts & Assumptions

Given: The periodic C1 flow from time s to time t on Rd.

[F1]

A periodic C1 velocity has a global characteristic flow on a finite horizon: the lifted characteristic exists uniquely over [0,T] for every initial point.

[F2]

Transport characteristics depend C^1 on the initial position: for a C1 field, the flow depends C1 on its initial position over a common compact time interval.

[F3]

The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a): derivatives of a composition multiply in the order D(g∘f)=Dg(f)Df.

[F4]

A finite square real matrix is invertible if and only if its determinant is nonzero: a finite square real matrix is invertible exactly when its determinant is nonzero.

[F5]

For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries: for fixed finite dimension, determinant is a polynomial and hence a continuous function of the matrix entries.

[F6]

Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b): a continuous real function on an interval cannot pass from a positive value to a negative value without taking zero.

Proof

1.1givenF1F2algebra

By [F1], both the forward flow Φt,s and the reverse-time flow Φs,t are defined. Uniqueness of the ODE implies that following the same characteristic first from s to t and then backward to s returns the initial point; likewise in the opposite order. Thus Φs,t∘Φt,s=id and Φt,s∘Φs,t=id. By [F2] both maps are C1, so Φt,s is a C1 diffeomorphism.

2.1step 1.1F3F4algebra

Applying [F3] to Φs,t∘Φt,s=id gives DΦs,t(Φt,s(x))DΦt,s(x)=Id. Hence DΦt,s(x) is invertible, and [F4] gives det⁡DΦt,s(x)≠0.

3.1givenF2F5F6step 2.1algebra∎

For fixed s,x, the function r↦det⁡DΦr,s(x) is continuous by [F2] and [F5], and equals 1 at r=s. It never vanishes by step 2.1. If it were negative at some r, [F6] on the interval between s and r would force a zero, a contradiction. Therefore it is positive at every r, including the chosen t.

Depends on

Used by

Dependency tree · two levels

45 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