valueFunctional_nonneg
plain-language theorem explainer
The declaration proves non-negativity of the agent recognition value functional whenever the normalized sigma charge obeys a J-cost upper bound of one. Researchers formalizing consent criteria in recognition-based mechanism design would cite this when verifying admissible charge ratios keep value positive. The argument is a direct unfolding of the functional definition followed by a linear-arithmetic inequality check.
Claim. Let $s>0$ and $s_>0$ be real numbers satisfying $J_>(s/s_>)≤1$. Then the recognition value functional obeys $0≤1-J_>(s/s_>)$.
background
The module mechanizes a consent interface from the J-cost function of the recognition framework. The value functional is defined by $V(s,s_>)=1-J_>(s/s_>)$, where $s$ is an agent's sigma charge and $s_>$ its healthy maximum; consent holds when an action leaves this quantity non-decreasing. The construction upgrades the scaffold tag in the pre-Big-Bang origin paper ethics section to a structural theorem with zero axioms or hidden hypotheses.
proof idea
The proof is a one-line wrapper that unfolds the definition of valueFunctional to obtain the expression 1 minus Jcost of the ratio, then applies linear arithmetic to the supplied hypothesis Jcost(ratio)≤1.
why it matters
This result supplies the non-negativity step required by the consent criterion in the ethics upgrade, closing the local structural theorem that converts the pre-Big-Bang paper scaffold into a proved interface. It rests on the J-uniqueness function from the forcing chain (T5) and the value-functional definition imported from the inflaton-potential and glossary modules. The module leaves open the empirical proxy-observable bridge to documented consent violations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.