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.

Inizia in Lck/Json/Parser.lean leggendo SortedKVs.ofListWithPolicy, hasDuplicateKeysList, ofList e ofListLastWins. Poi esamina la struttura esistente in Syntax.lean e le dimostrazioni correlate in Proofs.lean. Il lavoro è completato quando un helper fromSortedList consente un solo passaggio di mergeSort per rejectDuplicates, firstWins e lastWins, preservando le dimostrazioni corrispondenti e il comportamento O(n log n).