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 and let on the periodic lift . Then is a diffeomorphism with inverse , and
Facts & Assumptions
Given: The periodic flow from time to time on .
A periodic C1 velocity has a global characteristic flow on a finite horizon: the lifted characteristic exists uniquely over for every initial point.
Transport characteristics depend C^1 on the initial position: for a field, the flow depends on its initial position over a common compact time interval.
The chain rule for total derivatives: : derivatives of a composition multiply in the order .
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.
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.
Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on takes every value between and : a continuous real function on an interval cannot pass from a positive value to a negative value without taking zero.
Proof
By [F1], both the forward flow and the reverse-time flow are defined. Uniqueness of the ODE implies that following the same characteristic first from to and then backward to returns the initial point; likewise in the opposite order. Thus and . By [F2] both maps are , so is a diffeomorphism.
Applying [F3] to gives . Hence is invertible, and [F4] gives .
For fixed , the function is continuous by [F2] and [F5], and equals at . It never vanishes by step 2.1. If it were negative at some , [F6] on the interval between and would force a zero, a contradiction. Therefore it is positive at every , including the chosen .
Depends on
- A periodic C1 velocity has a global characteristic flow on a finite horizon
- Transport characteristics depend C^1 on the initial position
- The chain rule for total derivatives: $D(g\circ f)(a)=Dg(f(a))\circ Df(a)$
- For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries
- A finite square real matrix is invertible if and only if its determinant is nonzero
- 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)$
Used by
- Characteristic-cell overlap remapping for a conservative density Definition
- A smooth deforming flow remaps two cell averages conservatively Example
- Characteristic departure cells are measurable and have positive finite volume Lemma
- Characteristic-cell overlap remapping preserves mass and positivity Theorem
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
- European Centre for Medium-Range Weather Forecasts, Numerical Methods, Meteorological Training Course Lecture Series, 2002 (standard reference, not scraped)
- Lukas Einkemmer and Alexander Ostermann, On the error propagation of semi-Lagrange and Fourier methods for advection problems, Computers & Mathematics with Applications 69 (2015), 170–179 (standard reference, not scraped)