TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck 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.

Vanishing algebraic intersection gives geometric disjunction in the simply connected stable range

Statement

Assume ${A C}_{ω}$ . Let $X^{m}$ be a simply connected oriented smooth manifold and let $A^{a}, B^{b} \subseteq X$ be closed connected oriented embedded complementary submanifolds with $a, b \geq 3$ , meeting transversely, with at least one of $A, B$ compact. Suppose the oriented intersection number vanishes: $I (A, B) = 0$ . Then there is an isotopy of $X$ carrying $A$ to an embedded submanifold $A^{'}$ transverse to $B$ with $A^{'} \cap B = \emptyset$ . More generally, if $I (A, B) = n$ for some integer $n$ , one can isotope $A$ so that it meets $B$ in exactly $∣ n ∣$ points (with the remaining intersections removed in opposite-sign pairs); in particular any two algebraically cancelling pairs can be removed one at a time without creating new intersections. The corresponding statement with group-ring coefficients holds for a general simply connected ambient manifold by the label lemma.

Facts & Assumptions

[F1]

Compact transverse complementary intersections are finite. Compact transverse complementary intersections are finite

[F2]

The oriented intersection number. The oriented intersection number

[F3]

Two points of a closed connected embedded submanifold of dimension at least two can be joined by a smooth embedded arc avoiding a prescribed finite set away from its endpoints. Arcs joining two points of a connected submanifold avoiding finitely many points

[F4]

In the stable range an admissible opposite-sign pair with nullhomotopic Whitney circle can be removed, leaving every other intersection fixed. The high-dimensional Whitney trick

Proof

Given: Countable choice, simply connected $X$ , closed connected oriented complementary transverse sheets of dimensions at least three, and their signed intersection number $n$ .

1.1givenconstructalgebraF1F2F3

Complementary transversality makes the intersection set discrete. Since one sheet is compact and the other is closed, [F1] makes it finite. If there are $P$ positive and $Q$ negative points, then $n = P - Q$ . Choose $\min (P, Q)$ disjoint pairs of opposite signs. For each pair the arcs lemma gives sheet arcs avoiding every other intersection, and their circle contracts because $X$ is simply connected.

2.1step 1.1constructalgebraF4∎

Apply the high-dimensional Whitney trick to one pair at a time. It fixes the other intersection germs, creates no new points, and preserves embeddedness and connectedness of the moved sheet. The next pair therefore has the same signs and can be treated in the same way. After finitely many steps exactly $∣ P - Q ∣ = ∣ n ∣$ points remain, all of one sign. Reparametrize the finitely many isotopies to be stationary near their endpoints and concatenate them smoothly. In particular $n = 0$ gives disjunction. In the simply connected case all group labels are the identity, so its group-ring formulation has exactly this signed-pair computation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

91 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

Andrew Ranicki, Algebraic and Geometric Surgery (Oxford Mathematical Monographs, Oxford University Press 2002; complete electronic copy) (standard reference, not scraped)
Wolfgang Lück, A Basic Introduction to Surgery Theory (complete lecture notes, ICTP/Münster) (standard reference, not scraped)