sigmaImpact
SigmaImpact defines the externalized J-cost impact on a receiver as the product of output magnitude and receiver sensitivity. Ethics researchers in Recognition Science cite it for the O(1) audit that checks whether an output increases another agent's recognition burden. The definition is a direct real-number multiplication with no lemmas or reductions required.
claimThe sigma impact is the real-valued function given by $I(m,s) = m s$, where $m$ is output magnitude and $s$ is receiver sensitivity.
background
In Recognition Science, J-cost is the recognition burden measured by $J(x) = (x + x^{-1})/2 - 1$. The Sigma Externalization Audit (G-VII-1) performs an O(1) per-output check to determine whether an output increases another agent's J-cost. This definition supplies the linear impact measure used inside that check.
proof idea
The definition is the direct product of the two real parameters; no lemmas or tactics are applied.
why it matters in Recognition Science
This definition supplies the impact function used by the downstream theorem zero_output_zero_impact, which proves that zero output yields zero impact. It implements the G-VII-1 audit step in the Ethics module and keeps externalization checks computationally trivial while remaining consistent with the J-uniqueness and phi-ladder structures of the forcing chain.
scope and limits
- Does not compute nonlinear J-cost increments.
- Does not incorporate phi-ladder rungs or forcing-chain constants.
- Does not normalize or bound the resulting impact value.
- Does not address discrete outputs or agent-specific sensitivity models.
Lean usage
theorem zero_output_zero_impact (s : ℝ) : sigmaImpact 0 s = 0 := by unfold sigmaImpact; ringformal statement (Lean)
15def sigmaImpact (output_magnitude receiver_sensitivity : ℝ) : ℝ :=
proof body
Definition body.
16 output_magnitude * receiver_sensitivity
17