This note describes how to leverage bifurcation results in the KeYmaera X theorem prover. The Saddle-node bifurcation is a canonical bifurcation in a continuous dynamical system. The simplest example of a Saddle-node bifurcation is a one dimensional system with one parameter r; as this parameter varies, the system’s equilibrium point changes.

This note will describe how to write a computer-checked proof (using the KeYmaera X prover) that the system x' = r + x^2 has at least one equilibrium point for every non-positive choice of r. Explore the full proof in our web UI for KeYmaera X on web.keymaerax.org, or download the source code from KeYmaera X projects repository. If you’re unfamiliar with KeYmaera X, you may want to work through the Learner’s Mode tutorial by creating a new account on web.keymaerax.org before continuing.

The System

In KeYmaera X, we can express the one dimensional saddle node as a simple reachability property:

r <= 0 -> \exists f (x=f -> [{x' = r + x^2}]x=f)

This property states that for every r <= 0, there is a fixed point of the system x' = r + x^2. I.e., for every non-positive choice of r, there an initial value x_0 = f such that along every flow of the ODE x' = r + x^2, x=f is always true. More concisely, for every non-positive choice of the parameter r there exists an equilibrium point f of x' = r + x^2.

As we vary the parameter r, the equilibrium point of this system will change.

  • At r<0, there is an equilibrium point at f = -\sqrt(-r).
  • At r=0, there is an equilibrium point at f = 0.

The Proof

We cannot prove this property for a single choice of r; the value of f will be different when r<0 than when r=0. Therefore, any proof that begins by instantiating the existential \exists f will fail! Instead, the proof needs to split into two cases at the bifurcation point.

I do this by introducing a lemma r<0 | r=0 and then splitting the proof along this disjunction. First, we cut in the disjunction lemma and prove it follows from our existing assumption that r <= 0.

        *
QE --------------------       ---------------------------------------------------------
   r<=0 |- ..., r<0|r=0       r<=0, r<0|r=0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)
--------------------------------------------------------------------------------------- cut({`r<0 | r=0`})
                          r <= 0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)

On the right branch, the proof now decomposes along the bifurcation point by splitting the disjunction:

r<0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)     r<0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)
----------------------------------------------------------------------------------------------- orL(-1)
              r<0|r=0       |- \exists f (x=f -> [{x' = r + x^2}]x=f)
----------------------------------------------------------------------------------------------- hideL(-1)
              r<=0, r<0|r=0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)

We choose the appropriate instantiation of f for each value of r.

The right subgoal is easiest:

     *
--------------------------------------------- implyR(1); ODE
r<0 |- x=0 -> [{x' = r + x^2}]x=0
--------------------------------------------- existsR({`0`}, 1)
r<0 |- \exists f (x=f -> [{x' = r + x^2}]x=f)

Proving that x=0 is an equilibrium point when r<0 is a job for differential ghosts; fortunately, the ODE tactic already automates this proof. If you’re curious about how to do this proof by hand, see my note on differential ghosts.

For the r<0 case we have to do a bit more work in order to express the quantity -\sqrt(-r) in KeYmaera X. Introduce a value s = \sqrt(-r) via an arithmetic ghost and then phrase the equilibrium point in terms of this new value s.

                      *
--------------------------------------------------------------- implyR(1); ODE
r<0, r=-s*s           |- x=-s -> [{x' = r + x^2}]x=-s
--------------------------------------------------------------- existsR({`-s`}, 1)
r<0, r=-s*s           |- \exists f (x=f -> [{x' = r + x^2}]x=f)
--------------------------------------------------------------- existsL(-2)
r<0, \exists s r=-s*s |- \exists f (x=f -> [{x' = r + x^2}]x=f)
--------------------------------------------------------------- cut({`\exists s r=-s*s`})
r<0                   |- \exists f (x=f -> [{x' = r + x^2}]x=f)

The “cut show” branch just involves hiding everything except the valid cut \exists s r=-s*s.

The by-hand proof for this equilibrium point is slightly more difficult than those covered in my note on differential ghosts. Here’s the answer, which you can verify using the process outlined in my note on ghosts:

dG({`{y'=(-(x-s))*y}`}, {`y*(x+s)=0&y>0`}, 1); 
existsR({`1`}, 1); 
boxAnd(1) ; andR(1) <(
  dI(1)
  ,
  dG({`{z'=(x-s)/2*z}`}, {`z^2*y=1`}, 1);
  existsR({`1`}, 1); 
  dI(1)
)

Conclusion

Most bifurcation results are very simple to leverage in KeYmaera X:

  • Cut in a disjunction that describes the bifurcation; each “side” of the bifurcation should be a separate term in the disjunction.
  • Split the proof into sub-cases by splitting the disjunction.
  • Prove each sub-case separately. This step is the most difficult, but we’re working on providing more and more ODE prover automation.

Appendix: The whole proof

I’ve avoided using ODE tactic in this proof to demonstrate how the entire differential ghost argument works:

/* Move r <= 0 to the antecedent */
implyR(1); 
/* Introduce and prove r=0|r<0; hide assumption that r<=0 */
cut({`r=0|r < 0`}) <(hideL(-1), hideR(1) ; QE); 
/* Split the proof. */
orL(-1) <(
 
  /* CASE 1: r=0 */
  existsR({`0`}, 1);                    /* choose f=0 */
  implyR(1); 
  dG({`{y'=-x*y}`}, {`y*x=0&y>0`}, 1);  /* x=0 <-> \exists y (y*x=0&y>0) */
  existsR({`1`}, 1);                    /* choose arbitrarily y != 0; e.g. y=1 */
  /* Consider y*x=0 and y>0 differential invariants separately */
  boxAnd(1); andR(1) <(
    /* y*x=0 is differentially inductive because:
       (yx)'=0 <-> y'x + x'y = 0 <-> -x*y^2 + r + x^2 = 0
       (recall: r=0)
    */
    dI(1)
    ,
    /* y>0 case needs an extra cut. See note on differential ghosts. */
    dG({`{z'=x/2*z}`}, {`z^2*y=1`}, 1); 
    existsR({`1`}, 1); 
    dI(1)
  )

  ,

  /* CASE 2: r<0 */
  /* introduce new variable s = sqrt(-r) and prove s exists. */
  cut({`\exists s r=-s*s`}) <(nil, hideR(1) ; QE);
  /* Some cleanup work about s */
  existsL(-2) ; existsR({`-s`}, 1) ; implyR(1) ; 
  /* See not on differential ghosts. */
  dG({`{y'=(-(x-s))*y}`}, {`y*(x+s)=0&y>0`}, 1) ; existsR({`1`}, 1) ; 
  boxAnd(1) ; andR(1) <(
    dI(1),
    dG({`{z'=(x-s)/2*z}`}, {`z^2*y=1`}, 1) ; existsR({`1`}, 1) ; dI(1)
  )
)