mkError
mkError converts a list of violation indices into diagnostic strings that report the aligned 8-step window and the first step where J-budget increases. Certificate builders for LNAL programs or cellular automata simulations invoke it inside JMonotoneCert.fromProgram when the monotonicity check fails. The definition is a simple pattern match on the head of the input list that computes the window start as (i/8)*8 and emits one formatted message.
claimDefine the map $mkError : List(Nat) → List(String)$ by $mkError([]) = []$ and, for nonempty input with head $i$, $mkError(i::_) = [s!``J-monotone violated within window starting at $(i/8)*8$ (first increase at step $i→i+1$)''].
background
The module supplies a lightweight certificate package that diagnoses per-window monotonicity of the J-budget for compiled LNAL programs or cellular-automaton tapes. J-budget monotonicity is the concrete check that the cumulative J-cost (derived from the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$) never increases inside any 8-tick window. The central data structure is the record JMonotoneCert holding the Boolean outcome, the budget array, the delta-J array, the list of violation indices, and the generated error strings.
proof idea
The definition is a one-line pattern match on the input list. The empty case returns the empty error list. The nonempty case extracts the first index $i$, computes the window start as $(i/8)*8$, and returns a singleton list containing the single formatted diagnostic string.
why it matters in Recognition Science
mkError supplies the error-formatting step required by JMonotoneCert.fromProgram and fromSource, the two entry points that turn either raw code or LNAL source into a complete monotonicity certificate. The certificate in turn certifies compliance with the J-uniqueness fixed point (T5) and the eight-tick octave (T7) inside the unified forcing chain. It therefore closes the diagnostic loop for any downstream verification that a simulated system respects the Recognition Science mass ladder and Berry threshold.
scope and limits
- Does not itself run the monotonicity check or compute delta-J values.
- Reports only the first violation index; ignores any later indices.
- Assumes the supplied indices are already the output of jMonotoneViolations.
- Produces human-readable strings only; does not generate machine-checkable proof terms.
formal statement (Lean)
22private def mkError (idxs : List Nat) : List String :=
proof body
Definition body.
23 match idxs with
24 | [] => []
25 | (i::_) =>
26 let windowStart := (i / 8) * 8
27 [s!"J-monotone violated within window starting at {windowStart} (first increase at step {i}→{i+1})"]
28
29/-- Build a JMonotone certificate from compiled code. -/
30def JMonotoneCert.fromProgram (code : Array LInstr) (initBudget : Nat := 4) : JMonotoneCert :=
31 let budgets := simulateBudget code initBudget
32 let delta := deltaJPerWindow code
33 let violations := jMonotoneViolations code initBudget code.size
34 let ok := violations = []
35 let errors := if ok then [] else mkError violations
36 { ok := ok, initBudget := initBudget, budgets := budgets, deltaJ := delta,
37 violations := violations, errors := errors }
38
39/-- Build a JMonotone certificate directly from LNAL source text. -/
40def JMonotoneCert.fromSource (src : String) (initBudget : Nat := 4) : JMonotoneCert :=
41 let code := match parseProgram src with
42 | .ok code => code
43 | .error _ => #[]
44 fromProgram code initBudget
45
46/-- Helper returning the first violation index, if any. -/
47def JMonotoneCert.firstViolation? (c : JMonotoneCert) : Option Nat :=
48 match c.violations with
49 | [] => none
50 | i :: _ => some i