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

Lies zuerst die drei genannten Bereiche: cli/LckJsonFmt.lean:30, Lck/Json/Syntax.lean:444-450 und Lck/Json/Parser.lean. Trenne die Vorschläge zu Präzision, Ordnungsinvarianz und Dokumentation, bevor du ihren Umfang festlegst; für einen Abschluss wäre eine vereinbarte Lösung für jeden aufgeführten Punkt erforderlich, einschließlich der Frage der API-Sichtbarkeit für convOfPolicy.