sigma_preserving_consensual
plain-language theorem explainer
Researchers formalizing the consent interface in Recognition Science cite this result to confirm that any action preserving an agent's σ-charge satisfies the non-decreasing value condition. It follows directly from the definition of the value functional V = 1 - J(σ/σ_max) and the reflexivity of the ordering on reals. The proof is a one-line wrapper that unfolds the consent predicate and invokes the reflexivity lemma.
Claim. Let σ > 0 and σ_max > 0. Then the σ-preserving action satisfies valueFunctional(σ, σ_max) ≥ valueFunctional(σ, σ_max), where valueFunctional(σ, σ_max) = 1 - J(σ / σ_max) and J is the recognition cost function.
background
The module ConsentInterfaceFromJCost mechanizes consent from the pre-Big-Bang paper §ethics upgrade. The recognition value functional is V_i = 1 - J(σ_i / σ_max), with σ_i the agent's charge. Consent holds precisely when post-action V is at least pre-action V. The σ-charge itself is the gap between private preference and public vote, as defined in the Abilene paradox module: σ(a) = (if private_pref then 1 else 0) - (if public_vote then 1 else 0).
proof idea
This is a one-line wrapper. It unfolds the definition of IsConsensual, reducing the goal to valueFunctional sigma sigma_max ≥ valueFunctional sigma sigma_max, then applies the reflexivity theorem le_refl to conclude the inequality.
why it matters
The theorem is used to build ConsentInterfaceCert, which packages valueFunctional_at_optimum together with this consent property. It upgrades the scaffold in the paper's consent section to a proved structural theorem. The result ties consent directly to non-increasing J-cost under σ-preserving moves, consistent with the J-uniqueness and recognition composition law in the forcing chain, though the empirical mapping to observed systems remains open per the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.