consensual_iff_jcost_nondecreasing
plain-language theorem explainer
The equivalence states that an action changing sigma charge from s_b to s_a is consensual exactly when the J-cost on the normalized ratio to s_max does not increase. Researchers verifying ethical constraints on sigma-preserving interactions in the Recognition Science ethics layer would cite this biconditional. The proof reduces directly by unfolding the value functional and applying linear arithmetic to both directions.
Claim. Let $V(s, s_m) := 1 - J(s / s_m)$ denote the recognition value functional for positive reals $s, s_m$. An action taking charge $s_b$ to $s_a$ (with $0 < s_b, s_a, s_m$) is consensual if and only if $V(s_a, s_m) > V(s_b, s_m)$, which holds precisely when $J(s_a / s_m) < J(s_b / s_m)$.
background
The module supplies the consent interface for the pre-Big-Bang paper ethics upgrade. The recognition value functional is defined as $V(s, s_m) = 1 - J(s / s_m)$, where $s$ is an agent's sigma-charge and $s_m$ the maximum healthy charge. IsConsensual holds exactly when the post-action value is at least the pre-action value, i.e., the J-cost on the normalized charge does not rise.
proof idea
The proof is a one-line wrapper. It unfolds IsConsensual and valueFunctional, splits the biconditional with constructor, and closes both directions with linarith on the resulting arithmetic inequality.
why it matters
This theorem discharges the local consent criterion in the ethics upgrade, converting the scaffold tag in pre_big_bang_origin_paper.tex §consent into a structural theorem. It anchors the Recognition Science framework at the point where J-cost governs recognition events and value preservation supplies the ethical filter on sigma-preserving moves. The module notes that the proxy-observable bridge to empirical systems remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.