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.

Lck/Json/Parser.lean で SortedKVs.ofListWithPolicy、hasDuplicateKeysList、ofList、ofListLastWins を読んで始めます。次に、Syntax.lean にある既存の構造と、Proofs.lean にある関連する証明を調べます。rejectDuplicates、firstWins、lastWins に対して1回の mergeSort パスを可能にする fromSortedList ヘルパーが追加され、対応する証明と O(n log n) の動作が維持されれば完了です。