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.

One-sided trivial-holonomy classes form a normal subgroup

Statement

Assume Countable Choice ACω. Let F be a transversely oriented codimension-one foliation, L a leaf, x∈L, and j one of its two sides. The classes in π1(L,x) whose one-sided holonomy germ is the identity form a normal subgroup Nj(L,x)◃π1(L,x). Consequently the quotient Pj(L,x)=π1(L,x)/Nj(L,x) used to define ordinary one-sided limit cycles is a group.

Facts & Assumptions

Given: A transversely oriented codimension-one foliation F, a leaf L, a base point x∈L, one side j of L, and the standing countable choice assumption.

Proof

technique · direct
1.1given

By the definition of the holonomy representation, each class in π1(L,x) is assigned the germ of the return map along its reversed representative, on the chosen side (the library homomorphism convention), and the transverse orientation makes these germs side-preserving, so the assignment is a group homomorphism from π1(L,x) to the group of side-preserving germs of local diffeomorphisms of a half-transversal of the given side (The holonomy representation and the holonomy group of a leaf, Germs of local diffeomorphisms at a point).

2.1step 1.1∎

The classes in π1(L,x) whose one-sided holonomy germ is the identity are exactly the kernel of that homomorphism; the kernel of a group homomorphism is a normal subgroup, so the indicated classes form Nj(L,x)◃π1(L,x), and the quotient Pj(L,x)=π1(L,x)/Nj(L,x) used to define ordinary one-sided limit cycles is a group; no choice principle beyond the standing assumption is used.

Depends on

Used by

Dependency tree · two levels

23 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