Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

Local morse sublevel pair is a handle pair

Statement

Assume ACω. In a sufficiently small Morse chart f=c−∣u∣2+∣v∣2, with u∈Rk and v∈Rn−k, the change across c is a rounded index-k handle: a compact product piece attaches along Sk−1×Dn−k on f=c−ε, its core is v=0, and after a local modification the remaining region up to c+ε is a regular collar. The modification agrees with f off a compact subset of the chart. The collar assertion is made inside a compact band having no other critical point.

Facts & Assumptions

[F1]

K handle core cocore attaching region and belt sphere: For integers 0≤k≤n, the standard n-dimensional k-handle is Dk×Dn−k. Its core is Dk×{0}, its cocore is {0}×Dn−k, its attaching region is Sk−1×Dn−k, and its attaching sphere is Sk−1×{0}. The outgoing region is Dk×Sn−k−1 and the belt sphere is {0}×Sn−k−1. Here Dj is the closed unit disk, D0 is a point, and S−1=∅. For n=0 both boundary regions are empty.

[F2]

Smooth handle attachment is independent of corner rounding up to diffeomorphism: For fixed attaching and product-collar data, two compatible smooth monotone roundings of a handle attachment are diffeomorphic by an isotopy supported in that collar. The diffeomorphism is the identity outside the collar.

[F3]

Morse lemma: Let f:M→R be smooth, let p be a nondegenerate critical point of f, and let λ be the index of p. If n=dim⁡M, then there are local coordinates (x1,…,xn) centered at p in which f=f(p)−∑i=1λ(xi)2+∑i=λ+1n(xi)2. For n=0, both sums are empty.

[F4]

Regular interval diffeomorphism: Assume ACω. If a<b and the closed band K=f−1([a,b]) of a smooth function on a boundaryless manifold is compact and critical-point-free, its normalized flow gives a level-preserving diffeomorphism T:Ma×[a,b]→K, T(x,t)=Φt−a(x).

[F5]

Local critical-value lowering preserves the upper sublevel: Assume ACω. In a Morse chart f=c−∣u∣2+∣v∣2 containing the closed ball ∣u∣2+∣v∣2≤2ε, choose a smooth μ:[0,∞)→[0,∞) supported in [0,2ε) with μ(0)>ε and −1<μ′≤0. Set F=f−μ(∣u∣2+2∣v∣2) in the chart and F=f outside. This is smooth, has the same critical points as f, lowers p below c−ε, and satisfies {F≤c+ε}={f≤c+ε}. If f−1([c−ε,c+ε]) is compact with only the critical point p, the corresponding closed band of F is compact and regular.

[F6]

The fundamental theorem on flows: Let X be a smooth vector field on M. For each p∈M, let γp:Ip→M be the maximal integral curve through p, and set D:={(t,p)∈R×M:t∈Ip},Φ(t,p):=γp(t). Then D is open in R×M, each fibre Dp is an interval containing 0, the map Φ:D→M is smooth, and Φ is the unique maximal local flow generated by X.

[F7]

A manifold bump for a compact set inside an open set: Let M be a smooth manifold, let K⊆M be compact, and let W⊆M be open with K⊆W. Then there exists a smooth function ρ:M→[0,1] that equals 1 on an open neighbourhood of K and satisfies supp⁡(ρ)⊆W.

Proof

Given: The objects and hypotheses in the statement.

1.1F3F5

Use the Morse chart and choose ε small enough that the ball of squared radius 6ε is contained in it. Apply the lowering construction, put x=∣u∣2, y=∣v∣2, and subtract c from both functions. Thus F=−x+y−μ(x+2y). Put r=sup⁡{t:μ(t)>0}<2ε. Since μ(0)>ε and μ′>−1, r>ε.

2.1F1step 1.1algebra

First let 0<k<n. For each x≥0 the equation −x+s−μ(x+2s)=−ε has a unique positive solution s=s(x): its left side is strictly increasing in s, is below −ε at zero because x+μ(x)≥μ(0)>ε, and tends to infinity. Its derivative in s is 1−2μ′>0, so s is smooth and s′=(1+μ′)/(1−2μ′)>0. Also s(x)≥x−ε, with equality for x≥r (in fact it holds earlier). Choose d>0 with d<s(0) and ε+3d<r. The compact region H0={y≤d, x≤ε+y} is parametrized by (U,V)↦(ε+d∣V∣2 U,d V) on Dk×Dn−k. Its inverse is (u,v)↦(u/ε+∣v∣2,v/d). These formulas are smooth on the axes. Its attaching face is ∣U∣=1, on f=−ε, and its core is v=0.

3.1F2step 2.1

The union of the lower sublevel with H0 has local boundary y=max⁡(d,x−ε). Round this single corner by a smooth nondecreasing function j(x) equal to that maximum off a small neighborhood of x=ε+d. Choose the rounding above the maximum and below s(x); the strict gap at the corner permits this, for example by smoothing the absolute-value formula for the maximum on a sufficiently short interval. Then j>0 and j=s=x−ε for x≥r. This is precisely the compatible rounding of the attached product handle.

4.1F6F7step 3.1algebra

The graphs y=jt(x)=(1−t)j(x)+ts(x) stay strictly positive. Near them use the smooth field Vt=(s(x)−j(x))v/(2jt(x)) in the v coordinates and zero in the u coordinates. Then dy(Vt)=s−j on the graph. Multiply this field by a bump that is one on the moving graphs where they differ and zero near v=0 and outside the chart. The graph difference has compact support in x, and all these graph points lie in the chosen chart. Integrate ∂t+Vt with this cutoff on time times the chart. Smooth dependence and uniqueness give inverse evolution; compact spatial support gives continuation throughout 0≤t≤1. Since dy/dt=s−j on the moving graph, this isotopy carries {y≤j(x)} onto {y≤s(x)}, is identity away from the chart, and fixes the core. Hence the rounded attachment is diffeomorphic to {F≤−ε}. This uses positive smooth radii, never an inverse of a flat cutoff at its endpoint.

5.1F4F5step 4.1

The lowering lemma gives {F≤ε}={f≤ε} and a compact regular F-band from −ε to ε. Its product description supplies the complementary collar. An extra finite collar does not change the diffeomorphism type: join it to an inner collar and reparametrize the collar interval by a smooth increasing map fixed near its inner end. Thus the smooth handle change reaches the upper sublevel.

6.1F1F5step 5.1algebra∎

For k=0<n, the lower local sublevel is empty and {F≤−ε} is the disk ∣v∣2≤s(0), so it is a disjoint zero-handle; the same regular collar finishes. For k=n>0, there is no v variable: x+μ(x)>ε for every x≥0, so the missing disk x≤ε is filled along its whole sphere; outside that disk the lower sublevel was already present locally. For n=0, the chart is a single point and crossing its value adds that point. These descriptions require no corner or angular coordinate.

Depends on

Used by

Dependency tree · two levels

24 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