Theorem 3.4 (complete) — nothing earlier

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

For every phase there is exactly one conjugate time in (0, p₁], and it lies in [p₀, p₁]. Prediction: Lean accepts JacobiFull.first_time_complete using only the standard axioms (no sorry).

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

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

Same hypotheses as Theorem 3.4.

• JacobiFull.first_time_complete

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

  Re-verifyPassed· 24.5s · 16 h agoaxioms: propext, Classical.choice, Quot.sound