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

Leggi prima le tre aree indicate: cli/LckJsonFmt.lean:30, Lck/Json/Syntax.lean:444-450 e Lck/Json/Parser.lean. Separa le proposte relative a precisione, invarianza dell'ordine e documentazione prima di decidere il loro ambito; per considerare il lavoro completato sarebbe necessaria una risoluzione concordata per ciascun elemento elencato, inclusa la questione della visibilità dell'API per convOfPolicy.