ActionConstraints
plain-language theorem explainer
Packages the two hard ethical constraints for the RS-to-RL bridge: consent (value derivatives non-negative for affected agents) and zero externalized harm (ΔS ≤ 0). Anyone wiring a feasible-action filter or LACompletion-style projector would cite it. It is a pure structure definition with no proof obligations beyond the field types.
Claim. An action-constraint record consists of two propositions: (i) consent holds whenever every affected value derivative satisfies $dV \ge 0$; (ii) harm is bounded whenever the externalized surcharge obeys $\Delta S \le 0$. Together they encode the combined consent-plus-harm-bound gate used by the RS$\to$RL bridge.
background
The module casts Recognition Science as control theory for reinforcement learning: moral states carry ledger, bonds, skew, and energy; admissible moves are the 14 virtue generators; hard feasibility is $\sigma=0$ via LACompletion; selection is lexicographic (feasible, then harm-minimax, then value, then robustness); and the policy is thermodynamic, $p(a|s)\propto\exp(-J(s,a)/T_R)$, evaluated on undiscounted eight-tick windows forced by T6.
Consent is the predicate $\mathrm{SatisfiesConsent}(dV):\Leftrightarrow dV\ge 0$: an action does not decrease any affected agent's value functional without consent, formalized as a derivative sign condition. Harm is the externalized action surcharge $\Delta S\ge 0$, with $\mathrm{HarmBound}(\Delta S,b):\Leftrightarrow\Delta S\le b$; the zero bound means no exported cost. The structure simply conjoins these two gates as named fields.
proof idea
No proof. This is a structure declaration whose fields are propositional constraints typed as universal implications into $\mathrm{True}$. Instantiation reduces to supplying (or deriving) those two propositions from the ambient consent and harm predicates.
why it matters
In the RS$\to$RL bridge, creativity (policy propose) is separated from physics (project onto the feasible set). This record is the ethical half of that hard gate: consent plus zero externalized $\Delta S$, matching the module's anti-parasitic stance that evil is local stability bought by exporting harm. It sits beside LACompletion ($\sigma=0$), the lexicographic selector, and the Gibbs policy as the constraint layer those selectors assume. The eight-tick cadence (T6/T7) and the J-cost thermodynamic policy remain the evaluation and scoring layers; this object only names the consent/harm filter. No downstream theorems yet consume it (used-by is empty), so it is infrastructure awaiting the selector and evil-detection sections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.