IsConsensual
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.
claimAn 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 in Recognition Science
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.
scope and limits
- Does not compute sigma charges from underlying physical states.
- Does not address consent across multiple agents simultaneously.
- Does not supply a falsification procedure for the criterion.
- Does not extend to global multi-agent consent.
formal statement (Lean)
60def IsConsensual (sigma_before sigma_after sigma_max : ℝ) : Prop :=
proof body
Definition body.
61 valueFunctional sigma_after sigma_max ≥ valueFunctional sigma_before sigma_max
62
63/-- Consensual action preserves or improves value. -/