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.

Start in Lck/Json/Parser.lean by reading SortedKVs.ofListWithPolicy, hasDuplicateKeysList, ofList, and ofListLastWins. Then inspect the existing structure in Syntax.lean and related proofs in Proofs.lean. Done means a fromSortedList helper enables one mergeSort pass for rejectDuplicates, firstWins, and lastWins while preserving the corresponding proofs and O(n log n) behavior.