goal_harm_bound_zero
plain-language theorem explainer
The zero harm bound is definitionally the same as a non-positive externalized action surcharge ΔS. Audit and RL-checklist authors cite it as the no-externalized-harm case inside the Recognition Stability Audit pipeline. The proof is pure reflexivity from the predicate definition.
Claim. For every real number $\Delta S$, the externalized-harm predicate at bound $0$ holds if and only if $\Delta S \le 0$.
background
The RSA RL module turns Recognition Stability Audit constraints into Lean goals an agent can close with a whitelist of simp and milestone lemmas. One exported predicate is the harm bound on an externalized action surcharge $\Delta S$.
By definition the harm predicate at a real bound $b$ is simply $\Delta S \le b$. Upstream documentation states that harm is non-negative ($\Delta S \ge 0$ always) and that $\Delta S = 0$ means no externalized cost. Bound zero therefore isolates the no-externalized-harm regime.
This declaration is one of the module's proved gold training goals: closed theorems with no sorry that exercise the pipeline and supply a reward signal via goal closure.
proof idea
One-line wrapper by definitional equality. The harm predicate at bound $0$ unfolds to $\Delta S \le 0$, so the biconditional is rfl.
why it matters
Canonical gold theorem for the RSA reinforcement-learning training loop: agents learn that the zero harm bound is exactly the non-positive surcharge condition. The module frames such goals as checklist and reward signals, not as links in the T0–T8 forcing chain. No downstream theorems currently depend on it. It anchors the harm side of the audit (near the consent condition $D_j V_i \ge 0$) without touching J-uniqueness, the phi ladder, eight-tick structure, or dimensional forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.