ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck pass

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.

Explicit Godbillon-Vey rescaling calculation

Example

Assume Countable Choice ${A C}_{ω}$ . On $M = R^{3}$ with coordinates $(x, y, z)$ let $φ = z e^{x^{2} / 2}$ , so that $ω : = e^{- x^{2} / 2} d φ = d z + x z d x$ is a nowhere-vanishing defining form and $F = \ker ω$ is the regular codimension-one foliation by the surfaces $z = c e^{- x^{2} / 2}$ , $c \in R$ . The $1$ -form $η = (x y z - x) d x + y d z$ satisfies $d ω = η \land ω$ , and $d η = - x z d x \land d y - x y d x \land d z + d y \land d z \neq 0$ with $η \land d η = - x d x \land d y \land d z$ , nonzero where $x \neq 0$ . For the rescaled defining form $ω^{'} = e^{y} ω$ , the form $η^{'} = η + d y$ satisfies $d ω^{'} = η^{'} \land ω^{'}$ , $d η^{'} = d η$ , and $η^{'} \land d η^{'} = η \land d η + d y \land d η = η \land d η + d (y d η) = (x y - x) d x \land d y \land d z$ ; the difference is the exact form $d (y d η)$ , the explicit instance of Rescaling the defining form changes the Godbillon-Vey form by an exact form with $f = y$ .

Facts & Assumptions

Given: $R^{3}$ with coordinates $(x, y, z)$ , the function $φ = z e^{x^{2} / 2}$ , the one-form $ω = e^{- x^{2} / 2} d φ = d z + x z d x$ , and the one-form $η = (x y z - x) d x + y d z$ .

[F1]

The kernel of the differential of a constant-rank submersion is an integrable distribution whose leaves are the connected components of the level sets. (The kernel distribution of a constant-rank submersion is integrable).

[F2]

If $d ω = η \land ω$ and $ω^{'} = e^{f} ω$ , then $η^{'} = η + d f$ satisfies $d ω^{'} = η^{'} \land ω^{'}$ and $η^{'} \land d η^{'} = η \land d η + d (f d η)$ , so the two forms define the same de Rham class. (Rescaling the defining form changes the Godbillon-Vey form by an exact form).

Proof

technique · direct

1.1F1given

The function $φ = z e^{x^{2} / 2}$ has $d φ = e^{x^{2} / 2} ω$ nowhere zero, so $φ$ is a constant-rank submersion and by [F1] the common kernel $\ker ω = \ker d φ$ is an integrable codimension-one distribution whose leaves are the level surfaces $z = c e^{- x^{2} / 2}$ , $c \in R$ .

2.1givenalgebrastep 1.1

A direct calculation gives $d ω = x d z \land d x$ and $η \land ω = (x y z - x) d x \land d z + x y z d z \land d x = (- x y z + x + x y z) d z \land d x = x d z \land d x = d ω$ . Also $d η = - x z d x \land d y - x y d x \land d z + d y \land d z$ and $η \land d η = - x d x \land d y \land d z$ , which is nonzero exactly where $x \neq 0$ . The level surfaces in step 1.1 are connected graphs over the $(x, y)$ plane, so the supplier’s connected components are precisely these surfaces.

3.1F2step 2.1∎

For $ω^{'} = e^{y} ω$ one has $d ω^{'} = e^{y} (d y \land ω + d ω) = e^{y} (d y + η) \land ω = (η + d y) \land ω^{'}$ , so $η^{'} = η + d y$ is admissible with $d η^{'} = d η$ and $η^{'} \land d η^{'} = η \land d η + d y \land d η = η \land d η + d (y d η)$ ; the last term is exact by the graded Leibniz rule, so $η \land d η$ and $η^{'} \land d η^{'}$ define the same Godbillon-Vey class, which is the explicit instance of [F2] with $f = y$ , the discrepancy $(x y - x) d x \land d y \land d z = - x d x \land d y \land d z + d (y d η)$ being exactly the rescaled form modulo an exact form.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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

Steven Hurder and Remi Langevin, Dynamics and the Godbillon-Vey Class of C1 Foliations (complete author-hosted PDF) (standard reference, not scraped)