Alphabeta MathHow 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.
Movie-move equivalence for surface cobordisms
Statement
Assume countable choice. Let be compact smooth properly embedded oriented surfaces from fixed oriented knots to , with the same boundary parametrizations and product collars. Suppose their generic movies represent ambient isotopic cobordisms by an isotopy fixed on those collars. Then one movie can be changed to the other by a finite sequence of planar isotopies, the fifteen Carter–Saito movie moves, sweep-around moves, and interchanges of two disjoint elementary movie events (including disjoint critical points of the surface-height function). A sweep-around moves a closing arc of a one-interval tangle over the tangle to its other side and back underneath, or reverses that movie; geometrically it is a local sheet passage through the missing vertical arc in a spatial chart . Every intermediate movie represents a generic surface cobordism with the same fixed boundary data.
Statement references
Facts & Assumptions
Given: Countable choice, the two fixed-boundary generic movies and the stated ambient isotopy of their oriented traced cobordisms in .
The Axiom of Countable Choice () is used through the two geometric suppliers.
A generic movie of an oriented knot cobordism supplies traced movies, their actual orientations, parametrized boundary and product collars.
Spherical cobordism isotopies reduce to sweep-around events proves that an actual spherical comparison of two Euclidean traced cobordisms factors into finitely many Euclidean ambient isotopies and local sheet passages through the missing vertical arc, the sweep-around events.
Euclidean surface isotopies have finite movie-move decompositions proves the finite Euclidean decomposition into the fifteen types and distant interchanges, with its independent-jet, local normal-form and finiteness arguments. The local types and all orientation/height variants are The fifteen Euclidean local movie moves.
Proof
Use the actual smooth traced realizations of the two planar movies, with their prescribed endpoint realizations and collars. These lie in the standard spatial chart ; by [F1] and the hypothesis, their oriented traces have the specified spherical isotopy relative to those collars. Apply [F2]. The comparison is a finite sequence of Euclidean isotopies and isolated sweep-around events, with the same parametrized boundary. At the intermediate cuts choose generic movies fixed on the retained collars; the same finite-jet construction in [F3] applies with these cuts protected.
On each Euclidean isotopy interval, [F3] replaces its comparison by finitely many of the fifteen local moves, distant interchanges and planar isotopies. All hidden-coordinate height orders and orientations are preserved. At each missing-arc passage retain the sweep-around supplied by [F2]; it is not silently replaced by a Euclidean move. The two boundary movies of each interval match those at the adjacent pieces, because the construction fixes the chosen cuts and collars.
Concatenate these finite lists. There are finitely many intervals and passages, so the total list is finite. Every retained frame is a regular frame of a generic traced surface, and every elementary replacement has its stated oriented local trace with the same outside and boundary data. Consequently all intermediate movies have the prescribed parametrized knots and collars. The total sequence starts and ends at the given movies and proves the claimed spherical comparison.
Source and scope note
The fifteen Euclidean types are derived locally from the unframed smooth-sheet calculations in Queffelec–Walker, not from a citation standing in for a proof. Their full framed-foam theorem and its seam moves are not premises here. The spherical step uses the separately proved missing-arc incidence reduction, in accordance with the explicit distinction on p.2 of Morrison–Walker–Wedrich. The original Carter–Saito publisher text was not retrieved; no reading of that unavailable article is claimed. A homology theory must still prove its own sweep-around map identity; this geometric theorem does not establish one.
Depends on
Used by
Dependency tree · two levels
10 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
- Scott Morrison, Kevin Walker and Paul Wedrich, Invariants of 4-manifolds from Khovanov–Rozansky link homology (standard reference, not scraped)
- Hoel Queffelec and Kevin Walker, Movie moves for framed foams from multijet transversality (standard reference, not scraped)
- J. Scott Carter and Masahico Saito, Reidemeister moves for surface isotopies and their interpretations as moves to movies (standard reference, not scraped)
- Magnus Jacobsson, An invariant of link cobordisms from Khovanov homology, §4.2 (standard reference, not scraped)
- Hilary Hunt, Movie presentations of isotopies, §5.2 (standard reference, not scraped)