previewNatArray
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not validate or interpret the numerical meaning of the array entries.
- Does not accept or produce custom formatting strings.
- Truncates output strictly at the supplied limit; never returns the full array.
- Operates only on arrays of natural numbers.
Lean usage
let preview := previewNatArray cert.deltaJformal statement (Lean)
44def previewNatArray (arr : Array Nat) (limit : Nat := 4) : String :=
proof body
Definition body.
45 let previewVals := (arr.toList.take limit).map (fun n => toString n)
46 let body := String.intercalate ", " previewVals
47 if previewVals.isEmpty then "[]"
48 else
49 let ellipsis := if arr.size > previewVals.length then ", …" else ""
50 "[" ++ body ++ ellipsis ++ "]"
51