IsConsensual
plain-language theorem explainer
The definition states that an action on an agent's sigma-charge is consensual precisely when the recognition value functional after the action is no smaller than before. Workers on the ethics interface in Recognition Science cite this when establishing preservation properties for sigma-preserving moves. It is introduced as the direct inequality on valueFunctional.
Claim. An action changing an agent's charge from $s_b$ to $s_a$ (with healthy maximum $s_m$) is consensual when $V(s_a,s_m) >= V(s_b,s_m)$, where the value functional is $V(s,s_m) := 1 - J(s/s_m)$ and $J$ is the J-cost.
background
The ConsentInterfaceFromJCost module supplies the consent criterion for the pre-Big-Bang paper ethics upgrade. The value functional is given by valueFunctional sigma sigma_max := 1 - Jcost (sigma / sigma_max), expressing agent recognition value as one minus the normalized J-cost. Consent is defined locally as preservation of this value under the action. This builds on the J-cost from the Cost module and the value definition in SpinStatistics. The module doc states that consent holds iff the J-cost on the post-action sigma does not increase.
proof idea
The declaration is a definition that directly sets IsConsensual to the inequality valueFunctional sigma_after sigma_max >= valueFunctional sigma_before sigma_max. No lemmas are applied; it is the primitive consent predicate.
why it matters
This predicate is the foundation for the equivalence theorem consensual_iff_jcost_nondecreasing and the certificate structure ConsentInterfaceCert. It completes the structural mechanization of the consent interface, replacing the scaffold tag in the paper with a partial theorem. The definition ties directly to the J-cost non-increase condition in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.