nit: several low-priority polish items in JSON parser (decimal rendering, ordering invariant, docstrings)

Items

These are low-priority nits flagged by AI code review on PR #8. Grouping them into a single issue to keep the tracker clean.

1. Decimal rendering precision (cli/LckJsonFmt.lean:30)

The renderNumber function may truncate fractional digits beyond 20 decimal places, losing round-trip fidelity for numbers with high precision.

2. Dependent types for ordering invariant (Lck/Json/Syntax.lean:444-450)

SortedKVs currently enforces its key-sorted ordering invariant by convention. Using dependent types (a sigma type or a subtype with a Sorted proof) would make the invariant enforcement compile-time rather than runtime.

3. Missing docstrings (Lck/Json/Parser.lean)

• convOfPolicy: no docstring explaining what it does or why it exists
• SortedKVs.ofList: no documentation of the byte-lexicographic key ordering behavior
• Consider making convOfPolicy private to reduce public API surface

References

• Flagged by AI code review on PR #8

まず、指定された3つの領域を読みます: cli/LckJsonFmt.lean:30、Lck/Json/Syntax.lean:444-450、Lck/Json/Parser.lean。スコープを決める前に、精度、順序不変性、ドキュメントに関する提案を分けてください。完了とするには、convOfPolicy の API の公開範囲に関する問題を含め、列挙された各項目について合意された解決策が必要です。