HarmBound
plain-language theorem explainer
Predicate asserting that an externalized action surcharge ΔS stays at or below a numeric bound. Cited by the RS→RL bridge when packaging hard constraints on admissible virtue-actions, and by the zero-harm goal lemma. Pure definitional unfolding of a real inequality; no proof content.
Claim. For real numbers $\Delta S$ (externalized action surcharge) and $B$ (bound), the harm-bound predicate holds precisely when $\Delta S \le B$. By convention $\Delta S \ge 0$ always, and $\Delta S = 0$ means no externalized cost.
background
The ambient module is the RS→RL bridge: it recasts Recognition Science as control theory with MoralState (ledger, bonds, skew, energy), fourteen virtue generators as the admissible action basis, LACompletion as the σ=0 feasibility projector, and a lexicographic selector (feasible → harm-minimax → value → robustness). Thermodynamic policies are Gibbs in the J-cost at recognition temperature.
Harm here is the externalized action surcharge ΔS attached to a proposed virtue-action. The doc-comment fixes the sign convention: ΔS is always non-negative, and vanishing ΔS means the action externalizes no cost onto the ledger or bonds. The bound parameter is left free so the same predicate can express both a hard zero-harm cut and softer numerical caps.
(The gravity-side window slack also named deltaS is a different quantity; this definition only consumes a real parameter.)
proof idea
Definitional abbreviation, not a theorem. The body is the single inequality deltaS ≤ bound on ℝ. No lemmas, tactics, or algebraic reduction are involved; downstream results obtain the predicate by rfl or by direct application of the inequality.
why it matters
Supplies the harm half of ActionConstraints (consent + harm bound), the combined hard filter on virtue-actions before lexicographic selection. The sibling goal lemma goal_harm_bound_zero specializes the bound to zero and records the equivalence with ΔS ≤ 0, i.e. the no-externalized-harm cut used by the harm-minimax tier of the selector.
In the bridge design this is the quantitative stand-in for the ethical non-harm constraint: propose in the virtue basis, project to σ=0 via LACompletion, then reject any residual with positive externalized surcharge. It does not itself invoke T6/eight-tick or the J-cost uniqueness chain; those enter through the surrounding Gibbs policy and cadence structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.