maxHarm
plain-language theorem explainer
Maximum harm on an eight-tick evaluation window is the supremum of a state-wise harm functional across the eight moral states of a cadence. RL and control workers on the RS-to-RL bridge cite it when wiring the harm-minimax layer of lexicographic action selection. The body is a direct Finset supremum over the nonempty index set Fin 8; no extra lemmas.
Claim. Given an eight-tick cadence $c$ (states $c(t)$ for $t\in\{0,\ldots,7\}$) and a harm functional $h$ from moral states to $\mathbb{R}$, the maximum harm is $\max_{t\in\{0,\ldots,7\}} h\bigl(c(t)\bigr)$.
background
The module casts Recognition Science as control theory for RL: moral states, fourteen virtue generators as the action basis, $\sigma=0$ feasibility via propose-then-project, and a lexicographic multi-objective selector. Design rule from the module doc: no arbitrary discount; evaluate trajectories in undiscounted eight-tick blocks forced by T6 minimality (the eight-tick octave).
An eight-tick cadence packages the window map $\mathrm{Fin},8\to$ moral state together with the eight virtue actions. A moral state holds reciprocity skew $\sigma$, energy budget, value $V=\kappa\cdot I(A;E)-C_{J^*}$, a max-harm slot, and spectral gap $\lambda_2$. The argument $h$ is whatever external $\Delta S$-style harm measure the caller supplies; this definition only aggregates it over the window.
Upstream, the RS tick is the unit time quantum $\tau_0=1$, and one octave is eight ticks.
proof idea
Pure definition. The body is Finset.sup' on Finset.univ for Fin 8, with tick $0$ as the nonempty witness, applied to $t\mapsto h(c.\mathrm{window},t)$. No Recognition lemmas fire; only the standard-library supremum on a finite nonempty set.
why it matters
Feeds the second layer of the RS lexicographic selector: after the hard $\sigma=0$ gate, minimize worst-case harm ($\min\max\Delta S$). AuditResult stores this quantity as a field; lexBetter compares two audits by it once feasibility is settled. The eight-tick horizon is the T7 octave (period $2^3$) forced by T6, so the aggregator is not an arbitrary RL hyperparameter. Parent consumers in this module are the audit bundle, the lex comparator, and the moral-state record that carries a max-harm slot for training.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.