LemmaStatement: Literature-sourcedProof: Literature-sourcedprecheck 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.

Frobenius divisibility: d omega equals eta wedge omega

Statement

Assume Countable Choice ${A C}_{ω}$ . Let $F$ be a transversely oriented codimension-one foliation of a smooth manifold $M$ with nowhere-vanishing defining $1$ -form $ω$ , so $T F = \ker ω$ . Then $ω \land d ω = 0$ and there exists a smooth $1$ -form $η$ on $M$ with $d ω = η \land ω$ . If $η^{'}$ is another such form, then $η^{'} - η = f ω$ for a unique $f \in C^{\infty} (M)$ .

Facts & Assumptions

Given: A transversely oriented codimension-one foliation $F$ of a smooth manifold $M$ with nowhere-vanishing defining one-form $ω$ , so $T F = \ker ω$ , and the standing countable choice assumption.

[F1]

For a nowhere-zero one-form $α$ , the hyperplane distribution $\ker α$ is integrable if and only if $α \land d α = 0$ . (The codimension-one Frobenius criterion).

[F2]

If $ω$ is nowhere vanishing, then $α \land ω = 0$ for a one-form $α$ forces $α = f ω$ for a unique smooth $f$ , and $θ \land ω = 0$ for a two-form $θ$ forces $θ = β \land ω$ for a smooth one-form $β$ . (Divisibility by a nowhere-vanishing one-form).

[F3]

The wedge product of alternating forms is associative and graded-commutative, so for forms of odd degree $α \land β = - β \land α$ . (The wedge product is associative and graded commutative).

Proof

technique · direct

1.1F1F3given

Since $F$ is integrable with $T F = \ker ω$ , the Frobenius criterion [F1] gives $ω \land d ω = 0$ , and by the graded commutativity of [F3] with degrees one and two (and hence sign $(- 1)^{1 \cdot 2} = 1$ ) this is equivalent to $d ω \land ω = 0$ .

2.1F2step 1.1

Applying the divisibility lemma [F2] to the two-form $θ = d ω$ with $θ \land ω = 0$ produces a smooth one-form $η$ with $d ω = η \land ω$ .

3.1F2step 2.1∎

If $η^{'}$ is another one-form with $d ω = η^{'} \land ω$ , then $(η^{'} - η) \land ω = 0$ , so by part (i) of [F2] there is a unique smooth $f$ with $η^{'} - η = f ω$ ; evaluating at any vector field $X$ with $ω (X) = 1$ gives $f = η^{'} (X) - η (X)$ , which both exhibits $f$ and proves its uniqueness, and no choice principle beyond the standing vocabulary is used.

Depends on

Used by

Dependency tree · two levels

25 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)