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.

Regular constraint directions are realised by level-set curves

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $X$ be a real Banach space, $U \subseteq X$ open, $G : U \to R^{m}$ of class $C^{1}$ (C k map between Banach spaces, Fréchet derivative between Banach spaces), $u \in U$ , and suppose $D G (u)$ is surjective, with $Y$ , $A \subseteq \ker D G (u)$ , $B \subseteq Y$ and $φ : A \to B$ as in A split surjective derivative parametrises its level set. Then for every $h \in \ker D G (u)$ there are $ε > 0$ and a $C^{1}$ curve $c : (- ε, ε) \to X$ with $c (0) = u$ , $c^{'} (0) = h$ and $G (c (t)) = G (u)$ for every $t \in (- ε, ε)$ ; explicitly $c (t) = u + t h + φ (t h)$ .

Facts & Assumptions

Given: The setting of A split surjective derivative parametrises its level set: a split surjective derivative $D G (u)$ at $u \in U$ , and the open sets $A \subseteq \ker D G (u)$ with $0 \in A$ and the $C^{1}$ map $φ : A \to B$ with $φ (0) = 0$ , $D φ (0) = 0$ of that theorem.

[F1]

A split surjective derivative parametrises its level set: $\ker D G (u)$ is a closed subspace of $X$ , and the level set is parametrised as ${z \in u + (A + B) : G (z) = G (u)} = {u + a + φ (a) : a \in A}$ with $A$ open, $0 \in A$ , and $φ$ of class $C^{1}$ with $φ (0) = 0$ and $D φ (0) = 0$ .

[F2]

C k map between Banach spaces, Chain sum product and composition rules for Banach derivatives: sums and scalar multiples of $C^{1}$ maps are $C^{1}$ with the sum rule for derivatives, the derivative of a bounded linear map is the map itself, and composites of $C^{1}$ maps are $C^{1}$ with the chain rule; in particular $t \mapsto t h$ and $a \mapsto u + a + φ (a)$ are $C^{1}$ .

[A1]

The Axiom of Choice: the hypothesis under which the parametrisation of [F1] is available.

Proof

technique · direct

Given: The setting of [F1] and a vector $h \in \ker D G (u)$ .

1.1givenA1F1algebra

Since $A$ is open and $0 \in A$ there is $r > 0$ with $B (0, r) \subseteq A$ ; if $h \neq 0$ , set $ε : = r / (2 ∥ h ∥)$ , and if $h = 0$ take $ε : = 1$ . For $∣ t ∣ < ε$ one has $∥ t h ∥ < r$ , so $t h \in A$ , and $c (t) : = u + t h + φ (t h)$ is a well-defined element of $u + (A + B) \subseteq U$ with $G (c (t)) = G (u)$ by the parametrisation identity of [F1]; moreover $c (0) = u + 0 + φ (0) = u$ .

2.1step 1.1F1F2

The curve $c$ is $C^{1}$ on $(- ε, ε)$ and $c^{'} (t) = h + D φ (t h) h$ for every $t$ , by the sum and chain rules applied to $t \mapsto t h$ and $φ$ [F2]; at $t = 0$ this gives $c^{'} (0) = h + D φ (0) h = h$ because $D φ (0) = 0$ [F1].

2.2step 1.1

In particular $c$ is a $C^{1}$ curve on $(- ε, ε)$ with values in $X$ , $c (0) = u$ , and $G (c (t)) = G (u)$ for every $t$ by step 1.1, which is the asserted realisation of $h$ by a level-set curve.

3.1step 2.1step 2.2A1∎

Steps 1.1, 2.1 and 2.2 prove the claim for an arbitrary $h \in \ker D G (u)$ ; no convexity of the constraint was used, and the Axiom of Choice enters only through the parametrisation supplied by [F1] [A1].

Depends on

Used by

The tangent space of a regular level set is the kernel of the constraint derivative Lemma

Dependency tree · two levels

32 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

Thomas C. Sideris, Ordinary Differential Equations and Dynamical Systems (complete author-hosted book text) (standard reference, not scraped)