Alphabeta Math
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-homotopic closed transversal yields a vanishing cycle

Statement

Assume Countable Choice ACω. Let F be a C2 cooriented codimension- one foliation of a closed oriented 3-manifold M and let γ:S1→M be a closed transversal that is null-homotopic in M. Then F admits a vanishing cycle.

Facts & Assumptions

Given: Assume ACω. A C2 cooriented codimension-one foliation F of a closed oriented 3-manifold M and a closed transversal γ:S1→M that is null-homotopic in M.

[F1]

A vanishing cycle supported on a leaf L1 is a jointly C2 family of leafwise loops σt with [σ1] nonzero in π1(L1), each σt null-homotopic in Lt for t<1, and transverse trace. (Vanishing cycles of a codimension-one foliation).

[F2]

Under ACω, the embedding and neighborhood retraction constructed in Relative Whitney approximation for manifold-valued maps, Facts L1 and Proof 1.1, can be fixed for the smooth ambient target. Whitney approximation for Euclidean-valued maps approximates a continuous Euclidean map uniformly on a compact disk. Finite general position for a leafwise loop supplies regular C² representatives of intrinsic leaf-loop classes.

[F3]

The generic-position supplier assumes a C² defining form, but a C² atlas supplies only C¹ forms dz. Its proof still applies: singularities are critical points of u=z∘h; collar adjustment uses a smooth positive transverse flow and continuity; interior perturbations are u↦u+ρ a⋅x. The gradient is C¹, so Sard applies in equal source and target dimension two. Compactness preserves earlier nondegenerate cores. No operation differentiates the defining form twice. The cited proof therefore supplies the required genericity from a C² atlas and C¹ defining form.

Proof

technique · direct
1.1F2givenconstruct

The nullhomotopy supplies a continuous filling of the C² transversal γ. Compress it into a smaller concentric disk and set it equal to γ(θ) on an outer radial collar, extended slightly beyond the boundary. Fix the embedding and neighborhood retraction of F2, approximate the embedded filling smoothly, and blend with the original C² map using a cutoff supported in that collar and equal to one near the boundary. A small uniform error keeps the blend inside the retraction neighborhood. Retraction gives a C² filling with exactly the prescribed boundary and collar. Its characteristic tangential derivative is nonzero there because γ is transverse.

2.1F3step 1.1

Apply the finite gradient perturbations of F3, the proof of Relative generic position for characteristic disk maps, fixing the already regular transverse collar. This gives a relative generic C² characteristic disk without assuming a C² defining form.

3.1F1step 2.1

Applying the transverse-boundary alternative of the finite characteristic-disk supplier (A characteristic disk with essential boundary data produces a vanishing cycle) produces a vanishing cycle in the sense of [F1] on the side approached by the family.

4.1step 3.1∎

Thus F admits a vanishing cycle; the richer Haefliger original-disk minimal-cycle claim is retained separately and is not used as a prerequisite, and only the standing countable choice is invoked.

Depends on

Used by

Dependency tree · two levels

60 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