previewNatArray
plain-language theorem explainer
previewNatArray produces a compact bracketed string of the first few natural numbers from an input array, defaulting to four entries and appending an ellipsis when the source is longer. LNAL report generators cite it to summarize delta-J sequences inside certification outputs. The implementation is a direct list truncation, string conversion, and conditional concatenation.
Claim. Let $arr$ be an array of natural numbers and $limit$ a natural number (default 4). The function returns the string ``[n_1, n_2, ..., n_k]'' (or ``[]'' if empty) where the $n_i$ are decimal representations of the first $min(limit, |arr|)$ elements of $arr$, with ``, …'' appended when $|arr| > limit$.
background
The definition sits inside the LNALReports module that assembles readable summaries for LNAL compiler outputs and J-budget certificates. It relies on standard Array.toList, List.take, and String.intercalate operations. The module imports RSNative.Core.map (which transforms measurement values while preserving window and uncertainty) and ObservablePayloads.toList (which yields the canonical lepton-mass-ratio triple [μ/e, τ/e, τ/μ]).
proof idea
The body converts the array to a list, truncates to the limit, maps each entry to its decimal string, and joins the strings with commas. It then branches on emptiness or on whether the original length exceeds the preview length to decide whether to add the ellipsis before wrapping in brackets.
why it matters
The definition is invoked inside jmonotone_report to embed a readable ΔJ preview inside the J-monotone certification string. That report in turn supports the J-uniqueness step (T5) of the forcing chain by logging natural-number budget sequences without full enumeration. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.