LemmaStatement: Literature-sourcedProof: 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.

Increasing reparametrization of finitely many critical levels

Statement

Assume ${A C}_{ω}$ . Let $0 < c_{0} < \dots < c_{m} < 1$ and $0 < d_{0} < \dots < d_{m} < 1$ . There is a smooth diffeomorphism $ϕ : [0, 1] \to [0, 1]$ with $ϕ^{'} > 0$ , equal to the identity near both endpoints, and $ϕ (c_{j}) = d_{j}$ for every $j$ . It may additionally be chosen to have derivative one near every $c_{j}$ ; there it is translation by $d_{j} - c_{j}$ .

Facts & Assumptions

[F1]

A Euclidean bump for a compact set inside an open set gives nonnegative smooth bumps supported inside an open interval, positive on a smaller closed interval.

Proof

Given: The two strictly increasing finite sequences.

1.1F1givenconstruct

Adjoin nodes $c_{- 1} = d_{- 1} = 0$ and $c_{m + 1} = d_{m + 1} = 1$ . Choose small disjoint neighbourhoods of all source nodes. Construct a positive smooth function $q$ equal to one on smaller node neighbourhoods and equal to a small constant $η > 0$ off the chosen neighbourhoods, interpolating by scalar cutoffs from [F1]. The neighbourhoods and $η$ may be chosen so small that for every $j = - 1, \dots, m$ , $I_{j} : = \int_{c_{j}}^{c_{j + 1}} q (s) d s < d_{j + 1} - d_{j}$ : there are finitely many positive target gaps, and the integrals are bounded by the total lengths of the node neighbourhoods plus $η$ .

2.1F1step 1.1constructalgebra

In each $(c_{j}, c_{j + 1})$ choose a nonnegative smooth bump $b_{j}$ supported away from the node neighbourhoods and with integral one, by normalizing a bump positive on a smaller interval. Set $r = q + \sum_{j = - 1}^{m} (d_{j + 1} - d_{j} - I_{j}) b_{j}$ and $ϕ (x) = \int_{0}^{x} r (s) d s$ . Then $r > 0$ , $r = 1$ near every node, and its integral over each source interval is exactly its target gap. Summing these identities gives $ϕ (c_{j}) = d_{j}$ , $ϕ (0) = 0$ and $ϕ (1) = 1$ .

3.1step 2.1algebra∎

Thus $ϕ^{'} > 0$ and $ϕ$ is a bijection of the closed interval; the inverse is smooth by the one-variable inverse function theorem, including at endpoints by the identity there. Near each node its derivative is one, hence it is translation by $d_{j} - c_{j}$ . All selections were finite and the construction uses no choice principle. The empty list uses the identity.

Depends on

Used by

Dependency tree · two levels

25 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

Andrei Pajitnov, Circle-Valued Morse Theory (de Gruyter Studies in Mathematics 32), Chapter 5 Sections 1-3 (pp. 163-189) and Chapter 4 Section 3 (pp. 132-162) (standard reference, not scraped)