sigma_conservation
plain-language theorem explainer
In a closed list of moral actions the summed source and target J-cost deltas equal zero, so net sigma is conserved. Game theorists certifying VCG mechanisms and urban modelers deriving Zipf rank-size laws cite the result to close their incentive and scaling arguments. The proof is a one-line wrapper that returns the supplied closed-system hypothesis unchanged.
Claim. Let $A$ be a finite list of moral actions, each carrying real source J-cost change $s_i$ and target J-cost change $t_i$. If $sum_i (s_i + t_i) = 0$, then the total sigma change across the list is zero.
background
MoralAction is the structure whose fields are the real numbers source_delta_j and target_delta_j recording the J-cost shift imposed on each of two agents. The MoralDebt module defines moral wrongness as sigma externalization, the uncompensated increase in another agent's J-cost. The upstream map operation from RSNative.Core applies a function to the value of a Measurement while copying its window, protocol, uncertainty and notes; the summation in the theorem is the concrete instance of that map applied to the delta pair.
proof idea
The declaration is a one-line wrapper that applies the hypothesis h_closed directly as the conclusion.
why it matters
The statement is invoked inside VCGCert to certify that truthful bidding remains a Nash equilibrium and inside ZipfFromCitySigmaCert to enforce the rank-size product identity. It supplies the conservation step that links the Recognition Composition Law to both mechanism design and city-size scaling, ensuring that sigma changes balance inside any closed population of agents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.