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

Read the three named areas first: cli/LckJsonFmt.lean:30, Lck/Json/Syntax.lean:444-450, and Lck/Json/Parser.lean. Separate the precision, ordering-invariant, and documentation proposals before deciding their scope; done would require an agreed resolution for each listed item, including the API-visibility question for convOfPolicy.