Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)
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.

A simple fold has a unique local Lyapunov–Schmidt chart and nonzero parameter curvature

Statement

Let n≥1, let U⊆Rn×R be open, and let F:U→Rn be C3. Write DxF(x,λ)u:=DF(x,λ)(u,0) and Fλ(x,λ):=DF(x,λ)(0,1). Define Fxx(x0,λ0)[v,v]:=ddt(DxF(x0+tv,λ0)v)∣t=0. Suppose F(x0,λ0)=0,J:=DxF(x0,λ0),rank⁡J=n−1. Assume that v∈Rn is a unit vector with ker⁡J=span⁡{v}, that w∈Rn∖{0} satisfies wTJ=0, and that a:=wTFλ(x0,λ0)≠0,b:=wTFxx(x0,λ0)[v,v]≠0. Then there is δ>0 and a unique local C3 curve of solutions (x(s),λ(s)), ∣s∣<δ, with x(0)=x0,λ(0)=λ0,vT(x(s)−x0)=s,x′(0)=v,λ′(0)=0,λ′′(0)=−ba≠0. In particular, on a smaller interval there is a finite M3 such that ∣λ(s)−λ0+b2as2∣≤M36∣s∣3. The full derivative D(x,λ)F has rank n at the fold, and the solution curve tangent there is (v,0). Thus an augmented pseudo-arclength hyperplane with unit normal τ remains locally regular whenever ∣τT(v,0)∣>0. This is a local statement; it asserts no global branch completeness.

Facts & Assumptions

Given: The dimensions, U,F,(x0,λ0),J,v,w,a,b and hypotheses in the Statement.

[F1]

Complement splitting and range projection for a simple fold: with X=v⊥, Y=ker⁡(wT), q=Fλ/a, and P=I−qwT, the map P is the complement projection notation used below.

[F2]

The simple-fold complement restriction is an isomorphism: J∣X:X→Y is a linear isomorphism, P2=P, range⁡P=Y, ker⁡P=span⁡{q}, PJ=J, and PFλ=0.

[F3]

The parametrized implicit function theorem with Ck regularity: a C3 equation with invertible derivative in the solved variables has a unique local C3 implicit solution in the remaining parameters.

[F4]

The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a): derivatives of the parameterized compositions are obtained by composing their derivatives.

[F6]

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value: a continuous real-valued function on a compact metric space is bounded and attains its extrema.

[F7]

Invertibility and a norm bound for the pseudo-arclength bordered matrix: the augmented derivative with last row τT is invertible when its dot product with the unit tangent is nonzero.

[F8]

If dim⁡FV=n and U is a linear subspace of V, then U is finite-dimensional, dim⁡FU≤n, and dim⁡FU=n if and only if U=V: each finite-dimensional subspace has a finite basis, so finite-dimensional coordinates can be fixed on X and Y.

[F9]

Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T: for a linear map with finite-dimensional domain, the domain dimension is the sum of kernel and image dimensions.

[F10]

Ck Euclidean maps and diffeomorphisms: C3 means each component has continuous coordinate partial derivatives through order three.

[F11]

The total (Fréchet) derivative Df(a) as the linear first-order approximation with o(∥h∥2) remainder: DF is the linear map in the first-order approximation; state and parameter derivatives are its restrictions to the corresponding coordinate directions.

[F12]

Rank and nullity of a linear map with finite-dimensional domain: rank of a map with finite-dimensional domain is the dimension of its image.

Proof

Given: The hypotheses in the Statement.

1.1F2F3F9F10F11F12givenalgebra

Let c:=Fλ(x0,λ0). By [F2], im⁡J=Y=ker⁡(wT); and wTc=a≠0. For any r∈Rn, the vector r−(wTr/a)c lies in Y, so the columns of [J c] span Rn. Thus the full derivative has rank n. Its kernel is one-dimensional by [F9] and contains (v,0), so its unit tangent at the fold is (v,0). The local full-rank curve chart follows from [F3], as also recorded in the regular-curve lemma.

1.2F3F4F10F11givenalgebra

First take n=1. Then J=0, v∈{−1,1}, and a=wFλ≠0 implies Fλ≠0. Apply [F3] solving for λ as a function of x=x0+sv. Differentiating F(x0+sv,λ(s))=0 once gives λ′(0)=0, and differentiating twice gives Fxx[v,v]+Fλλ′′(0)=0. Since w is a nonzero scalar, this is λ′′(0)=−b/a. Local uniqueness is the uniqueness clause of [F3].

1.3F1F2F3F8F10F11givenconstruct

Now take n≥2. Fix finite-dimensional coordinates on X and Y by [F8]. Apply [F3] to the complement equation PF(x0+sv+u,λ0+μ)=0,u∈X. Its derivative in u at (0,0,0) is PJ∣X=J∣X, invertible by [F1]–[F2]. It therefore has a unique local C3 solution u=ψ(s,μ)∈X with ψ(0,0)=0.

2.1F1F2F4F10F11step 1.3algebra

Differentiating the complement equation at (0,0) and using [F1]–[F2] gives Jψs(0,0)=0 and Jψμ(0,0)=0. Both derivatives lie in X, on which J is injective, so ψs(0,0)=ψμ(0,0)=0. Define g(s,μ):=wTF(x0+sv+ψ(s,μ),λ0+μ). The identity F=PF+q(wTF) shows that F=0 is equivalent, locally, to the complement equation and g=0.

3.1F4F10F11step 2.1givenalgebra

The chain rule and wTJ=0 give g(0,0)=0,gs(0,0)=0,gμ(0,0)=a,gss(0,0)=b. For the last equality, terms involving Jψss vanish after multiplication by wT, and ψs(0,0)=0 leaves exactly wTFxx[v,v].

4.1F3F4F10F11step 2.1step 3.1algebra

Since a≠0, apply [F3] to g(s,μ)=0 to obtain a unique local C3 function μ=μ(s). Differentiating this scalar equation gives μ′(0)=−gs/gμ=0 and μ′′(0)=−gss/gμ=−b/a. The resulting x(s)=x0+sv+ψ(s,μ(s)), λ(s)=λ0+μ(s) has x′(0)=v and λ′(0)=0. The equivalence in step 2.1 proves local uniqueness among solutions.

5.1step 1.2step 1.3step 4.1

Step 1.2 gives the stated curve and derivatives when n=1; steps 1.3–4.1 give them when n≥2. In both cases x′(0)=v, λ′(0)=0, and λ′′(0)=−b/a≠0.

6.1F5F6step 1.2step 4.1step 5.1algebra

In both cases n=1 and n≥2, the branch is C3. Choose a compact subinterval [−δ,δ] and use [F6] to set M3:=sup⁡∣s∣≤δ∣λ′′′(s)∣<∞. Repeatedly applying [F5] gives the integral remainder λ(s)−λ0−λ′(0)s−12λ′′(0)s2=∫0s∫0u∫0tλ′′′(r) dr dt du, whose absolute value is at most M3∣s∣3/6.

7.1F7step 1.1step 1.2step 4.1step 5.1givenalgebra∎

The tangent (v,0) has unit length because ∥v∥2=1. Taking τ=(v,0) in [F7] gives angular factor 1, so the bordered derivative of the local pseudo-arclength corrector is invertible at the fold. More generally it remains invertible whenever ∣τT(v,0)∣>0. The local curve has therefore a regular pseudo-arclength chart through the fold, while λ′(0)=0 and λ′′(0)≠0 show that λ is not a local regular coordinate. No assertion about other components or global branch coverage follows.

Depends on

Used by

Dependency tree · two levels

85 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