Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)
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.

Essential torus curves with the same primitive class are isotopic

Statement

Let T=R2/Z2 be oriented by dx∧dy, and identify H1(T;Z) with Z2 in the standard basis, so the algebraic intersection of classes v,w is det⁡(v,w). Let γ0,γ1⊂T be smooth embedded circles that are not null-homotopic. Orient them so that their homology classes agree, and suppose their common class v∈H1(T;Z) is primitive, meaning it is not an integer multiple mu with ∣m∣>1. Then γ0 and γ1 are isotopic through embedded circles in T.

Facts & Assumptions

Given: The torus and two oriented essential smooth embedded circles with common primitive class v.

Proof

1.1givenalgebraconstruct

Since v is primitive, Bezout's identity gives w∈H1(T;Z) with det⁡(v,w)=1. The linear torus diffeomorphism taking the basis (v,w) to the standard basis takes both curves to curves of class (1,0). It is enough to prove the claim for that class.

2.1givenstep 1.1constructalgebra

Put the two curves in transverse position. If they intersect, lift them to the annular cover A=R2/⟨(1,0)⟩. Each lift is an essential embedded circle, and the deck translates of each one are disjoint. In the universal cover of A, a lift of either circle is a proper line invariant under horizontal unit translation and contained in a bounded horizontal strip; all such lines have the same two ends. The signed intersection sum in a fundamental period is zero because both curves have class (1,0). Thus intersections have both signs. Two successive intersections of opposite sign cut off a bounded region between subarcs of the two lines. Choose among such regions one with the least number of interior intersections and, among those, least horizontal width modulo deck translation. If a lifted arc entered the region, its first entry and exit would cut off a region with fewer interior intersections; if a nontrivial deck translate met it, the overlap would yield a region of smaller horizontal width. Hence its interior is disjoint from all lifted arcs and translates, and its projection is an embedded bigon in T. Isotoping one arc across the bigon removes two intersections and creates none. Compactness and transversality give finitely many intersections, so finitely many such isotopies make the curves disjoint.

3.1givenstep 1.1step 2.1algebra∎

The disjoint curves still have primitive class (1,0), so neither bounds a disk. Cutting the torus along the second curve gives a connected orientable surface with two boundary circles and Euler characteristic zero, hence an annulus. The first curve remains essential in that annulus. Cutting the annulus along it gives two annuli, so it is parallel to the second curve and isotopic to it. Composing this isotopy with the finite bigon-removal isotopies in step 2.1 proves the assertion for the original pair; undoing the linear diffeomorphism proves it for v.

Used by

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources