zero_output_zero_impact
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not address nonzero output magnitudes.
- Does not invoke the full J-cost expression beyond the impact multiplier.
- Does not cover multi-agent or time-dependent externalization.
formal statement (Lean)
18theorem zero_output_zero_impact (s : ℝ) : sigmaImpact 0 s = 0 := by
proof body
One-line wrapper that applies unfold.
19 unfold sigmaImpact; ring
20