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

A null characteristic frontier transports nullity to the adjacent annulus

Statement

Assume Countable Choice ${A C}_{ω}$ . Let $P$ be a regular closed characteristic orbit in a generic disk map, and suppose its based class is trivial in its ambient leaf $L$ . Then the characteristic return map on a transverse section in the disk is the ambient foliation holonomy of $P$ , hence is the identity germ. The adjacent characteristic period annuli therefore consist of closed prescribed level loops; every sufficiently close loop on either side is null-homotopic in its own leaf.

Facts & Assumptions

Given: A regular closed characteristic orbit $P$ of a generic disk map, with ambient leaf $L$ , whose based class $[P]$ is trivial in $π_{1} (L)$ (Based loops and the fundamental group), and a small transverse section in the disk at a point of $P$ .

[F1]

The holonomy representation and holonomy group of a leaf are defined on leafwise homotopy classes, so a loop whose based class is trivial in its leaf has identity holonomy germ (The holonomy representation and the holonomy group of a leaf).

[F2]

If a $C^{2}$ transverse trace annulus has leafwise loops and its base loop bounds a compact continuous leafwise disk, then the prescribed loops are null-homotopic in their own leaves for all parameters in some open interval about the base parameter (the sibling item lem-nullhomotopy-persists-under-a-compact-transverse-deformation). This is a local assertion; it supplies neither persistence throughout an arbitrary compact parameter interval nor a transport of one fixed disk map.

[F3]

The standing assumption is Countable Choice ${A C}_{ω}$ as recorded for this pair (The countable-choice principle used in the foliation pair).

Proof

technique · direct

1.1givenconstruct

Because $P$ is regular, the characteristic line field is nonzero along it and there is a small transverse section at a point of $P$ on which the first-return map of the characteristic field is defined. Along the regular orbit, foliated-chart transport on this section is exactly that first-return map: the orbit lies in the single ambient leaf $L$ and the section maps transversely to the foliation, so chartwise transport of the section along the finitely many charts covering $P$ composes to the characteristic return and to the ambient foliation holonomy simultaneously.

2.1F1step 1.1

Triviality of $[P]$ in $π_{1} (L)$ makes the holonomy germ of the transported section the identity by [F1]; hence every sufficiently close point of the section returns to itself under the first-return map, and the nearby characteristic trajectories close on both sides of $P$ . The adjacent characteristic period annuli therefore consist of closed prescribed level loops.

3.1F2step 1.1step 2.1construct

Shrink the identity-return interval of step 2.1. Finite regular characteristic strips give a jointly $C^{2}$ trace of the prescribed closed loops across $P$ : in each strip the pulled-back $C^{2}$ transverse coordinate is a submersion, so its nearby level arcs have $C^{2}$ graph parametrizations; the finite overlaps are matched by the same transverse label, and identity return closes the trace. Its point tracks are transverse to the ambient foliation, since the transverse label has nonzero parameter derivative. Fix a compact continuous leafwise filling of $P$ and apply [F2] at its base parameter. The resulting open interval contains parameters on both sides of $P$ , and every prescribed loop there is null-homotopic in its own leaf. No continuation to distant levels or transport of the original disk parametrization is required.

4.1F2F3step 3.1∎

Therefore the return map is the ambient holonomy, it is the identity germ, the adjacent annuli are closed level loops, and every sufficiently close loop on either side is null-homotopic in its leaf; the argument is asserted for regular orbits only and does not identify holonomy with the characteristic return across a saddle polycycle, and it uses only the fixed nullhomotopy and finitely many charts, hence only the standing countable choice from [F3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

S. P. Novikov, The Topology of Foliations (English translation by J. A. Zilber; complete PDF of the translation) (standard reference, not scraped)