Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

The standard stem system cuts the punctured disk open to a disk

Statement

Assume AC. Cutting D2∖Qn open along the standard stem system s1,…,sn of Standard meridians of a punctured disk, with each puncture end completed by its slit-tip point, yields a compact connected surface H homeomorphic to the closed disk D2. Each slit has two boundary sides meeting at its puncture tip; the outer boundary is opened at d into boundary arcs. A homeomorphism of D2 fixing ∂D2, Qn, and all the stems pointwise lifts to a homeomorphism of H fixing ∂H pointwise, and conversely such a homeomorphism of H reglues to a homeomorphism of D2.

Facts & Assumptions

Given: AC, the disk and the finite standard stem system of Standard meridians of a punctured disk. Cutting includes the indicated end completion; the uncompleted cut of the punctured surface is obtained by deleting the puncture tips from H.

[F1]

A Jordan curve bounds a closed disk, with a prescribed boundary parametrization extending to a disk homeomorphism, under the stated AC (Jordan–Schönflies extension for plane curves, The Axiom of Choice).

Proof

1.1givenconstruct

A concrete model of a slit tip. Choose pairwise disjoint small round disks Bi about the punctures, meeting only their own stems. In polar coordinates about qi, put the stem radius at angle 0. The cut of Bi∖{qi} is (0,Ri]×[0,2π], not a compact annulus or disk. Adjoin its missing tip by forming Ei=([0,Ri]×[0,2π])/({0}×[0,2π]): the whole zero-radius edge is collapsed to one point. This is a closed disk (a rectangle with one edge collapsed, equivalently a triangle), whose boundary is the outer circular arc and the two radial sides joined at the tip. The map (r,θ)↦qi+reiθ extends continuously to the tip and, on identifying the two radial sides, gives the filled disk Bi. Deleting the tip before regluing gives Bi∖{qi}.

2.1F1step 1.1construct

The outer piece. Put Ω=D2∖⋃iint⁡Bi. Open it along the truncated stems from d to Ci=∂Bi, separating all sectors at their common endpoint d. To see that the result is a disk, first thicken each truncated stem to a narrow strip, with strips disjoint away from a small half-disk at d. The region left between these strips and the Bi has one polygonal Jordan boundary: tracing it visits the outer boundary once and makes one detour along both sides of each strip and around its associated hole. It is a closed disk by [F1]. Shrinking the strip widths gives the same cut topology, since each strip-side collar has a rectangular coordinate chart and changing its width is a homeomorphism. Each opened Ci is a closed boundary arc Ai; at d there are n+1 sector copies when n>0, rather than just two copies for the whole star. For n=0 the outer piece is D2.

3.1step 1.1step 2.1construct

Attaching the completed tips. Glue the circular boundary arc of Ei to Ai with matching radial-side endpoints. Gluing two disks along a proper closed boundary arc gives a disk: map the two disks to the upper and lower half-disks, with the glued arcs as their common diameter, and use these maps on the quotient. Applying this construction finitely many times to the outer disk and the Ei yields a compact disk H. Its boundary consists of the outer boundary arc and the two sides of every stem, with each pair joined at qi and with consecutive sides joined at the appropriate sector copy of d.

4.1step 3.1construct

The quotient and its topology. Identify matching points on each pair of stem sides, including the copies of d. The quotient map π:H→D2 is the ordinary coordinate map off the cuts and the polar map of step 1.1 at a tip. It is a continuous surjection whose fibers are exactly these prescribed identifications; compactness of H and the Hausdorff property of D2 show that its quotient is the filled disk D2. Removing the images qi of the added tips recovers X=D2∖Qn. Thus the compact disk assertion concerns the completed cut, with both filled and punctured quotients accounted for.

5.1givenstep 1.1step 4.1

Lifting maps. A homeomorphism f as in the statement preserves each local side of every stem: an orientation-reversing map would reverse the outer boundary, which f fixes pointwise, and an orientation-preserving map fixing an oriented stem cannot interchange its sides. Thus it lifts on the open cut surface, fixing both stem-side copies and all sector copies of d. Near a tip, continuity of f at qi implies that points with radius tending to zero have image radius tending to zero, uniformly in their angle; the collapsed-edge model therefore extends the lift continuously by fixing the tip. The same argument applies to f−1, so the lift is a boundary-fixed homeomorphism of H.

6.1step 4.1step 5.1construct∎

Regluing maps and isotopies. A boundary-fixed homeomorphism g of H respects every fiber of π and induces a homeomorphism of the filled disk, with inverse induced by g−1. It fixes the outer boundary, stems and punctures pointwise. If G:H×I→H is a boundary-fixed isotopy, the map (z,t)↦π(G(z,t)) is constant on the fibers of π×id⁡I; this map is a quotient map because its domain is compact and its target is Hausdorff. It therefore induces a continuous isotopy D2×I→D2, including at every puncture uniformly in time. This proves the asserted correspondence and the isotopy version needed by consumers.

Depends on

Used by

Dependency tree · two levels

37 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