perf: refactor rejectDuplicates in Parser.lean to avoid redundant sort and O(n²) insertion

Problem

SortedKVs.ofListWithPolicy .rejectDuplicates in Lck/Json/Parser.lean does two passes:

1. hasDuplicateKeysList: sorts the list (mergeSort, O(n log n)) then scans adjacent pairs
2. SortedKVs.ofList: builds the sorted structure via repeated insert (O(n) each → O(n²) total)

Total cost is O(n log n) + O(n²) = O(n²) with a hidden constant from sorting twice.

Suggested Fix

Add a SortedKVs.fromSortedList helper that builds the sorted structure from a pre-sorted list in O(n), then combine the duplicate check and structure construction into a single pass over the mergeSort output. This would bring the rejectDuplicates path to O(n log n) overall.

The same refactor would help firstWins and lastWins paths in ofList/ofListLastWins.

Complexity

Moderate: requires a new Syntax.lean helper and corresponding proof in Proofs.lean.

Beginne in Lck/Json/Parser.lean, indem du SortedKVs.ofListWithPolicy, hasDuplicateKeysList, ofList und ofListLastWins liest. Untersuche anschließend die bestehende Struktur in Syntax.lean und die zugehörigen Beweise in Proofs.lean. Die Aufgabe ist abgeschlossen, wenn ein fromSortedList-Helfer einen einzigen mergeSort-Durchlauf für rejectDuplicates, firstWins und lastWins ermöglicht und dabei die entsprechenden Beweise sowie das O(n log n)-Verhalten erhalten bleiben.