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

Lee primero las tres áreas indicadas: cli/LckJsonFmt.lean:30, Lck/Json/Syntax.lean:444-450 y Lck/Json/Parser.lean. Separa las propuestas de precisión, invariancia del orden y documentación antes de decidir su alcance; darlo por terminado requeriría una resolución acordada para cada elemento enumerado, incluida la cuestión de la visibilidad de la API de convOfPolicy.