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.

Empieza en Lck/Json/Parser.lean leyendo SortedKVs.ofListWithPolicy, hasDuplicateKeysList, ofList y ofListLastWins. Después, inspecciona la estructura existente en Syntax.lean y las pruebas relacionadas en Proofs.lean. El trabajo estará terminado cuando un helper fromSortedList permita una sola pasada de mergeSort para rejectDuplicates, firstWins y lastWins, preservando las pruebas correspondientes y el comportamiento O(n log n).