ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (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.

Oppositely signed intersections of two three-manifolds in a simply connected six-manifold

Example

In $S^{6}$ let $A = S^{3} \subset S^{6}$ be a standard linear $3$ -sphere and let $B$ be a $3$ -sphere obtained from a standard $3$ -sphere disjoint from $A$ by a finger move that pushes a small $3$ -ball across $A$ ; the move creates exactly two transverse intersection points $p, q$ with opposite local signs, so $A \cap B = {p, q}$ and $I (A, B) = I (p) + I (q) = 0$ . Here $m = 6$ , $a = b = 3$ , and $a = b = m - 3 = 3,$ so the clean-disk general-position lemma applies at its boundary, and $S^{6}$ is simply connected, so every Whitney circle is null-homotopic; the high-dimensional Whitney trick then isotopes $A$ to an embedded $3$ -sphere $A^{'}$ with $A^{'} \cap B = \emptyset$ . The example thus verifies the dimension range $a, b \leq m - 3$ in the first non-trivial case and exhibits the cancellation of a single opposite-sign pair in a simply connected ambient manifold.

Facts & Assumptions

[F1]

Smooth embeddings. Smooth embeddings

[F2]

The local sign compares the ordered tangent spaces of the two sheets with the ambient orientation. The local oriented intersection sign

[F3]

The oriented intersection number. The oriented intersection number

[F4]

$S^{n}$ is simply connected for every $n \geq 2$ . $S^{n}$ is simply connected for every $n \geq 2$

[F5]

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

Verification

Given: Countable choice and $S^{6}$ as the one-point compactification of $R^{6}$ with coordinates $(e_{1}, e_{2}, e_{3}, y_{1}, y_{2}, y_{3})$ .

1.1givenconstructF1

Take $A$ to be the compactification of the plane $y = 0$ , a standard linear $S^{3}$ . Start with a small round $3$ -sphere $B_{0}$ in the affine $4$ -plane $e_{2} = e_{3} = 0$ , centred far enough in the positive $y_{3}$ direction to miss $A$ . Near its lowest point it is a graph $y_{3} = h_{0} (e_{1}, y_{1}, y_{2}) > 0$ over a small $3$ -ball. Replace only a smaller graph cap by $y_{3} = h_{1} (e_{1}, y_{1}, y_{2})$ , where $h_{1} = e_{1}^{2} + y_{1}^{2} + y_{2}^{2} - ρ^{2}$ on a small inner ball and is positive outside it, agreeing with $h_{0}$ near the outer cap boundary. Such a smooth radial interpolation can be chosen positive whenever $e_{1}^{2} + y_{1}^{2} + y_{2}^{2} > ρ^{2}$ , by choosing $ρ$ sufficiently small. The linear interpolation from $h_{0}$ to $h_{1}$ gives embedded graph caps throughout and fixes the outer collar; it is a local finger move of this $3$ -ball. The resulting $B$ is an embedded $S^{3}$ .

2.1step 1.1constructalgebraF2F3

An intersection with $A$ forces $y_{1} = y_{2} = y_{3} = 0$ . On the changed cap it therefore forces $e_{1}^{2} = ρ^{2}$ , giving exactly $p = (ρ, 0, 0, 0, 0, 0)$ and $q = (- ρ, 0, 0, 0, 0, 0)$ . Outside the changed cap $y_{3} > 0$ wherever $y_{1} = y_{2} = 0$ , so there are no other intersections. At either point the tangent directions of $B$ are $\partial_{e_{1}} + 2 e_{1} \partial_{y_{3}}, \partial_{y_{1}}, \partial_{y_{2}}$ . Together with $T A = span (\partial_{e_{1}}, \partial_{e_{2}}, \partial_{e_{3}})$ they span the six-dimensional ambient space; their determinant differs at the two points only by the sign of $2 e_{1}$ . Thus the local signs are opposite and $I (A, B) = 0$ .

3.1step 2.1constructF4F5∎

Here $a = b = 3 = m - 3$ , so the stable dimension inequalities are met at equality. The sphere $S^{6}$ is simply connected by the published sphere theorem, and the two connected sheets admit the required avoiding arcs. The high-dimensional Whitney trick therefore removes exactly this pair, producing an embedded $A^{'}$ disjoint from $B$ . The explicit cap verifies the claimed finger-move witness, rather than presupposing its intersection count.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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)
John Milnor, Lectures on the h-Cobordism Theorem (notes by L. Siebenmann and J. Sondow, Princeton University Press 1965; scanned edition with searchable text layer) (standard reference, not scraped)