Theorem 3.4 — uniqueness of the first conjugate time

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

For every phase ψ there is exactly one p in [p₀, p₁] with J₂(ψ + p, p) = 0. Prediction: Lean accepts JacobiFull.exact_first_time using only the standard axioms (no sorry).

Formalised in Lean 4 + Mathlib; #print axioms JacobiFull.exact_first_time after lake build.

Kernel-checked: JacobiFull.exact_first_time compiles and depends only on propext, Classical.choice and Quot.sound.

Stated for the abstract JacobiFull structure, which assumes finitely many tangencies.

• JacobiFull.exact_first_time

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

  Re-verifyPassed· 18.0s · 1 d agoaxioms: propext, Classical.choice, Quot.sound