ExampleConstruction: Literature-sourcedVerification: 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.

A fibre foliation of a mapping torus is taut

Example

Assume Countable Choice ${A C}_{ω}$ . Let $L$ be a nonempty closed connected smooth manifold and $f : L \to L$ a diffeomorphism, with mapping torus $M_{f} = (L \times R) / Z$ , where $k \cdot (x, t) = (f^{k} (x), t + k)$ , and fibre foliation $F_{f}$ (Mapping torus foliations realize global Reeb stable examples). Every leaf is compact and diffeomorphic to $L$ . There is a smooth path $a : [0, 1] \to L$ , constant near its endpoints, with $a (1) = f (a (0))$ , and its graph $t \mapsto [a (t), t]$ descends to a smooth embedded closed transversal meeting every fibre exactly once. Consequently $F_{f}$ is taut and a single closed transversal meets all its leaves.

Facts & Assumptions

Given: A nonempty closed connected smooth manifold $L$ , a diffeomorphism $f : L \to L$ , the mapping torus $M_{f} = (L \times R) / Z$ with its fibre foliation $F_{f}$ whose leaves are the fibres $L \times {t}$ .

[F1]

The mapping-torus foliations realize the global Reeb-stable examples: the fibres of $M_{f}$ are the leaves of $F_{f}$ , each diffeomorphic to $L$ and compact (Mapping torus foliations realize global Reeb stable examples).

[F2]

A foliation is taut when every leaf admits a closed transversal (Taut codimension-one foliations), and on a nonempty compact connected manifold the leaf-by-leaf condition is equivalent to the existence of a single closed transversal meeting every leaf (A taut foliation of a compact connected manifold has a single closed transversal).

[F3]

Gluing two Reeb components gives a foliation of the three-sphere and A Reeb component obstructs tautness give the negative comparison, the non-taut Reeb foliation of $S^{3}$ ; the standing assumption is Countable Choice ${A C}_{ω}$ as recorded for this pair (The countable-choice principle used in the foliation pair).

Verification

technique · direct

1.1F3

Gluing the two standard Reeb solid tori produces the Reeb foliation of $S^{3}$ , with their common boundary torus a leaf and each torus a Reeb component. The Reeb-component obstruction implies that no closed transversal meets that boundary leaf, so the resulting foliation is not taut. This supplies the negative comparison directly from the general obstruction.

1.2givenconstruct

A connected smooth manifold is path connected, so join a chosen $x_{0} \in L$ to $f (x_{0})$ by a finite smooth chartwise path, smooth its finitely many corners and reparametrize it to be constant near $0$ and $1$ ; this gives a smooth path $a : [0, 1] \to L$ with $a (0) = x_{0}$ , $a (1) = f (x_{0})$ and stationary ends.

2.1F1step 1.2

Extend $a$ by $a (t + k) = f^{k} (a (t))$ ; the stationary ends make the extension smooth across every integer, and the graph $t \mapsto [a (t), t]$ is periodic under the diagonal mapping-torus action $k \cdot (x, t) = (f^{k} (x), t + k)$ , hence descends to a smooth closed curve in $M_{f}$ .

3.1F1step 2.1

The descended curve is embedded because its composition with the base projection $S^{1} \to S^{1}$ is the identity, so distinct parameters have distinct images; its derivative has base component $1$ , so it is everywhere positively transverse to the fibre foliation $F_{f}$ .

4.1F2step 3.1

The curve meets every fibre exactly once, because the base component of its parametrization runs monotonically once around the circle; hence the leaf-by-leaf condition of tautness holds for $F_{f}$ directly, with no fixed point of $f$ assumed.

5.1F2F3step 4.1∎

Since $L$ is nonempty, $M_{f}$ is nonempty, compact and connected, [F2] upgrades the leaf-by-leaf condition to a single closed transversal meeting every leaf, so $F_{f}$ is taut and a single closed transversal meets all its leaves. This verifies the positive model dual to the non-taut Reeb foliation example [F3], and the construction uses one finite chartwise path, hence only the standing countable choice from [F3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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

Danny Calegari, Foliations and the Geometry of 3-Manifolds (Oxford Mathematical Monographs; complete author-hosted PDF) (standard reference, not scraped)
Samuel Ranz, Approximately Holomorphic Techniques in Foliations: A Simple Proof of Novikov's Theorem (PhD thesis, Universidad Autonoma de Madrid, 2024; complete PDF) (standard reference, not scraped)