mkError
plain-language theorem explainer
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.
Claim. Define 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.