zero_output_zero_impact
plain-language theorem explainer
The theorem establishes that zero output magnitude produces zero impact on a receiver for any sensitivity value. Ethics auditors applying the O(1) externalization check would cite this to anchor the no-output baseline before scaling to nonzero cases. Proof is a one-line wrapper that unfolds the multiplicative definition and reduces via ring.
Claim. For any real sensitivity $s$, the impact satisfies $0 · s = 0$.
background
Module G-VII-1 implements an O(1) audit that checks whether an output increases another agent's J-cost. The impact function is defined as the product of output magnitude and receiver sensitivity. The upstream definition supplies the exact multiplicative form used here.
proof idea
One-line wrapper that unfolds sigmaImpact to the product 0 * s and applies the ring tactic to obtain equality with zero.
why it matters
The result supplies the zero baseline inside the Sigma Externalization Audit (G-VII-1). It closes the trivial case before any scaling or sensitivity analysis proceeds in the ethics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.