JMonotoneCert
plain-language theorem explainer
JMonotoneCert packages a boolean compliance flag together with diagnostic arrays and lists that record J-budget values, deltas, violations, and error strings for per-window monotonicity checks. Recognition Science work on cost functions derived from the Recognition Composition Law would cite this structure when building verification pipelines for J-monotonicity. The definition enumerates the record fields with defaults for the initial budget and empty diagnostic collections.
Claim. A record type consisting of a boolean flag $ok$ for compliance, an initial budget $initBudget : ℕ$ (default 4), arrays $budgets, deltaJ : Array ℕ$, a list $violations : List ℕ$ of violation steps, and a list $errors : List String$ of diagnostic messages.
background
JMonotoneCert lives in the Certificates module that imports JBudget and Parser. J denotes the cost function $J(x) = (x + x^{-1})/2 - 1$ whose monotonicity is governed by the Recognition Composition Law. The structure collects per-window data over eight-tick intervals, using the mkError helper to format violation reports that reference the first step where the budget increases.
proof idea
The declaration is a plain structure definition that lists the six fields with default values for budgets, deltaJ, violations, and errors. A subsequent simp lemma defines the verified predicate as the proposition that the ok flag equals true.
why it matters
The structure supplies the concrete data carrier for J-monotonicity diagnostics inside the certificate layer. It supports downstream checks that the J-cost remains non-increasing inside each eight-tick window, consistent with the T5 J-uniqueness and T7 octave steps of the forcing chain. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.