Bistro Research
mathematics
archive · read-only

Conjugate locus on SE(2)

Where rotating sub-Riemannian geodesics stop being optimal, with the counting theorems checked by the Lean kernel.

Maintained by Igor Moiseev

Articles

Research graph

5 experiments · 2 tracks
first causticglobal countexperiment order, earliest on the left →
confirmedpartialrefutedpendingfinding motivated a later hypothesislater experiment controlled an earlier caveatlater experiment superseded an earlier oneEach dot is one experiment, coloured by its finding's verdict; click one to open it.

Findings

Latest 5

Claims

Each one re-executes on demand
  • CrossingData.crossing · lean

    For every phase ψ there is exactly one parameter p in [lo, hi] and one branch σ = ±1 whose value equals ψ modulo the period 2K.

  • JacobiFull.exact_first_time · lean

    For every phase ψ there is exactly one p in [p₀, p₁] with J₂(ψ + p, p) = 0.

    Passed· 18.0s · 1 d agoaxioms: propext, Classical.choice, Quot.sound
  • JacobiFull.first_time_complete · lean

    For every phase there is exactly one conjugate time in (0, p₁], and it lies in [p₀, p₁].

    Passed· 24.5s · 15 h agoaxioms: propext, Classical.choice, Quot.sound
  • JacobiFull.roots_ncard · lean

    Away from K = 2E, every phase has exactly 2N conjugate times before the end of the N-th Maxwell cell: two per cell, none before the first.

  • JacobiConcrete.first_time_unique · lean

    For the concrete Jacobi elliptic data with modulus 0 < k < 1, the first conjugate time is unique for every phase.