Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-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.

Critical levels connected by a trajectory cannot always be interchanged

Statement refuted

The disjointness hypothesis in the critical-value interchange lemma can be dropped: whenever two critical levels are joined by a trajectory, their values can always be interchanged while keeping the same gradient-like field.

Facts & Assumptions

[F1]

Critical values of disjoint trajectory closures can be interchanged permits arbitrary assignments of the two cluster values inside a regular-endpoint band containing just those clusters, with the same field, under the no-connecting-trajectory hypothesis.

[F2]

Downward gradient-like vector fields for a Morse function: A smooth field X is downward gradient-like for a Morse function h when dhx(Xx)<0 at every x∉Crit⁡(h) and X has the model form (2u,−2v) in Morse coordinates at every critical point.

[F3]

A Morse trajectory from one critical point to another: For critical points p,q of a Morse function, a Morse trajectory from p to q is a nonconstant full trajectory of −grad⁡gf with past limit p and future limit q.

[F4]

Nonconstant negative-gradient trajectories strictly decrease the function: Along a nonconstant negative-gradient trajectory, (f∘γ)′(t)<0 for every t.

[F5]

Morse function adapted to a cobordism: An adapted pair on a triad consists of an adapted Morse function and a complete downward gradient-like field; excellence is not required for this item.

[A1]

Put f(θ)=(2+cos⁡θ)/4 on the circle. Choose a positive smooth function a equal to 4/(1+cos⁡θ) near p=0, to 4/(1−cos⁡θ) near q=π, and patched to one away from these two disjoint neighbourhoods by scalar cutoffs. Set X=a(θ)sin⁡θ ∂θ. The metric dθ2/(4a(θ)) makes X=−grad⁡f.

Counterexample

Given: The circle with f,X of [A1], with its closed-triad faces empty.

1.1F2F5A1algebra

Its only critical points are p,q, with values 3/4,1/4 and indices 1,0. Near p take the Morse coordinate u=sin⁡(θ/2)/2, so f=3/4−u2 and Xu=2u; near q take v=sin⁡((θ−π)/2)/2, so f=1/4+v2 and Xv=−2v. Elsewhere df(X)=−asin⁡2θ/4<0. Thus this is an exact downward gradient-like field, rather than merely a descending round-metric gradient.

2.1F3A1step 1.1algebra

On each of the two open arcs the field is nonzero and points from p to q. Its solutions are full trajectories: near either endpoint the smooth field has a simple linear zero with slope ±2, so reaching it requires infinite time (equivalently the separated time integral has logarithmic divergence). Consequently each arc has past limit p and future limit q.

3.1F1F2F4step 2.1algebra

If X is downward gradient-like for a new function g with these same critical points, then g is strictly decreasing on either arc trajectory. For finite t1<t2, continuity at the endpoints gives g(p)≥g(γ(t1))>g(γ(t2))≥g(q); hence g(p)>g(q). Reversing their values while retaining X is impossible. This refutes the stated universal interchange without the no-connection hypothesis.

4.1step 1.1step 3.1algebra∎

The lower point has index zero and the upper point index one, so the separation hypothesis requiring lower index at least upper index is absent here. Perturbation cannot be promised for every connecting pair; the index hypothesis is exactly what licenses it in the rearrangement argument. The counterexample establishes the fixed-field obstruction independently of such a perturbation.

Depends on

Used by

Nothing in the library uses this result yet.

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