Concrete instance for 0 < k < 1

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

For the concrete Jacobi elliptic data with modulus 0 < k < 1, the first conjugate time is unique for every phase. Prediction: Lean accepts JacobiConcrete.first_time_unique using only the standard axioms (no sorry).

Formalised in Lean 4 + Mathlib; #print axioms JacobiConcrete.first_time_unique after lake build.

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

Covers the open modulus range 0 < k < 1 only; endpoints k = 0 and k = 1 are not covered.

• JacobiConcrete.first_time_unique

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

  Re-verify